ConstantEnergyContribution
plain-language theorem explainer
ConstantEnergyContribution encodes a positive real energy density that remains fixed across recognition ticks for phase-locked modes. Cosmologists working in the Recognition Science framework cite it when deriving the dark energy equation of state from J-cost ledger entries. The declaration is a pure structure definition whose three fields directly supply the input type for the downstream w = -1 theorem.
Claim. A structure consisting of a real number $ρ > 0$ (constant energy density) together with the assertion that this density is independent of tick count.
background
The module derives the dark energy equation of state w = -1 from phase-locked recognition modes whose J-cost is tick-independent. J-cost is the recognition cost function J(x) = (x + x^{-1})/2 - 1 supplied by PhiForcingDerived.of. The upstream theorem energy_pos from OscillatoryDynamicsDeep guarantees positivity of energy levels via multiplication of positive terms involving phi and omega. LedgerFactorization.of and SpectralEmergence.of supply the discrete tier structure and gauge content that place constant vacuum contributions at J(1) = 0.
proof idea
This is a structure definition with no proof body. The fields energy_density, energy_pos, and tick_independent directly encode the required properties of a constant contribution. No lemmas or tactics are invoked; the structure simply packages the data for use by equation_of_state and w_eq_neg_one.
why it matters
The structure supplies the hypothesis for DarkEnergyEOSCert and the theorem dark_energy_w_derived that establish w = -1 exactly. It implements the constant-energy case of Theorem 7.1 in Dark_Energy_Mode_Counting.tex by linking phase-locked modes to the thermodynamic relation ρ + p = 0. Within the forcing chain it sits downstream of T5 J-uniqueness and the eight-tick octave, providing the vacuum mode that yields the observed cosmological constant behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.