passive_fraction_lt_one
plain-language theorem explainer
The passive fraction of phase-locked modes drawn from the Q3 budget is strictly less than one. Researchers modeling vacuum energy uniformity cite it to guarantee a positive active complement in the stress-energy tensor. The proof is a one-line term wrapper that unfolds the constant definition and applies numerical normalization.
Claim. Let $f$ denote the fraction of phase-locked modes in the $Q_3$ budget, defined by $f = 11/16$. Then $f < 1$.
background
The module establishes that phase-locked modes contribute a constant, isotropic J-cost to every voxel of the $Z^3$ carrier. PassiveFraction is the combinatorial fraction $11/16$ of the total mode budget allocated to these locked states. The complements definition pairs each vantage with its active and outside counterparts, ensuring the active fraction is the remainder that sums to unity with the passive part.
proof idea
One-line wrapper that unfolds passiveFraction to the literal constant $11/16$ and invokes norm_num to discharge the inequality.
why it matters
The result closes the elementary bound needed for the vacuum energy uniformity argument in the same module. It confirms that the passive share remains strictly below unity, so the active complement is positive and the total J-cost remains spatially uniform. This step supports the structural half of the vacuum uniformity theorem while leaving the physical identification of the fraction with $T^vac_mu nu$ as a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.