cert
plain-language theorem explainer
Packages the three structural obligations for the white-dwarf radius certificate: diagonal vanishing of the domain cost, non-negativity off the diagonal, and positivity of the canonical threshold. Astrophysicists citing the RS white-dwarf match (φ¹⁹·0.75 km ≈ 7000 km) use this inhabitant. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There exists a certificate 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 5 of the RS astrophysics stack targets the white-dwarf radius scale $\phi^{19}\cdot 0.75,\mathrm{km}\approx 7012,\mathrm{km}$, reported as a structural match near $7000,\mathrm{km}$. The local certificate type bundles three cost axioms that any such match must satisfy before numerical comparison is meaningful.
The domain cost is the recognition cost specialized to mass/energy (or radius) pairs in this module. Its diagonal vanishing says equal arguments incur zero cost; non-negativity is the standard J-cost lower bound transferred to the domain. The upstream foundation result states: "The cost of any recognition event is non-negative," proved via Jcost_nonneg on positive states. The canonical threshold is the positive cutoff against which the white-dwarf scale is judged.
proof idea
One-line structure inhabitant. Field cost_at_eq is filled by the sibling lemma domainCost_at_eq; cost_nonneg by domainCost_nonneg (itself resting on the foundation non-negativity of J-cost); threshold_pos by canonicalThreshold_pos. No additional tactics or rewriting.
why it matters
Gives a zero-sorry, zero-axiom certificate object for RS Astrophysics Module 5, so downstream white-dwarf radius claims can assume the cost axioms by projecting fields rather than re-proving them. Status line of the module: STRUCTURAL THEOREM. No used_by edges are recorded yet; the inhabitant is the hand-off point for any later theorem that quotes the φ-ladder white-dwarf radius. Sits in the broader RS pattern where physical scales are forced on the φ-ladder once the cost functional (T5 J-uniqueness) and self-similar fixed point φ (T6) are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.