cert
plain-language theorem explainer
Packages the three certificate fields for the carbon-oxygen stellar module into one inhabited record: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Astrophysicists citing the structural C/O = φ^{-1.5} claim use this bundle. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There is a certificate for the carbon-oxygen stellar domain consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 12 treats carbon-oxygen stellar chemistry as a structural Recognition Science claim: the predicted C/O ratio is $\phi^{-1.5}\approx 0.504$, compared with the observational band near $0.55$ (about 10% off). Status is structural theorem, zero sorry and zero axiom.
The certificate structure RSAstro012Cert packages three elementary cost properties of the domain cost functional used in this module. Domain cost is the local specialization of the Recognition J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive reals.
Sibling lemmas establish the three fields separately: diagonal vanishing, nonnegativity for positive mass/energy arguments, and positivity of the canonical threshold against which the domain is scored.
proof idea
One-line structure constructor. It fills cost_at_eq by domainCost_at_eq, cost_nonneg by domainCost_nonneg, and threshold_pos by canonicalThreshold_pos. No new algebra; the work lives in those three sibling proofs (the nonnegativity field ultimately rests on the foundation fact that J-cost is nonnegative).
why it matters
Gives a single named inhabitant of the Module-12 certificate so downstream astrophysics code can assume the cost axioms without re-proving them. The module frames C/O chemistry as structural: the ratio is forced to $\phi^{-1.5}$ on the phi-ladder rather than fitted. That sits downstream of the forcing chain landmarks T5 (J-uniqueness) and T6 ($\phi$ as self-similar fixed point), which fix the cost and the ladder rung arithmetic used for elemental ratios.
No used_by edges are recorded yet; the immediate consumer in-module is the inhabitedness witness for the same certificate type. The declaration closes the packaging step for a zero-sorry structural theorem, not an observational fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.