OmegaMatter3Cert
plain-language theorem explainer
Certificate bundling three structural facts used to derive the matter density parameter from J-cost geometry: diagonal vanishing of domain cost, nonnegativity for positive mass/energy arguments, and positivity of the canonical threshold. Cosmology proofs that close Ω_m from recognition cost cite this interface. Pure structure definition; inhabitation is supplied separately by wiring the sibling lemmas.
Claim. An $\Omega_m$-from-$J$ certificate is a triple of statements: (i) domain cost vanishes on the diagonal, $C(r,r)=0$ for every $r\neq 0$; (ii) domain cost is nonnegative on the positive quadrant, $C(m,e)\geq 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
The module targets the Planck 2018 matter density $\Omega_m\approx 0.315$ as a structural consequence of J-cost geometry rather than a free fit. In RS units the companion dark-energy fraction is written $\Omega_\Lambda=8\varphi^5/45$, and the ratio identity $\Omega_m/\Omega_\Lambda=(D+1)/(D-1)=2$ (with $D=3$) is the intended structural relation; raw numerical substitution still mixes RS and SI units, so the module isolates the cost hypotheses first.
Domain cost $C(m,e)$ is the two-argument cost used on mass/energy pairs in this cosmology layer. It is built from the recognition cost $J$, whose uniqueness ($J(x)=(x+x^{-1})/2-1$) is forced upstream (T5). The classical nonnegativity fact "the cost of any recognition event is non-negative" (ObserverForcing.cost_nonneg, via $J\geq 0$ for positive states) is the template for the two-variable inequality packaged here.
The canonical threshold is the positive cutoff against which domain-cost comparisons are made when separating matter-like from vacuum-like contributions.
proof idea
No proof body: the declaration is a structure with three Prop fields. Inhabitation is external. The downstream definition cert fills the fields by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (positivity on $m,e>0$), and canonicalThreshold_pos. The theorem cert_inhabited then packages ⟨cert⟩ as Nonempty OmegaMatter3Cert.
why it matters
Gives the cosmology layer a named, reusable hypothesis bundle so later Ω_m arguments do not restate cost axioms inline. Downstream, cert and cert_inhabited discharge the interface and prove the certificate type is inhabited, which is the structural-theorem status claimed in the module header (0 sorry, 0 axiom).
Framework landmarks in play: T5 J-uniqueness (the cost whose nonnegativity and diagonal minimum seed domainCost), T6 φ (enters the explicit Ω_Λ formula $8\varphi^5/45$), and T8 $D=3$ (forces the ratio $(D+1)/(D-1)=2$). The module still flags the sign/units mismatch between the RS algebraic expression and the physical Ω_m band; this certificate deliberately stops at the cost hypotheses and does not close that numerical gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.