4. The exponential race
This page proves the race inequality. Notation follows section 0 of the contact page. Let p be a
probability law on a product X\times Y of finite alphabets, let L be a finite latent of p whose posterior rows
r_z(i)=\Pr(L=i\mid Z=z) are positive at every cell z of the support, and let a>1. Running an exponential race
among the labels, with one set of clocks shared by all cells, gives a calibrated random deterministic map F from the
cells to the labels with h\le aB+2\,j(a)\,d. Here B=I(L;X\mid Y)+I(L;Y\mid X) is the leakage budget of L,
d is the probability that two labels drawn independently from the posterior at a cell drawn from p disagree,
h is the seed average of the conditional entropies of the fixed maps given X and given Y, and
j(a)=a\ln\Gamma(1-1/a)-\gamma_E, with \Gamma the Gamma function and \gamma_E Euler's constant; section 1
gives the exact definitions. This is step 3 of the
route: the ledger turns such an F into
T(p)\le M-B/2+3h/2, where T(p) is the deterministic optimum and M=I(X;Y\mid L) as in (D3), a
separate cap page bounds j(a), and the mismatch payment bounds d. In the
assembly NaturalLatents.General.T_le_of_connected (NaturalLatents/General/Pricing.lean), exists_race is applied at
a=211/45 to the setup latent, whose posterior rows are positive by the field rows_pos of the setup.
Each lemma below states its hypotheses, so that it can be read alone. The lemmas are numbered R1 to R11 and the equations
(R1) to (R31); the cap page continues both numberings. Unless prefixed stoch_to_det, the Lean declarations named below are in the namespace
NaturalLatents.General; the stoch_to_det declarations are in NaturalLatents/Upstream/, adapted from
DLorell/stochtodet.