w_eq_neg_one
plain-language theorem explainer
Constant energy contributions in the Recognition ledger satisfy an equation of state parameter of exactly -1. Cosmologists modeling dark energy would cite this to ground w = -1 in phase-locked J-cost rather than postulate it. The proof is a direct algebraic reduction from the definition of equation_of_state using energy positivity.
Claim. For any constant energy contribution $c$ with positive energy density, the equation of state parameter satisfies $w(c) = -1$.
background
The module replaces a prior definitional assignment of w := -1 with a theorem derived from phase-locked recognition modes. A ConstantEnergyContribution is a structure holding a positive energy density that remains tick-independent. The equation_of_state is defined as the ratio -energy_density / energy_density, which encodes the thermodynamic relation dE = -p dV for constant E implying p = -ρ.
proof idea
The proof is a term-mode reduction. It unfolds the definition of equation_of_state and rewrites using neg_div together with div_self applied to the positive energy density supplied by the structure.
why it matters
This theorem supplies the core identity used by dark_energy_w_derived to establish the equation of state for all such contributions. It realizes Theorem 7.1 in Dark_Energy_Mode_Counting.tex §7.1 by deriving w = -1 from J(1) = 0 under phase locking. In the framework it connects to T5 J-uniqueness and the eight-tick octave, confirming that spatially uniform, temporally constant energy density implies w = -1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.