RSAstro009Cert
plain-language theorem explainer
Certificate bundle for Astrophysics Module 9 (ISM dust fraction): diagonal domain-cost vanishes, domain-cost is nonnegative on positive mass/energy, and the canonical threshold is positive. Downstream code inhabits it to mark the module's structural claims as certified. Pure structure definition; no proof body.
Claim. A certificate is a triple of properties: (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 9 targets the ISM dust fraction claim $J(\varphi)^2 \approx 1.39%$ against the empirical $\sim 1%$ match, flagged as a structural theorem with no sorry and no axioms.
Domain cost is the module-local cost on a pair of positive reals (mass/energy style arguments). It sits on the Recognition Science $J$-cost $J(x)=(x+x^{-1})/2-1$, which is minimized at the identity ratio $x=1$. The upstream result cost_nonneg states that every recognition event has nonnegative cost, via nonnegativity of $J$ on positive states.
The three fields of this certificate are exactly the interface the module needs before it can exhibit a concrete witness: vanishing on the diagonal, global nonnegativity for positive inputs, and a positive threshold scale.
proof idea
No proof: this is a structure (Prop-valued field bundle). An inhabitant must supply proofs of the three fields. The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are the intended fillers; the downstream cert definition wires them in by named field assignment.
why it matters
Gives Module 9 a single named certificate type so the ISM dust-fraction structural package can be inhabited once and reused. Downstream cert builds a concrete value from the three sibling lemmas; cert_inhabited then records Nonempty of the certificate, closing the module's zero-sorry structural claim.
In the broader RS chain this sits under the $J$-cost uniqueness (T5) and the self-similar fixed point $\varphi$ (T6): the dust-fraction match is phrased as $J(\varphi)^2$ against the percent-level ISM observation. The certificate does not itself compute that number; it packages the cost/threshold hygiene the match depends on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.