cert
plain-language theorem explainer
Packages a certificate that the RS gas-constant domain cost vanishes on equal positive ratios, stays nonnegative off-diagonal, and has a positive canonical threshold. Anyone citing the structural gas-constant match (R ≈ φ^7 · 0.286) uses this inhabited record. The body is a three-field structure instance wiring sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(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 universal gas constant $R \approx 8.314,\mathrm{J/(mol\cdot K)}$ in Recognition Science units. The claimed match is $R = k_B N_A$ realized as a $\phi$-power: $\phi^7 \cdot 0.286 \approx 8.30$, about $0.7%$ off the CODATA value, recorded as a structural (sorry-free) theorem.
GasConstRS is the structure that packages three cost axioms for that domain: diagonal vanishing, nonnegativity for positive mass/energy-like arguments, and positivity of a canonical threshold. Domain cost is the local cost functional on pairs of reals; the upstream foundation result cost_nonneg states that every recognition event has nonnegative J-cost, via Jcost_nonneg at positive state.
The certificate sits beside sibling facts domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, which discharge the three fields.
proof idea
One-line structure instance. The three fields of GasConstRS are filled by the sibling lemmas domainCost_at_eq (diagonal cost zero), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (threshold positivity). No extra tactics or algebraic work; the def is pure packaging.
why it matters
Gives an inhabited witness that the gas-constant cost layer meets the Recognition cost axioms (nonnegative J-type cost, identity at equal ratios, positive threshold). The module frames this as the structural half of the $R \approx \phi^7 \cdot 0.286$ match, consistent with the RS constant ladder built from $\phi$ (T6 fixed point) and the nonnegative cost forced by the J-uniqueness chain (T5). No downstream theorems are wired yet (used_by empty); the sibling cert_inhabited is the natural consumer. Does not itself close the numerical $0.7%$ residual; it only certifies the cost interface the match sits on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.