RSAstro005Cert
plain-language theorem explainer
Certificate bundle for Astrophysics Module 5 (white-dwarf radius match at ~7000 km). It packages three structural facts: the domain cost vanishes on the diagonal, is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance to discharge the module's structural obligations. The structure itself is a pure interface; the proofs live in the field witnesses.
Claim. A certificate consists of three properties: (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 5 of the RS astrophysics layer records the white-dwarf radius prediction $\phi^{19}\cdot 0.75,\mathrm{km}\approx 7012,\mathrm{km}$, reported as a structural match near $7000,\mathrm{km}$. Status is a structural theorem with no sorry and no extra axioms.
The domain cost is the local cost functional used to score mass/energy pairs in this module; its diagonal vanishing and nonnegativity mirror the global J-cost facts from the recognition calculus. Upstream, cost_nonneg in ObserverForcing states that every recognition event has nonnegative cost via Jcost_nonneg on a positive state. The canonical threshold is the positive cutoff against which the module's radius (or related scale) comparison is judged.
The certificate is the typed package of those three obligations so the module can export a single inhabited witness rather than three free-floating lemmas.
proof idea
No proof body: this is a structure declaration. Inhabitation is supplied by the sibling cert, which fills the three fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. Those field proofs are the actual content; the structure only names the interface. cert_inhabited then wraps cert as Nonempty RSAstro005Cert.
why it matters
Gives Module 5 a single, checkable certificate type for the white-dwarf radius structural claim. Downstream, cert builds a concrete inhabitant and cert_inhabited proves nonemptiness, which is the standard RS pattern for module-level structural theorems (0 sorry, 0 axiom).
In the broader framework this sits under the astrophysics applications of the phi-ladder mass/radius scalings (primer: mass formula on the phi-ladder; constants fixed in RS-native units). It does not itself derive $\phi^{19}$ or the 0.75 km yardstick; it certifies the cost and threshold hygiene those comparisons rely on. Parent use is local to this module's export surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.