5.2. 5. Remark: the cap at a = 211/45🔗

This remark is outside the proof of Lemma K13. For a = 211/45 and u = 3941/20000, the preceding universal lemma gives j(211/45) < F(211/45). Termwise substitution, with a - 1 = 166/45, is

\begin{aligned} \frac{533}{648a}&=\frac{533\cdot45}{648\cdot211}=\frac{23985}{136728}=\frac{2665}{15192},\\ \frac{241}{600a^2}&=\frac{241\cdot45^2}{600\cdot211^2}=\frac{488025}{26712600}=\frac{6507}{356168},\\ \frac{6503}{24000a^2(a-1)} &=\frac{6503\cdot45^3}{24000\cdot211^2\cdot166} =\frac{592585875}{177371664000}=\frac{1580229}{472991104}. \end{aligned} \qquad \text{(K39a)}

The three reduced denominators are 15192=2^3\cdot3^2\cdot211, 356168=2^3\cdot211^2 and 472991104=2^7\cdot83\cdot211^2, so their least common multiple is 2^7\cdot3^2\cdot83\cdot211^2=4256919936, with multipliers 280208, 11952 and 9. Common-denominator arithmetic gives

\begin{aligned} F(211/45) &=\frac{2665}{15192}+\frac{6507}{356168}+\frac{1580229}{472991104}\\ &=\frac{2665\cdot280208+6507\cdot11952+1580229\cdot9}{4256919936}\\ &=\frac{746754320+77771664+14222061}{4256919936} =\frac{838748045}{4256919936}. \end{aligned} \qquad \text{(K39)}

The strict comparison and reduced margin are

\begin{aligned} &20000\cdot838748045=16774960900000<16776521467776=3941\cdot4256919936,\\ &3941\cdot4256919936-20000\cdot838748045=1560567776>0,\qquad \frac{3941}{20000}-F(211/45)=\frac{48767743}{2660574960000}>0. \end{aligned} \qquad \text{(K40)}

The exact margin reduction is

1560567776=32\cdot48767743,\qquad 20000\cdot4256919936=85138398720000=32\cdot2660574960000. \qquad \text{(K40a)}

Thus the full cap lies strictly between j(211/45) and 3941/20000. This remark supplies pricing arithmetic only; it does not change the universal statement of Lemma K13.

Lean: inside T_le_of_connected (NaturalLatents/General/Pricing.lean), racePrice_lt_capC3b at 211/45 followed by norm_num [gammaPriceCap] proves gammaPrice (211/45) < 3941/20000; the intermediate fractions of (K39a) to (K40a) are not stated.