5. The cap on the race price
This page proves an explicit upper bound on the race price j(a)=a\ln\Gamma(1-1/a)-\gamma_E of the
race page, equation (R1): for every real a>1,
j(a)<F(a)=\frac{533}{648a}+\frac{241}{600a^2}+\frac{6503}{24000a^2(a-1)},
and at a=211/45 it evaluates the right side exactly, F(211/45)=838748045/4256919936, which is below
the rational price u=3941/20000 used by the assembly. This is step 4 of the route. The race inequality
h\le aB+2\,j(a)\,d keeps the exact price j(a); since d\ge0, the cap turns it into h\le aB+2ud, which the
assembly NaturalLatents.General.T_le_of_connected (NaturalLatents/General/Pricing.lean) combines with the ledger and
the mismatch payment at a=211/45 and u=3941/20000. Notation
follows section 0 of the contact page; every logarithm is natural.
What the cap is. The price j(a) is a value of the Gamma function. The proof expands it in a power series in
1/a whose coefficients are the values \zeta(k)=\sum_{n\ge1}n^{-k} of the Riemann zeta function \zeta, keeps the terms k=2 and k=3, dominates the
rest by a geometric series, and bounds \zeta(2), \zeta(3) and \zeta(4) by rational numbers obtained from
elementary sums and from \pi<3.1416. The series and a sharp bound on \zeta(2) are needed because the margin is
small: at a=211/45 the cap lies below u by only 48767743/2660574960000\approx1.8\cdot10^{-5}, while
the cap itself exceeds the price, whose numerical value is j(211/45)\approx0.196778, by about
2.5\cdot10^{-4}. With the bound \zeta(2)<79/48 of (K33) at (k,N)=(2,4) in place of 533/324, the same cap would be
93233145/472991104\approx0.197114, above u. The numerical values in this paragraph are for orientation
only; the pricing uses only the exact comparison of section 5.
Each lemma below states its hypotheses, so that it can be read alone. The lemmas are numbered K12 and K13 and the
equations (K32) to (K40a), continuing the numbering of the race page. Here F is the cap, not the random
map of the ledger page; f in the proof of Lemma K12 is the function x^{-k}, and y, k, n,
N are local. Unless prefixed otherwise, the Lean declarations named
below are in the namespace NaturalLatents.General, in NaturalLatents/General/Cap.lean.