2. Contact moments and the feasible Hessian
The reproduced contact conventions apply to the analytic chapters; the table-form chapter uses bits.
This page fixes the units and notation shared by the proof pages, and proves the moment relations of two positive
contacts of one feasible kernel: the ratio and conditional-moment identities, the quadratic and quartic moment
identities, the separation range 0<s<2 for distinct contacts and s=J=0 for equal contacts, a feasibility
inequality for nonnegative marginal fields, the Hessian test for centered marginal fields, and the quartic bound
J\le6A_0B_0-s^2\le s^2/2, with s, J, A_0 and B_0 defined in (C1.3). These relations are the
input of the affinity bound, which the mismatch payment applies to every pair of distinct components of
the setup latent (step 6 of the route); Lemma C1.3 and the Hessian test are
also used by the pair charge. In the assembly NaturalLatents.General.T_le_of_connected
(NaturalLatents/General/Pricing.lean), contact_moments is applied to each pair of distinct components of the setup
latent, and its conclusion is passed to affinity_bound.
Each lemma below states its quantified hypotheses, so that it can be read alone. Lemma, theorem, remark and equation
numbers carry the prefix of the page that states them: S for the setup, C for this page, L for the
ledger, R for the race, K for the cap, A for the affinity bound, Q for
the replica budget, P for the payment, PC for the pair charge, M for the
assembly, E for the extension and T for the table form; the tags (D1) to
(D3) of section 0 serve every page. Unless explicitly
qualified otherwise, the Lean declarations named below are in the namespace NaturalLatents.General; declarations
prefixed stoch_to_det are upstream, in NaturalLatents/Upstream/, adapted from
DLorell/stochtodet.