RSAstro003Cert
plain-language theorem explainer
Certificate packing three structural properties for the neutron-star radius module: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is positive. Downstream code cites it via the concrete inhabitant `cert` and the Nonempty proof. Pure structure definition with no proof body.
Claim. A certificate is a triple of facts: (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
Module 3 of the RS astrophysics layer targets the neutron-star radius prediction $\phi^5,\mathrm{km}\approx 11.09,\mathrm{km}$ (observational band $10$–$13,\mathrm{km}$), marked MATCH and statused as a structural theorem with zero sorry and zero axiom.
The certificate talks about a domain-specific cost functional (sibling domainCost) on pairs of positive reals, together with a positive scalar threshold (sibling canonicalThreshold). The diagonal-vanishing and nonnegativity fields mirror the global recognition-cost axioms: upstream, cost_nonneg states that every recognition event has nonnegative cost, via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$.
Locally the module only needs the restricted cost to be a genuine cost (zero on matched arguments, nonnegative off-diagonal) and the threshold that will later gate the radius claim to be positive.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that inhabitant.
why it matters
Gives the typed interface that Module 3 must satisfy before the neutron-star radius match is treated as certified. Downstream, cert builds a concrete value of this structure, and cert_inhabited records Nonempty RSAstro003Cert, closing the module's structural obligation.
In the broader RS chain the radius yardstick is the forced constant $Z_{\mathrm{cf}}=\phi^5\in(11,12)$ (primer landmark), here read in kilometres. The certificate does not itself derive $\phi$ or $D=3$; it only packages the cost/threshold hygiene that lets the astrophysics layer claim a clean MATCH against the $10$–$13,\mathrm{km}$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.