fractions_sum
plain-language theorem explainer
The theorem establishes that the passive fraction of phase-locked modes plus its complementary active fraction sums to one. Cosmologists using the Recognition Science framework cite this identity when certifying that vacuum energy density remains spatially uniform across voxels. The proof is a one-line term-mode reduction that unfolds the active-fraction definition and applies ring normalization.
Claim. Let $p = 11/16$ be the passive fraction of phase-locked modes from the $Q_3$ budget and let $a = 1 - p$ be the active fraction. Then $p + a = 1$.
background
The VacuumUniformity module proves that phase-locked J-cost supplies a constant, isotropic background to every voxel on the $Z^3$ carrier. PassiveFraction is defined as the combinatorial fraction $11/16$ of modes that remain phase-locked with zero maintenance cost $J(1)=0$. ActiveFraction is the definitional complement $1$ minus that value, ensuring the two fractions partition the mode budget.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of activeFraction (which expands to $1 - passiveFraction$) and invokes the ring tactic to reduce the arithmetic identity to reflexivity.
why it matters
This result supplies the fracs_sum field inside the vacuumUniformityCert structure, which in turn certifies the structural uniformity argument given in the module doc-comment. It closes the combinatorial step that the $11/16$ fraction is position-independent, supporting the claim that vacuum energy density is spatially uniform and consistent with the phase-saturation picture of $Omega_Lambda$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.