passiveFraction
plain-language theorem explainer
The declaration supplies the constant fraction 11/16 of phase-locked modes drawn from the Q₃ budget. Cosmologists working in the Recognition Science setting cite the value when constructing the isotropic vacuum energy density per voxel. The definition consists of a direct numerical assignment with no lemmas or computation required.
Claim. The passive fraction of phase-locked modes from the Q₃ mode budget is defined as $11/16$.
background
The Vacuum Uniformity module shows that phase-locked modes on the ℤ³ carrier contribute a constant J-cost background. These modes are committed ledger entries whose maintenance cost vanishes under the J-function. The module invokes VoxelSymmetry to guarantee that the combinatorial fraction of such modes is the same at every lattice point, yielding a spatially uniform vacuum energy density.
proof idea
The declaration is a direct definition that assigns the rational constant 11/16. No lemmas are invoked and no tactics are applied.
why it matters
This definition supplies the numerical input to phaseLockEnergy and to the uniformity theorem vacuum_energy_uniform, which asserts VoxelSymmetric (fun _ => phaseLockEnergy). It realizes the combinatorial step in the module argument that the fraction is independent of position. The same 11/16 appears in the bridge from PhaseSaturationVacuum to the stress-energy tensor T_μν^vac.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.