cert
plain-language theorem explainer
Packages the three field proofs that certify the stellar-metallicity domain cost: it vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is positive. Anyone citing the Module-7 metallicity match (J(φ)² ≈ Z_⊙) needs this inhabited certificate. Construction is a structure instance that wires three sibling lemmas.
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
Module 7 of the RS astrophysics layer targets stellar metallicity. The structural claim is that $J(\varphi)^2 \approx 0.0139$ matches the solar metallicity $Z_\odot \approx 0.014$. Status is a structural theorem (no sorry, no axioms).
The domain cost is the local cost functional comparing a model value to an empirical value in this metallicity setting. The certificate structure RSAstro007Cert packages three elementary properties any such cost must satisfy before the numerical match is trusted: vanishing when model equals data, non-negativity off the diagonal, and a positive decision threshold.
Upstream, non-negativity of recognition cost is already forced in the observer layer: every recognition event has cost $\ge 0$ because $J$ itself is non-negative on the positive reals. The module imports that fact and the global constants ($\varphi$, $J$).
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site; the def only assembles those proofs into the certificate record.
why it matters
Gives the inhabited certificate that Module 7 is well-formed as a cost-based match. Downstream consumers (none listed yet in the graph) can assume the metallicity cost is a genuine non-negative defect with a positive threshold, so the numerical claim $J(\varphi)^2 \sim Z_\odot$ sits on a certified cost rather than an ad-hoc residual.
In the broader RS chain this sits downstream of T5 ($J$-uniqueness) and the global non-negativity of $J$-cost. It does not itself derive the metallicity number; it only locks the cost axioms that make the reported MATCH meaningful as a structural theorem rather than a floating fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.