cert
plain-language theorem explainer
Packages the three structural properties of the ISM-dust domain cost into a single certificate: zero cost on the diagonal, non-negativity off-diagonal, and a strictly positive canonical threshold. Astrophysicists citing the J(φ)² ≈ 1.39% dust-fraction match use this as the formal witness that the cost model is well-posed. The definition is a pure structure inhabitant wiring three already-proved lemmas.
Claim. There exists a certificate recording that the ISM-dust domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and the canonical threshold $T$ obeys $T>0$.
background
Module 9 of the RS astrophysics stack treats the interstellar-medium dust fraction as a recognition-cost prediction. The empirical target is roughly one percent; the RS claim is $J(\varphi)^2\approx 1.39%$, where $J(x)=(x+x^{-1})/2-1$ is the unique cost functional forced by the Recognition Composition Law (T5).
The local cost is a two-argument domain cost $C(m,e)$ on positive reals (mass and energy scales, or analogous ratio variables). A well-posed cost must vanish on the diagonal $m=e$, stay non-negative off it, and sit below a positive threshold that marks the dust-fraction band. Those three properties are exactly the fields of the structure RSAstro009Cert.
Upstream, non-negativity of recognition cost is already known from ObserverForcing: every recognition event has $J$-cost $\ge 0$ because $J$ itself is non-negative on $(0,\infty)$. The module specializes that fact to the dust domain cost and adds the diagonal and threshold lemmas.
proof idea
One-line structure inhabitant. 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 additional tactic work; the definition simply assembles those proofs into the certificate record.
why it matters
Gives the formal MATCH witness for the ISM dust fraction $J(\varphi)^2\approx 1.39%$ against the empirical $\sim 1%$ band. In the RS forcing chain this sits downstream of T5 ($J$-uniqueness) and T6 ($\varphi$ as self-similar fixed point): the numerical value is forced once $J$ and $\varphi$ are fixed, and the certificate guarantees the cost model used to state that value is mathematically coherent (zero on match, non-negative, positive threshold).
The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom). No downstream consumers are wired yet in the graph; the certificate is the export surface for any later astrophysics aggregation that needs a single named proof object for Module 9.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.