passive_fraction_pos
plain-language theorem explainer
The passive fraction of phase-locked modes equals the constant 11/16 and is therefore strictly positive. Cosmologists using the Recognition Science vacuum model cite this result to guarantee that phaseLockEnergy remains non-negative. The proof is a one-line wrapper that unfolds the definition and applies norm_num.
Claim. The combinatorial fraction of phase-locked modes in the Q₃ budget, given by $11/16$, satisfies $11/16 > 0$.
background
The VacuumUniformity module shows that phase-locked modes contribute a constant isotropic J-cost to every voxel of the ℤ³ carrier. passiveFraction is the fixed combinatorial share 11/16 of the Q₃ mode budget, independent of position by the VoxelSymmetry axiom. The module doc-comment states that this fraction is a combinatorial property of Q₃, so the vacuum energy density is spatially uniform.
proof idea
The proof is a one-line wrapper that unfolds passiveFraction to the constant 11/16 and invokes norm_num to confirm the inequality.
why it matters
This theorem supplies the positivity hypothesis required by vacuum_energy_pos, which multiplies passive_fraction_pos by E_coh_pos to obtain phaseLockEnergy > 0. It completes the structural-uniformity step in the module argument that vacuum J-cost is position-independent. In the Recognition framework it anchors the non-negative vacuum contribution to the stress-energy tensor before any physical identification with Ω_Λ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.