vacuumUniformityCert
plain-language theorem explainer
The declaration constructs the master certificate for vacuum uniformity by instantiating the structure that records the passive fraction of 11/16, the partition summing to one, positivity of phase-locked energy, and spatial invariance of that energy density. Cosmologists working with the Recognition Science vacuum model would cite it to justify an isotropic background J-cost on the lattice. The construction is a direct structure instance that delegates three fields to prior sibling theorems and uses reflexivity for the passive fraction.
Claim. The vacuum uniformity certificate is the structure consisting of passive fraction equal to $11/16$, passive fraction plus active fraction equal to $1$, phase-lock energy strictly positive, and the energy density function invariant under lattice translations.
background
The Vacuum Uniformity module shows that phase-locked modes on the integer lattice contribute a constant isotropic J-cost to every voxel. Passive fraction is the combinatorial share $11/16$ of committed ledger entries whose maintenance cost is zero; active fraction is its complement. PhaseLockEnergy is the product of that passive fraction with the coherent energy scale, and VoxelSymmetric asserts that a function on the lattice is unchanged by any translation.
proof idea
The definition builds the VacuumUniformityCert structure directly. The passive_frac field is filled by reflexivity. The fracs_sum, energy_pos, and uniform fields are supplied by the sibling theorems fractions_sum, vacuum_energy_pos, and vacuum_energy_uniform respectively.
why it matters
This definition supplies the canonical certificate that phase-locked vacuum modes produce spatially uniform energy density, closing the structural uniformity argument in the module. It implements the claim that vacuum J-cost is a constant background independent of position. The result sits between the phase-saturation vacuum model and any later identification with the cosmological constant term; the physical interpretation remains a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.