cert
plain-language theorem explainer
Packages three elementary properties of the polymer-domain cost into a single certificate: diagonal vanishing, nonnegativity, and a positive canonical threshold. Polymer or RS chemistry work that wires freely jointed chain statistics to J-cost would cite it. The body is pure structure assembly from three local lemmas.
Claim. There is a polymer-chain statistics certificate asserting: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats freely jointed chain end-to-end statistics under Recognition Science: classical $\langle r^2\rangle=Nl^2$, with RS persistence lengths of the form $\ell_p=\ell_0\varphi^k$ by polymer class (DNA cited as $\ell_p\approx 50,\mathrm{nm}\approx\varphi^8\times 1,\mathrm{nm}$).
The domain cost is the local specialization of the RS J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) to polymer monomer/end-to-end ratios. Upstream, cost_nonneg records that every recognition event has nonnegative cost via Jcost_nonneg at positive state. The certificate structure simply freezes the three algebraic facts needed before any chain-length or threshold comparison.
proof idea
Definitional structure inhabitant, not a tactic proof. The three fields of PolyChainStatCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis.
why it matters
Gives the chemistry layer a single named witness that the polymer-domain cost behaves like a genuine RS cost (zero on matched ratios, nonnegative, with a usable positive threshold). That is the structural prerequisite for comparing chain statistics against J-cost thresholds and for the $\varphi^k$ persistence-length ladder sketched in the module doc (eight-tick / $\varphi$ landmarks). No downstream consumers are wired yet (used_by empty); the certificate is the handoff point for later polymer theorems rather than a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.