EOSDeep4Cert
plain-language theorem explainer
Packages three Prop fields that a cosmology certificate must satisfy: domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Cosmology proofs that need a single inhabited certificate type cite this structure. It is a pure data definition; the fields are discharged later by sibling lemmas.
Claim. An EOS deep-4 certificate is a record of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module is RS Cosmology (session 3), marked as a structural theorem with zero sorry and zero axioms. Its headline claim is that the dark-energy equation-of-state parameter satisfies $w=-1$ exactly from the RS vacuum; a DESI Y3 deviation from $w=-1$ at $2\sigma$ would falsify the framework.
Domain cost is the local cost functional on mass/energy pairs used in this file (siblings domainCost, domainCost_at_eq, domainCost_nonneg). It inherits nonnegativity from the foundation J-cost: upstream cost_nonneg states that every recognition event has nonnegative cost via Jcost_nonneg. The canonical threshold is a positive real cutoff (sibling canonicalThreshold / canonicalThreshold_pos) against which vacuum or EOS comparisons are made.
This structure does not compute cosmology observables; it only names the three inequalities a certificate must carry.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (cost_at_eq, cost_nonneg, threshold_pos). Inhabitation is supplied downstream by cert, which fills the fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and by cert_inhabited, which wraps that instance as Nonempty.
why it matters
Gives the cosmology layer a single named certificate type so later EOS arguments can assume one object rather than three loose lemmas. Downstream cert builds a concrete instance; cert_inhabited records that the type is nonempty. That inhabitation is the structural hook for the module claim that $w=-1$ follows from the RS vacuum (module status: structural theorem, 0 sorry). Ties to foundation cost nonnegativity (J-cost minimum at the identity event) rather than to the T0–T8 forcing chain directly. Any future EOS or vacuum lemma in this file that needs a certified cost/threshold package will take an EOSDeep4Cert (or use cert).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.