PhaseLocked
plain-language theorem explainer
PhaseLocked defines a structure for a real ratio fixed at 1 whose J-cost vanishes. Cosmologists deriving dark energy from Recognition Science cite it to anchor tick-independent vacuum energy density. The definition is a direct three-field structure that encodes the vacuum ledger entry at x=1.
Claim. A phase-locked mode is a real number $r$ such that $r=1$ and $J(r)=0$, where $J$ is the recognition cost function.
background
The module derives $w=-1$ for dark energy from phase-locked recognition modes whose ledger entries are committed and do not update. J-cost is the recognition cost function satisfying $J(1)=0$ by the upstream Jcost_unit0 lemma; the 8-tick phase space (Phase := Fin 8) supplies the underlying cycle from the EightTick and ChurchTuringPhysicsStructure imports. Upstream, modes supplies the finite set of truncated 2D modes while has encodes spectral peaks ranked by phi-rung.
proof idea
This is a structure definition whose three fields directly encode the vacuum condition: ratio of type real, at_vacuum asserting equality to 1, and cost_zero asserting Jcost ratio = 0. No tactics or lemmas are applied beyond the field assertions.
why it matters
PhaseLocked supplies the vacuum_exists field to DarkEnergyEOSCert, which in turn proves dark_energy_w_derived that equation_of_state c = -1 for any ConstantEnergyContribution. It fills Theorem 7.1 of Dark_Energy_Mode_Counting.tex §7.1 and supports the constant-energy contribution required for w=-1 in the Recognition framework, consistent with the eight-tick octave and phase locking at the vacuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.