RSCosmo011Cert
plain-language theorem explainer
Certificate structure for Cosmology Module 11 (ISM dust fraction) packing three interface facts: diagonal vanishing of the domain cost, non-negativity of that cost on positive arguments, and positivity of the canonical threshold. Downstream cert and cert_inhabited inhabit it. Pure structure definition with no proof body; the three fields are filled by sibling lemmas.
Claim. A certificate is a triple of claims: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Module 11 of the RS cosmology stack treats the ISM dust fraction. The module doc records the structural match $J(\phi)^2\approx 1.39%$ against the empirical $\sim 1%$ level, with status structural theorem (zero sorry, zero axiom).
The domain cost $C$ is the local real-valued cost on mass/energy-like arguments used in this module; the diagonal identity $C(r,r)=0$ for $r\neq 0$ is the on-shell vanishing condition. The canonical threshold is the positive cutoff against which the dust-fraction comparison is staged. Upstream, ObserverForcing proves that the cost of any recognition event is non-negative, via non-negativity of the $J$-cost on positive states; the module field is the analogous statement for $C$.
proof idea
Structure definition only: no tactics, no lemmas applied at this declaration. It declares the Prop-typed fields a valid certificate must carry. The concrete witness cert fills them by assigning the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Inhabitation is then immediate from that witness.
why it matters
Gives the typed bundle for Cosmology Module 11 so later audits can require one certificate rather than three loose lemmas. Downstream, cert assembles the siblings into an RSCosmo011Cert value, and cert_inhabited records Nonempty of that type, closing the module as a structural theorem. The scientific content is the ISM dust fraction match $J(\phi)^2\sim 1%$, which sits on the forcing chain via T5 ($J$-uniqueness) and T6 ($\phi$ as self-similar fixed point). No open scaffold remains at this node; the structure is the interface, not a sorry-bearing stub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.