equation_of_state
plain-language theorem explainer
Fixes the dark-energy equation-of-state parameter at the integer value w = −1. Cosmologists citing the phase-saturation vacuum story use this constant when stating that vacuum energy density does not evolve with redshift. The body is a one-line definitional assignment, justified upstream by J(1) = 0 being tick-independent.
Claim. The vacuum equation-of-state parameter is the integer $w = -1$. Equivalently, pressure and energy density of the phase-saturated vacuum satisfy $p/\rho = -1$, so the vacuum energy density is constant in cosmic time.
background
In the Phase Saturation Vacuum module, dark energy is identified with the equilibrium fraction of the discrete ledger that sits in vacuum modes. That fraction is written $\Omega_\Lambda = 11/16 - \alpha/\pi$, coming from Q₃ mode counting minus an electromagnetic correction. The local claim is only about the equation of state of that vacuum piece, not about the numerical value of $\Omega_\Lambda$.
Recognition cost $J$ vanishes at the identity: $J(1) = 0$. Phase-locked vacuum modes therefore carry a tick-independent energy density. In continuum language that is a Lorentz-invariant constant contribution to the stress-energy tensor, $T_{\mu\nu} = -\rho, g_{\mu\nu}$, which forces $p = -\rho$.
The sibling module DarkEnergyEOS packages the same idea as a real-valued function on a ConstantEnergyContribution structure and proves $w = -1$ by dividing $-\rho/\rho$. The present definition is the integer constant used inside the phase-saturation development.
proof idea
Definitional, not a proof. The declaration simply assigns the integer literal $-1$. Downstream lemmas such as no_dark_energy_evolution recover the claim by rfl after introducing an unused redshift variable. The physical justification lives upstream: constant energy density implies $w = p/\rho = -1$ via the stress-energy argument in DarkEnergyEOS (w_eq_neg_one).
why it matters
Pins the RS prediction that dark energy does not evolve: $w(z) = -1$ at every redshift. Downstream, no_dark_energy_evolution is the universal quantification over redshift, w_is_minus_one is the local equality, and both PhaseSaturationVacuumCert and DarkEnergyEOSCert record $w = -1$ as a certificate field. That matches the continuum theorem that any constant energy contribution has equation of state exactly $-1$.
In the broader framework this is the EOS side of the cosmological-constant story: vacuum energy is a dimensionless mode fraction (order one), not a Planck-scale density needing $10^{120}$ cancellation. The module still treats the bridge from ledger saturation to cosmology as a named hypothesis (CosmicPhaseEquilibrium, vacuum_fraction_bridge); this definition only freezes the EOS once that vacuum piece is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.