active_modes_eq
plain-language theorem explainer
The count of active ledger modes equals five: three face-pair modes from spatial dimension three, plus two diagonal (charge/parity) modes. Cosmologists deriving Ω_Λ from Q₃ mode budgets cite this equality as the fixed numerator side of the active/passive split. The proof is definitional reflexivity on the constant five.
Claim. The number of active modes equals $5$, where active modes are the matter excitations that participate in recognition: three face-pair (generation) modes forced by $D=3$, together with two diagonal charge/parity modes.
background
The module derives the dark-energy fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$ from phase saturation of the discrete ledger. At cosmic scale, matter excitations and vacuum modes equilibrate; the equilibrium vacuum fraction is identified with the passive-mode fraction of the cube graph $Q_3$.
Active modes are the complementary count: matter excitations that participate in recognition. By definition they equal five, decomposed as three face-pair/generation modes (from the forcing $D=3$ in the T0–T8 chain) plus two diagonal charge/parity modes. Passive modes are eleven: eight vertex ground states plus three unexcited face-pair contributions. The geometric seed $11/16$ is the passive share of the total mode budget $5+11=16$.
Upstream, active_modes is the bare natural-number constant five; the present theorem simply records that equality as a named fact for later arithmetic.
proof idea
One-line term proof by reflexivity: the definition of the active-mode count is the literal natural number five, so the equality holds by rfl. No lemmas are invoked.
why it matters
In the phase-saturation chain, the active count five is the combinatorial counterpart to the passive count eleven. Together they fix the geometric seed $11/16$ that appears in $\Omega_\Lambda = 11/16 - \alpha/\pi \approx 0.6852$. The three face-pair modes track the forced spatial dimension $D=3$ (T8); the two diagonal modes complete the recognition-active sector.
No downstream theorems currently depend on this equality by name (used-by is empty), but sibling results such as the geometric-seed identity and the $\Omega_\Lambda$ bounds treat five as the fixed active budget. The still-open pieces of the module are the hypotheses CosmicPhaseEquilibrium and vacuum_fraction_bridge, which must connect this combinatorial split to actual cosmic vacuum energy; the present fact only locks the integer side of that bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.