VacuumUniformityCert
plain-language theorem explainer
VacuumUniformityCert packages the uniformity properties of phase-locked vacuum energy on the ℤ³ carrier. Cosmologists deriving an isotropic stress-energy tensor from phase saturation would cite this certificate when closing the bridge to T_μν^vac. The structure is assembled directly from the passiveFraction definition, the fractions_sum lemma, a positivity result, and the VoxelSymmetric invariance axiom.
Claim. The master certificate asserts that the passive fraction of phase-locked modes equals $11/16$, that this fraction plus the active fraction sums to 1, that the phase-locked energy density is strictly positive, and that the energy density function is invariant under all translations on the integer lattice.
background
The Vacuum Uniformity module shows that phase-locked modes contribute a constant isotropic J-cost background to every voxel on the ℤ³ carrier. passiveFraction is defined as the combinatorial fraction 11/16 drawn from the Q₃ mode budget; activeFraction is its complement 1 minus that value. phaseLockEnergy is then defined as passiveFraction times the coherence energy E_coh. VoxelSymmetric is the structure whose single field shift_invariant requires that any function f : ℤ³ → ℝ satisfies f(v + d) = f(v) for all lattice vectors d, encoding translation invariance of the carrier.
proof idea
This is a structure definition whose four fields are populated downstream. The construction in vacuumUniformityCert supplies rfl for the passive fraction equality, the fractions_sum lemma for the sum-to-one property, the vacuum_energy_pos theorem for positivity, and the vacuum_energy_uniform result for the VoxelSymmetric invariance.
why it matters
The certificate supplies the structural uniformity needed to identify vacuum energy density with a constant isotropic background J-cost. It is instantiated by the downstream vacuumUniformityCert definition. The module document states that the result proves phase-locked modes contribute a constant, isotropic background J-cost to every voxel, thereby supporting spatial uniformity of the vacuum energy density. It touches the open identification of this density with the observed cosmological constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.