PolyChainStatCert
plain-language theorem explainer
Certificate packing three analytic side-conditions used for polymer end-to-end statistics derived from J-cost: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Polymer and RS chemistry developments cite it as the interface that a concrete cost model must satisfy. It is a pure structure definition; inhabitation is discharged elsewhere by the sibling lemmas.
Claim. A certificate consists of three properties of the polymer domain cost $C$ and threshold $\tau$: (i) $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module treats freely jointed polymer chains in Recognition Science units. Classical statistics give $\langle r^2\rangle=Nl^2$ for $N$ monomers of length $l$. RS upgrades the persistence length to a $\varphi$-ladder, $l_p=l_0\varphi^k$, with DNA as the running example ($l_p\approx 50,\mathrm{nm}\approx\varphi^8\times 1,\mathrm{nm}$).
Domain cost is the local J-cost model on mass/energy (or length) coordinates used for chain statistics; the canonical threshold is the positive cutoff against which those costs are compared. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The certificate simply packages the three inequalities the chemistry layer needs from that cost calculus.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Concrete witnesses are supplied later by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos when the default certificate is built.
why it matters
Gives the chemistry module a named, reusable interface for "J-cost is a valid polymer statistic generator." Downstream, cert assembles the three sibling lemmas into an inhabitant, and cert_inhabited records Nonempty PolyChainStatCert, closing the structural theorem (0 sorry, 0 axiom) advertised in the module doc. Ties the polymer persistence-length story ($l_p=l_0\varphi^k$, DNA near $\varphi^8$) to the global J-cost nonnegativity and identity-minimum facts from the forcing/observer layer, without yet deriving the full $\langle r^2\rangle$ law inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.