9. The pair charge
This page proves the pair charge PC(23/250,7/60) of section 0 of the contact page, in
strict form: for every two distinct positive contacts P,R of one feasible kernel on a common support S, holes
allowed,
\frac{I(P)+I(R)}2+\frac{23}{250}\Psi(s)>\frac7{60},\qquad \Psi(s)=-2\ln b(s),\quad b(s)=1-\frac{9s}{16}+\frac{3s^2}{64},
with s the separation of (C1.3) and b, \Psi as in (A2.1) of the affinity page. For
0<s\le1 an entropy payment for one explicit statistic bounds the averaged information below (section 4), and a
scalar certificate closes the charge (section 5); for 1\le s<2 the separation price alone pays. The charge is the
hypothesis PC of the mismatch payment, which turns it into \gamma d\le(1+2\beta)M+\beta B for the setup latent (step 6 of the
route), and its two parameters (\beta,\gamma)=(23/250,7/60)
enter the pricing of the constant. In the assembly NaturalLatents.General.T_le_of_connected
(NaturalLatents/General/Pricing.lean), the HasPairCharge hypothesis of mismatch_payment (NaturalLatents/General/Payment.lean)
is discharged by the pair-charge theorem pairCharge_C.
Lemma PC4.0 and Theorem PC5.3 state the standing hypotheses in full; Lemmas PC4.1 to PC4.5 refer to Lemma PC4.0,
and the scalar Lemmas PC5.1 and PC5.2 state their ranges. 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. The Lean proof
of this charge is complete; its declarations are in NaturalLatents/General/PairCharge.lean and the modules
PairCharge/Gram.lean, Features.lean, MomentBounds.lean, Information.lean, Correction.lean and
Certificate.lean.