darkEnergyEOSCert
plain-language theorem explainer
darkEnergyEOSCert assembles a certificate that the dark energy equation of state equals exactly -1 by bundling a phase-locked vacuum witness with the theorem that constant-energy contributions obey w = -1. Cosmologists working inside the Recognition Science ledger would cite the certificate when grounding w = -1 in J-cost properties rather than by definition. The construction is a direct structure instance that supplies the two required fields from vacuum_mode and dark_energy_w_derived.
Claim. Let DarkEnergyEOSCert be the structure asserting the existence of a phase-locked mode at ratio 1 (where the J-cost vanishes) together with the property that every constant energy contribution $c$ satisfies an equation of state equal to $-1$.
background
Phase-locked modes are recognition states whose ledger entries are committed and therefore do not update with additional ticks; their J-cost is tick-independent. The vacuum at ratio 1 satisfies J(1) = 0 by the unit property of the J-cost function. ConstantEnergyContribution denotes modes whose energy density remains fixed under expansion, while equation_of_state extracts the pressure-to-density ratio for such a mode.
proof idea
The definition is a one-line structure instance that directly assigns the vacuum_exists field from the vacuum_mode definition and the w_neg_one field from the dark_energy_w_derived theorem.
why it matters
This certificate supplies the derived w = -1 result required by the Recognition Science derivation of dark energy in Dark_Energy_Mode_Counting.tex §7.1, Theorem 7.1. It replaces an earlier definitional assignment with a theorem grounded in the phase-locking property and the J-cost vanishing at the vacuum, thereby closing the interface between the Wightman vacuum existence axiom and the cosmological equation of state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.