cert_inhabited
plain-language theorem explainer
The fourth-pass matter-perturbation certificate is inhabited: a single witness packs diagonal vanishing of the domain cost, off-diagonal nonnegativity, and positivity of the canonical threshold. Anyone citing the CMB anisotropy structural package (J-cost v4) needs this existence fact. The proof is a one-line term that introduces the already-built certificate constructor.
Claim. The type of certificates for the fourth-pass matter-perturbation cost model is nonempty: there exists a bundle asserting (i) the domain cost vanishes on the diagonal for every nonzero real ratio, (ii) the domain cost is nonnegative for positive mass and energy parameters, and (iii) the canonical threshold is strictly positive.
background
The module packages a structural theorem for CMB temperature anisotropy from the Recognition Science J-cost. Observed $\Delta T/T\sim 10^{-5}$ is compared with the RS estimate $J(\varphi)^{D+1}=J(\varphi)^4\approx 1.94\times 10^{-4}$, an order-of-magnitude match once $D=3$ is fixed by the forcing chain.
domainCost is the local cost functional on mass/energy (or ratio) pairs used in this pass; the certificate demands it vanish when the two arguments coincide (nonzero) and stay nonnegative when both are positive. canonicalThreshold is the positive cutoff against which that cost is compared. The structure MatterPert4Cert is exactly the triple of those three propositions; no dynamical evolution is encoded here.
proof idea
Term-mode one-liner. The sibling value cert already assembles a concrete MatterPert4Cert (its three fields are the proved lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos). The proof is the anonymous constructor ⟨cert⟩, which is the standard inhabitant of Nonempty MatterPert4Cert.
why it matters
This is the inhabitation gate for the CMB anisotropy structural package in Cosmology.MatterPert4. Downstream consumers that require a MatterPert4Cert (or that pattern-match on Nonempty to obtain one) can discharge the existence obligation in a single step. Within the Recognition framework it sits under the J-cost cosmology line: T5 forces $J(x)=(x+x^{-1})/2-1$, T6 forces $\varphi$, T8 forces $D=3$, and the module records $J(\varphi)^4\sim 2\times 10^{-4}$ against the observed $10^{-5}$ band. The declaration itself is pure scaffolding hygiene (0 sorry, 0 axiom); it does not close the quantitative gap between $2\times 10^{-4}$ and $10^{-5}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.