cert
plain-language theorem explainer
Packages three structural properties of the neutron-star domain cost into one certificate: cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cited by anyone checking the RS neutron-star radius claim (φ⁵ km ≈ 11.09 km in the 10–13 km band). Pure record assembly of three already-proved lemmas; no new mathematics.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(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
Astrophysics RS Module 3 targets the neutron-star radius prediction $\phi^5,\mathrm{km}\approx 11.09,\mathrm{km}$, which sits inside the observational 10–13 km window. The module status is structural theorem (zero sorry, zero axiom).
The domain cost is the local cost functional comparing a model value $m$ to an observational value $e$. Its diagonal vanishing and nonnegativity are the minimal sanity conditions any RS cost must satisfy; they descend from the global J-cost nonnegativity theorem in ObserverForcing ("the cost of any recognition event is non-negative").
The certificate structure RSAstro003Cert is the module's interface object: three propositions that must hold before the radius match is treated as certified. The canonical threshold is the positive cutoff against which the cost is compared.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No tactics, no rewriting; pure record construction.
why it matters
This is the inhabited certificate for Module 3's neutron-star radius claim. Downstream consumers (none yet wired in the graph) would require an RSAstro003Cert witness before treating $\phi^5,\mathrm{km}$ as a certified match. It sits in the astrophysics layer that applies the forcing-chain constants ($\phi$ from T6, the J-cost from T5) to concrete stellar observables. Closes the structural side of the module; the numerical MATCH claim in the module doc is the scientific payload this certificate underwrites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.