RSAstro007Cert
plain-language theorem explainer
Certificate bundle for the stellar-metallicity astrophysics module: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code cites it to witness that the module is inhabited. Pure structure definition with no proof body; fields are filled by sibling lemmas.
Claim. A certificate for RS astrophysics module 7 is a triple of facts: for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Module 7 is the stellar-metallicity layer of the RS astrophysics stack. Its headline match is $J(\varphi)^2 \approx 0.0139 \sim Z_\odot = 0.014$, recorded as a structural theorem (zero sorry, zero axiom). Here $J$ is the unique cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law.
The domain cost is the local cost functional on pairs of positive reals used in this module (mass/energy or ratio arguments). The canonical threshold is the positive cutoff against which metallicity-scale quantities are compared. Upstream, recognition-event costs are already known to be nonnegative via $J$-cost nonnegativity on positive states.
proof idea
No proof body: this is a structure packing three Prop fields. Inhabitation is discharged downstream by the definition cert, which assigns the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields. The theorem cert_inhabited then wraps that witness as Nonempty.
why it matters
Gives a single typed handle for the three structural obligations of the metallicity module so that cert and cert_inhabited can assert the module is fully certified. That certification underwrites the claimed match $J(\varphi)^2 \sim Z_\odot$ inside the Recognition Science astrophysics layer, tying the golden-ratio fixed point $\varphi$ (forcing step T6) and the unique $J$-cost (T5) to a solar-metallicity scale. It does not itself compute the numerical match; it packages the cost and threshold facts the match rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.