w_is_minus_one
plain-language theorem explainer
The phase-saturation vacuum has equation-of-state parameter exactly equal to -1, with no redshift dependence. Anyone assembling the RS dark-energy package (Ω_Λ from ledger saturation) cites this to lock w to the cosmological-constant value. The proof is pure reflexivity: the local definition already sets the parameter to -1.
Claim. The equation-of-state parameter of the phase-saturation vacuum equals $-1$: $w = -1$.
background
This module treats dark energy as the equilibrium vacuum fraction of a finite discrete ledger under phase saturation. The target fraction is $\Omega_\Lambda = 11/16 - \alpha/\pi$, read off from Q$_3$ mode counting minus the fine-structure correction.
In the companion DarkEnergyEOS development, any constant energy contribution has $w = p/\rho = -\rho/\rho = -1$. Here the same conclusion is specialized to the vacuum: the recognition cost $J(1) = 0$ is tick-independent, so the vacuum energy density does not evolve with cosmic time. The local equation_of_state is therefore the integer constant $-1$, not a redshift-dependent function.
The surrounding chain still leaves the bridge from ledger saturation to cosmology as an explicit hypothesis (CosmicPhaseEquilibrium, vacuum_fraction_bridge); the $w = -1$ fact itself is definitional once constancy of the vacuum density is granted.
proof idea
One-line term proof by rfl. The local definition sets the equation-of-state parameter to the integer $-1$, so equality to $-1$ is definitional reduction. No lemmas are unfolded beyond that definition; the upstream constant-energy $w = -1$ argument in DarkEnergyEOS supplies the physical reading but is not invoked in the term.
why it matters
Locks the vacuum sector of the phase-saturation story to a pure cosmological constant: no dark-energy evolution, $w(z) = -1$ at every redshift. Downstream, phase_saturation_vacuum_cert packages the $\Omega_\Lambda$ bounds, mode partition, and closure facts; this theorem supplies the EOS half of that certificate's physical interpretation.
Within the broader RS forcing chain it sits downstream of J-uniqueness ($J(1) = 0$) and the eight-tick discrete ledger: a tick-independent vacuum cost is exactly what forces constant vacuum density. It does not close the still-open hypotheses that identify ledger passive-mode fraction with cosmic $\Omega_\Lambda$, but it removes any freedom to put evolving $w$ into the vacuum once that identification is made.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.