vacuum_energy_pos
plain-language theorem explainer
The phase-locked vacuum energy per voxel is strictly positive. Cosmologists using Recognition Science to model the vacuum contribution to the stress-energy tensor would cite this when establishing that the J-cost background is non-zero. The proof is a one-line term wrapper that unfolds the definition of phaseLockEnergy and applies the product-positivity lemma to two already-proved positive quantities.
Claim. The phase-locked vacuum energy density, defined as the product of the passive fraction of modes and the coherent energy scale $E_0$, satisfies $E_0 > 0$.
background
The VacuumUniformity module proves that phase-locked modes contribute a constant, isotropic J-cost to every voxel of the ℤ³ carrier. Key definitions are the passive fraction (a combinatorial constant proved positive by norm_num) and the coherent energy scale $E_0$ (positive by the forcing-chain result $E_0 = c^{-5} > 0$). The module setting is that the vacuum energy density is spatially uniform because the fraction of phase-locked modes is independent of position under VoxelSymmetry.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition phaseLockEnergy := passiveFraction * E_coh and applies the lemma mul_pos to the upstream facts passive_fraction_pos and E_coh_pos.
why it matters
This theorem supplies the energy_pos field of the master certificate vacuumUniformityCert. It completes the structural half of the argument that vacuum energy density is spatially uniform, as stated in the module documentation, and supports the identification of the vacuum term in Ω_Λ with the phase-locked fraction inside the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.