cert
plain-language theorem explainer
Packages three structural facts (diagonal vanishing of domain cost, nonnegativity, positive canonical threshold) into the Module-011 certificate for the ISM dust fraction. Cosmologists citing the RS claim J(φ)² ≈ 1.39% (~1% empirical) point here as the Lean witness bundle. Proof shape: pure structure inhabitant wiring three local lemmas; no new mathematics.
Claim. There is a certificate whose fields assert: (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 RS_Cosmo_011 treats the interstellar-medium (ISM) dust fraction in Recognition Science. The module headline is the structural identity $J(\varphi)^2 \approx 1.39%$, read as matching the empirical ~1% dust fraction, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The underlying cost is the RS J-functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique at T5 of the unified forcing chain. Here domainCost is the module-local cost on a pair of positive reals (mass/energy-style arguments); its diagonal vanishes and it stays nonnegative. canonicalThreshold is the positive cutoff against which the dust-fraction comparison is staged.
Upstream, nonnegativity of recognition cost is the general fact that every recognition event has $0 \le$ cost, proved from $J$-cost nonnegativity on positive states. The certificate structure simply names the three props the module needs in one place.
proof idea
One-line structure construction. The three fields of RSCosmo011Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No tactics, no rewriting: pure field assignment of already-proved local facts. The upstream cost_nonneg theorem from ObserverForcing is the conceptual ancestor of the nonnegativity field, specialized here to domainCost.
why it matters
This is the inhabitance witness for Cosmology Module 011's certificate type. The module's scientific claim is the ISM dust-fraction match $J(\varphi)^2 = 1.39% \sim 1%$ empirical; the certificate packages the cost-calculus side conditions that make that comparison well-posed (cost zero on matched arguments, cost never negative, threshold above zero).
In the broader RS stack it sits downstream of T5 J-uniqueness and the φ fixed point (T6), since the numerical dust fraction is built from $J(\varphi)$. No further used_by edges are recorded yet; the natural consumer is any top-level cosmology audit or cert_inhabited-style nonemptiness lemma that needs a single term of type RSCosmo011Cert. It closes no open sorry; it is the clean packaging step for an already-sorry-free structural module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.