activeFraction
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the value 11/16 for the passive fraction.
- Does not map the numerical fraction to observed vacuum energy density.
- Does not address expansion dynamics or time dependence.
Lean usage
example : activeFraction = 5/16 := by unfold activeFraction; rw [passiveFraction]; norm_numformal statement (Lean)
35noncomputable def activeFraction : ℝ := 1 - passiveFraction
proof body
Definition body.
36