cert
plain-language theorem explainer
Packages three elementary J-cost facts into a single dark-energy equation-of-state certificate: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cosmologists citing the RS claim that w = −1 is the J-cost ground state use this bundle. The definition is a pure structure inhabitant wiring three already-proved lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive. Together these certify the structural $w=-1$ ground-state claim for the dark-energy equation of state from $J$-cost.
background
The module treats the dark-energy equation of state as a $J$-cost statement. In Recognition Science the cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain. The module doc records the structural claim $w=-1$ (cosmological constant): $J(\rho_{\mathrm{DE}}/\rho_{\mathrm{crit}})=J(\phi^5/45)=J(\Omega_\Lambda)$, and at $\Omega_\Lambda=0.68$ one has $J(1)=0$, the $J$-minimum.
domainCost is the local cost comparison used for the equation-of-state certificate; its diagonal vanishing and nonnegativity are the algebraic content of a pure ground state. The upstream fact cost_nonneg from ObserverForcing states that every recognition event has nonnegative cost, via Jcost_nonneg at positive state. The canonical threshold is the positive scale against which the cost comparison is judged.
proof idea
One-line structure inhabitant. The three fields of DEoS3Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass/energy arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further tactic work; the definition is pure packaging.
why it matters
This certificate is the exportable witness that the dark-energy equation-of-state module is a structural theorem (zero sorry, zero axiom) rather than a numerical fit. It anchors the RS reading that $w=-1$ is exactly the $J$-cost ground state at ratio one, consistent with T5 $J$-uniqueness and the $\phi$-ladder constants ($\phi^5$ appears in the $\Omega_\Lambda$ identification). No downstream consumers are recorded yet; the sibling cert_inhabited is the immediate inhabitation check. The declaration closes the certificate interface for Plan v7 pass 115 without adding new physics hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.