2.1. 0. Units, notation and standing inputs
Units. All entropies, mutual informations and relative entropies in the proof pages are in nats. The deterministic
optimum T and the stochastic optimum \tau scale by the same factor under a change of units, so the final
inequality T(p)\le(13999/2000)\,\tau(p) is unit-free. A quantity stated in bits is converted once:
H_{\mathrm{nat}}=(\ln2)H_{\mathrm{bits}},\quad I_{\mathrm{nat}}=(\ln2)I_{\mathrm{bits}},
\qquad (M,B,T,\tau,h)_{\mathrm{nat}}=(\ln2)(M,B,T,\tau,h)_{\mathrm{bits}}.
\qquad \text{(D1)}
Hereafter H,I,M,B,T,\tau,h are in nats. The relative entropy and the pair charge are natural-log quantities and are
unchanged. Probabilities and d,s,J,BC,\beta are dimensionless, whereas \Psi and \gamma have nat units. There
is no final division by \ln 2 in the mismatch conclusion. Here M, B, T, \tau and d are defined
in (D3) and s, J in (C1.3); BC denotes either marginal affinity, BC_X or BC_Y, and these and
\Psi are defined in (A2.1) on the affinity page; h is the seed average of the two fixed-map
conditional entropies H(f(Z)\mid X)+H(f(Z)\mid Y), defined in (L1) and (L7) on the ledger page; and
\beta, \gamma are the parameters of the pair charge below.
Lean: NaturalLatents.General.TNat and NaturalLatents.General.tauNat (NaturalLatents/General/Definitions.lean) are the
bit-valued stoch_to_det.T and stoch_to_det.tau (NaturalLatents/Upstream/Functionals.lean) converted by
NaturalLatents.General.nats, multiplication by Real.log 2 (NaturalLatents/General/Nats.lean, the only General file
where that factor appears); mediation, redundancy, replicaBudget and seedEntropy in Definitions.lean, the Lean
forms of M, B, K and h, are converted the same way. NaturalLatents.General.bits_of_nats (Nats.lean)
converts the nat-valued bound on connected supports back to the bit-valued stoch_to_det.T and stoch_to_det.tau, and
NaturalLatents.T_le_c_mul_tau (NaturalLatents/Main.lean) then extends it to every law in bits.
Conventions. For a finite law, all conditional sums range over positive-probability conditioning events. Entropy
uses 0\ln0=0, and a relative entropy sums over the positive mass of its first argument. With the reference
positive on that support,
H(q)=-\sum_{i:q_i>0}q_i\ln q_i,\qquad
D(q\Vert v)=\sum_{i:q_i>0}q_i\ln(q_i/v_i),\qquad
I(q)=D(q\Vert q_X\otimes q_Y).
\qquad \text{(D2)}
Lean: the mutual information I(q) of a law on X\times Y is the natural-log stoch_to_det.Knat
(NaturalLatents/Upstream/DomFloorCore.lean), used directly, with no conversion. Knat is an equivalent all-cell scalar-integrand formula rather than
the positive-support sum (D2); on probability laws, stoch_to_det.Knat_eq_log_two_mul_Ixy (same file) identifies it
with natural-log mutual information.
Latents and scores. A finite latent is a joint law of Z=(X,Y) and a finite label L, or equivalently a
mixture p=\sum_i\pi_iq_i, with r_z(i)=\Pr(L=i\mid Z=z) on \mathrm{supp}\,p. Set
\begin{aligned}
M&=I(X;Y\mid L),&B&=I(L;X\mid Y)+I(L;Y\mid X),\\
\tau(p)&=\inf_L(M+B),&
T(p)&=\min_{A=f(Z)}[I(X;Y\mid A)+H(A\mid X)+H(A\mid Y)],\\
d&=\sum_{z:p(z)>0}p(z)\left[1-\sum_i r_z(i)^2\right].
\end{aligned}
\qquad \text{(D3)}
The deterministic minimum exists because a finite alphabet has finitely many partitions. For a deterministic map f
on \mathrm{supp}\,p, write D_p(f) = I(X;Y\mid f(Z)) + H(f(Z)\mid X) + H(f(Z)\mid Y) for the score of the code
f(Z), so that T(p)=\min_f D_p(f).
Lean: a finite latent is stoch_to_det.Latent (NaturalLatents/Upstream/Functionals.lean), and posterior (the
posterior r_z(i)), mediation (M), redundancy (B) and mismatch (d) are in
NaturalLatents/General/Definitions.lean. stoch_to_det.detScore (NaturalLatents/Upstream/Functionals.lean) is the
score in bits of a map on all of X\times Y: the score D_p(f) is detScoreNat (NaturalLatents/General/Nats.lean),
that is nats of detScore, after extending the map off the support. In Lean, T is an infimum over deterministic latents
and d sums over all cells, the cells with p(z)=0 contributing zero.
The supplied setup. The mismatch payment is applied to a latent p=\sum_i\pi_iq_i with positive priors, distinct
components that are positive contacts of one feasible kernel on the common support \mathrm{supp}\,p (contacts and
feasibility are defined in section 1), and M+B=\tau(p). Such a latent exists when the support of p is connected
as a bipartite graph between the values of X and the values of Y (defined on the
setup page), and the bound for a general finite law is
reduced to that case by splitting the support into its connected components: with component weights \rho_k and
normalized component laws \bar p_k, \sum_k\rho_k\tau(\bar p_k)\le\tau(p) and T(p)\le\sum_k\rho_kT(\bar p_k)
((E3.F) on the extension page). Neither step is proved on this page; they are proved by
NaturalLatents.General.exists_setup_of_connected (NaturalLatents/General/Setup.lean) and
NaturalLatents.General.extension_of_connected (NaturalLatents/General/Extension.lean).
Lean: the setup is the structure NaturalLatents.General.CommonSetup (NaturalLatents/General/Definitions.lean),
which also records that every posterior r_z(i) is positive on the support; it is constructed for connected support
by NaturalLatents.General.exists_setup_of_connected (NaturalLatents/General/Setup.lean), and the extension to every
law is NaturalLatents.General.extension_of_connected (NaturalLatents/General/Extension.lean), which applies
stoch_to_det.reduce_to_connected (NaturalLatents/Upstream/Connected.lean).
The pair charge. The pair charge PC(\beta,\gamma), for \beta\ge0 and \gamma>0, is the averaged
natural-logarithm inequality
\frac{I(P)+I(R)}2+\beta\Psi(s(P,R))\ge\gamma
for every two distinct positive contacts P,R of a common feasible kernel, on a support S that need not be a rectangle (cells of X\times Y
outside S, the holes, are allowed); s is defined in
(C1.3) and \Psi in (A2.1). It is a hypothesis of the mismatch payment, generic in \beta\ge0 and \gamma>0, and
is not used on this page.
Lean: NaturalLatents.General.HasPairCharge (NaturalLatents/General/Definitions.lean), stated over a domain of pairs;
NaturalLatents.General.pairCharge_C (NaturalLatents/General/PairCharge.lean) proves it on
distinct positive contacts of a common feasible kernel at (\beta,\gamma)=(23/250,7/60). The formal HasPairCharge definition accepts
arbitrary real \beta and \gamma; the formal payment inequality mismatch_payment
(NaturalLatents/General/Payment.lean) requires \beta\ge0 and \gamma\ge0. This page keeps \gamma>0 so that
later bounds may divide by \gamma.