dark_energy_w_derived
plain-language theorem explainer
The result establishes that every constant energy contribution has equation of state parameter exactly -1. Cosmologists using the phase-locked recognition framework cite it to replace a prior definition of w with a derived theorem. The proof is a one-line application of the upstream lemma that unfolds the equation_of_state definition and cancels the positive density term.
Claim. For any constant energy contribution $c$ with positive tick-independent energy density, the equation of state parameter satisfies $w(c) = -1$.
background
A ConstantEnergyContribution is a structure carrying a positive real energy density that does not change with tick count. The equation_of_state function on such a contribution returns -energy_density divided by energy_density. The module derives the dark energy equation of state from phase-locked recognition modes whose J-cost vanishes at the fixed point x=1, producing constant energy density and therefore p = -ρ. The upstream lemma w_eq_neg_one proves the same identity by unfolding the definition and applying div_self on the positive density.
proof idea
The proof is a one-line wrapper that applies the lemma w_eq_neg_one.
why it matters
This theorem supplies the w_neg_one field of the DarkEnergyEOSCert certificate. It corresponds to Theorem 7.1 in Dark_Energy_Mode_Counting.tex §7.1 and closes the derivation that phase-locked vacuum modes produce w = -1. The result sits inside the Recognition Science forcing chain at the point where constant J-cost at x=1 forces the observed dark energy behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.