8. The mismatch payment
This page proves that the posterior mismatch d of the supplied setup latent is paid by its budgets: for every
\beta\ge0 and \gamma>0 such that the pair charge PC(\beta,\gamma) of section 0 of the
contact page holds, \gamma d\le(1+2\beta)M+\beta B. The proof weights the pair charge of each pair of
distinct components by the probability \mu_{ij} that two labels drawn independently from the posterior at the same
cell are i and j, bounds the separation prices by the replica budget K through the
affinity bound and a midpoint relative-entropy inequality, and closes with the
replica budget K\le2M+B. The argument is generic in (\beta,\gamma); at the pair charge
PC(23/250,7/60), it gives (7/60)\,d\le(148/125)\,M+(23/250)\,B. This is
step 6 of the route. In the assembly
NaturalLatents.General.T_le_of_connected (NaturalLatents/General/Pricing.lean), mismatch_payment is applied to the
setup latent, with its affinity hypothesis discharged by affinity_bound applied to contact_moments, its replica hypothesis by
replica_budget, and its pair-charge hypothesis by the pair charge PC(23/250,7/60), pairCharge_C.
Each lemma below states its hypotheses, so that it can be read alone. Units and conventions are those of section 0 of
the contact page: information is in nats, M, B and d are defined in (D3), the mutual
information I(q) of a law on X\times Y in (D2), and a relative entropy sums over the positive mass of its first
argument. The replicas L_1,L_2 are those of (Q3.2) on the replica page, and K is defined in (Q3.3)
there. Unless prefixed stoch_to_det, the Lean declarations named below are in the namespace NaturalLatents.General,
in NaturalLatents/General/Payment.lean; the stoch_to_det declarations are in NaturalLatents/Upstream/, adapted
from DLorell/stochtodet. In Lemma P5.2 the letters a,b,t,v are
probability vectors and c is their Bhattacharyya coefficient, not the race exponent a, the quadratic b of
(A2.1) or the constant of the theorem.