cert
plain-language theorem explainer
Packages a certificate that domain cost vanishes on equal nonzero ratios, is nonnegative for positive mass-energy pairs, and that the canonical threshold is strictly positive. Cosmologists tracing the RS derivation of Omega_m from J-cost cite this as the inhabited witness. Construction is a three-field structure instance wiring sibling lemmas; no new algebra.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ equals zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module targets the matter density parameter from J-cost (Plan v7, 117th pass). Status is structural: zero sorry, zero axiom. The Planck 2018 value Omega_m ~ 0.315 is recalled; RS writes Omega_m = 1 - Omega_Lambda with a phi-ladder expression, and notes a structural ratio Omega_m / Omega_Lambda = (D+1)/(D-1) = 2 when D = 3.
Domain cost is the local cost functional on mass-energy pairs used in that derivation. The certificate structure bundles three elementary properties of that cost and of a positive canonical threshold: diagonal vanishing, nonnegativity off the identity, and threshold positivity. Upstream, nonnegativity of recognition cost is the standard J-cost fact that any recognition event has cost at least zero (Jcost_nonneg on a positive state).
proof idea
One-line structure instance. The three fields 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 beyond field assignment; no new proof obligations.
why it matters
Gives an inhabited certificate object for the Omega_m-from-J-cost structural package. The module frames Omega_m as forced by J-cost geometry once D = 3 is fixed (forcing chain T8), with the ratio (D+1)/(D-1) = 2 tying matter to vacuum density. No downstream consumers are recorded yet; the witness exists so later cosmology lemmas can assume the three cost/threshold facts by projecting fields rather than re-proving them. Touches the structural (not numerical) half of the Omega_m claim: the module itself flags that naive RS-unit arithmetic does not yet match the physical sign/scale without a units bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.