activeFraction
plain-language theorem explainer
The definition sets the active fraction of modes to one minus the passive fraction of phase-locked modes. Cosmologists using the Recognition Science vacuum model cite this partition when splitting the Q₃ mode budget into locked and unlocked contributions for uniform J-cost calculations. The construction is a direct algebraic complement with no lemmas or tactics applied.
Claim. Let $f_p = 11/16$ be the passive fraction of phase-locked modes. The active fraction is defined by $f_a := 1 - f_p$.
background
The VacuumUniformity module treats the ℤ³ lattice as a translation-invariant carrier with no distinguished voxels. Phase-locked modes act as committed ledger entries that incur zero maintenance J-cost, and their combinatorial fraction is fixed at 11/16 by the Q₃ budget, independent of location. This supplies the constant isotropic background term needed for the stress-energy identification of vacuum energy.
proof idea
One-line definition that subtracts the upstream passiveFraction value from 1.
why it matters
The definition supplies the unlocked complement required by the fractions_sum theorem and the VacuumUniformityCert structure. It completes the mode-budget partition that lets the module prove spatial uniformity of phase-locked J-cost across the carrier. In the framework this supports the structural claim that vacuum energy density is position-independent before any physical mapping is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.