cert
plain-language theorem explainer
Packages a three-field certificate that the domain J-cost vanishes on equal arguments, stays nonnegative for positive mass and energy, and that the canonical threshold is positive. Anyone citing the RS heat-capacity anomaly (α ≈ J(φ)/2) needs this inhabited certificate. The body is a pure structure assembly of three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the specific-heat singularity $C_p \propto |T-T_c|^{-\alpha}$ near a continuous phase transition. Recognition Science places the exponent between mean-field ($\alpha=0$) and 3D Ising ($\alpha\approx 0.110$) by reading $\alpha=J(\varphi)/2\approx 0.059$ off the unique cost $J(x)=(x+x^{-1})/2-1$ forced at T5.
Domain cost is the local J-cost comparison used as the thermodynamic free-energy proxy; the certificate demands it vanish when the two arguments coincide (equilibrium identity) and stay nonnegative off-diagonal. The canonical threshold is the positive scale that marks the anomaly window.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has $0\le e.\mathrm{cost}$ because $J$ is nonnegative on the positive reals.
proof idea
One-line structure inhabitant. The three fields of HeatCapAnomalyCert are filled by the sibling facts domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed here.
why it matters
Gives a zero-sorry, zero-axiom certificate object for the structural claim that the J-cost domain model is a legitimate free-energy proxy for the heat-capacity anomaly. The module status line records this as a structural theorem of the eighty-sixth Plan v7 pass: RS sits between mean-field and Ising, with $\alpha=J(\varphi)/2$.
No downstream consumers are wired yet (used_by empty), so the certificate is presently a standing witness rather than an input to a larger derivation. It anchors the T5 J-uniqueness cost inside condensed-matter phenomenology and keeps the anomaly prediction auditable without axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.