cert_inhabited
plain-language theorem explainer
The ISM-dust-fraction cosmology certificate is inhabited: there exists a packaged witness that domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Cosmology auditors cite this to confirm Module 11 is structurally closed. The proof is a one-line term witness from the concrete certificate value.
Claim. The type of certificates for the ISM dust-fraction module is nonempty: there exists a record asserting that the domain cost $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
Module 11 packages the Recognition Science claim that the interstellar-medium dust fraction is $J(\varphi)^2\approx 1.39%$, matching the empirical $\sim 1%$ band. Status is structural: zero sorry, zero axioms.
The domain cost is the local cost functional on mass/energy-like pairs (imported from the Cost layer); its diagonal vanishing and nonnegativity are the usual J-cost sanity conditions. The canonical threshold is the positive cutoff used to mark the dust-fraction scale. The certificate structure bundles exactly those three propositions: diagonal cost zero, off-diagonal nonnegativity, and positive threshold.
proof idea
One-line term proof. The sibling value cert already inhabits the certificate structure, so the anonymous constructor ⟨cert⟩ supplies a witness for Nonempty RSCosmo011Cert. No tactics or further lemmas are required.
why it matters
Closes the structural side of Cosmology Module 11 (ISM dust fraction $J(\varphi)^2\sim 1%$). In the RS forcing chain the cost $J$ is the unique T5 solution of the Recognition Composition Law, and $\varphi$ is the T6 fixed point; squaring $J(\varphi)$ yields the dust-fraction scale packaged here. No downstream dependents are recorded yet; the declaration exists so later cosmology assembly theorems can assume the certificate type is inhabited without re-proving the three field identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.