RSAstro002Cert
plain-language theorem explainer
Certificate bundle for Astrophysics Module 2 (Chandrasekhar mass): diagonal vanishing of the domain cost, nonnegativity for positive mass and energy arguments, and positivity of the canonical threshold. Anyone citing the inhabited structural certificate for the exact relation $\phi^{-1}\cdot 2.33\,M_\odot=1.440\,M_\odot$ depends on this interface. It is a pure structure definition; the three fields are discharged by sibling lemmas in the same module.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost at equal arguments vanishes, $\mathrm{cost}(r,r)=0$; (ii) for all positive reals $m,e>0$, the domain cost is nonnegative, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Module RS_Astro_Module_002 packages the Chandrasekhar limiting mass as an exact Recognition Science identity: $\phi^{-1}\cdot 2.33,M_\odot=1.440,M_\odot$, marked as a structural theorem with no sorry and no axioms. The local cost is a two-argument domain cost on reals (mass and energy style inputs), not the one-argument J-cost on recognition events, though it inherits the same nonnegativity philosophy.
Upstream, ObserverForcing records that every recognition event has nonnegative cost via $J$-cost nonnegativity at positive state. Here the analogous statements are specialized: cost vanishes on the diagonal $m=e\neq 0$, stays nonnegative off-diagonal for positive arguments, and a fixed canonical threshold is positive. Those three properties are the only data the certificate carries.
proof idea
No proof body: this is a structure declaration. Inhabitation is supplied downstream by cert, which fills the three fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Nonemptiness is then the one-line ⟨cert⟩.
why it matters
The structure is the typed interface that makes Module 2's Chandrasekhar claim certifiable inside the Astrophysics layer. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty RSAstro002Cert, so later astrophysics results can assume the cost and threshold package without re-proving diagonal vanishing or positivity.
In the broader framework this sits under the phi-ladder and mass-yardstick story (masses as rung shifts of a fixed yardstick). The module headline is the exact Chandrasekhar number $\phi^{-1}\cdot 2.33,M_\odot=1.440,M_\odot$; the certificate does not itself derive that number, but it is the structural gate that keeps the cost side of the argument nonnegative and normalized before any numerical identification is used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.