phaseLockEnergy
Phase-locked energy density is defined as the product of the passive mode fraction (11/16) and the coherent energy E_coh. Cosmologists working on vacuum uniformity in the Recognition Science framework cite this when constructing the constant isotropic contribution to the stress-energy tensor. The definition is a direct product that inherits its properties from the upstream passiveFraction and E_coh factors.
claimThe phase-locked energy density equals the passive fraction of modes times the coherent energy scale, or equivalently (11/16) E_coh.
background
The Vacuum Uniformity module shows that phase-locked modes are committed ledger entries carrying zero maintenance cost under J(1) = 0. The passiveFraction definition supplies the combinatorial share 11/16 of such modes from the Q3 budget, independent of position. This declaration multiplies that fraction by E_coh to produce the constant J-cost per voxel that enters the stress-energy tensor T_μν^vac.
proof idea
The declaration is a direct definition that multiplies passiveFraction by E_coh. No lemmas or tactics are invoked; it is an immediate abbreviation.
why it matters in Recognition Science
This definition supplies the constant value used by vacuum_energy_uniform (which asserts VoxelSymmetric (fun _ => phaseLockEnergy)) and by the master certificate VacuumUniformityCert. It realizes the structural uniformity step that bridges PhaseSaturationVacuum to the vacuum stress-energy tensor, consistent with VoxelSymmetry and the position-independent Q3 fraction.
scope and limits
- Does not compute a numerical value for E_coh.
- Does not prove positivity of the result; that is supplied by separate lemmas on the factors.
- Does not address contributions from active modes.
- Does not derive the fraction 11/16; that is taken from passiveFraction.
formal statement (Lean)
46noncomputable def phaseLockEnergy : ℝ := passiveFraction * E_coh
proof body
Definition body.
47
48/-- The vacuum energy density function is spatially uniform. -/