Pith. sign in
module module high

IndisputableMonolith.Cosmology.DarkEnergyEOS

show as:
view Lean formalization →

The Cosmology.DarkEnergyEOS module defines phase-locked modes with zero J-cost at x=1, yielding constant energy contributions and the dark energy equation of state w=-1. Cosmologists working within Recognition Science would cite these definitions for vacuum energy modeling. The module consists of a sequence of definitions and algebraic derivations with no proofs required.

claimA phase-locked mode at $x=1$ satisfies $J(1)=0$ with J-cost independent of tick counter, producing constant energy contribution and dark energy equation of state $w=-1$.

background

The module imports the Cost module, which supplies the J-cost function measuring recognition cost via the Recognition Composition Law. It introduces PhaseLocked as a mode with committed ledger entry at x=1, so that J-cost is zero and does not vary with the tick counter. Additional definitions cover vacuum_mode, phase_locked_energy_constant, ConstantEnergyContribution, equation_of_state, w_eq_neg_one, and dark_energy_w_derived.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the dark energy equation of state w=-1 from phase-locked modes with zero J-cost, supporting cosmology derivations in the Recognition Science framework and linking to the J-uniqueness step in the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)