active_modes
plain-language theorem explainer
Active modes count the matter excitations that participate in recognition: three face-pair/generation modes plus two charge/parity modes, totaling five. Cosmologists deriving the phase-saturation formula for Ω_Λ cite this constant as the numerator of the bare matter fraction. It is a bare natural-number definition fixed by Q₃ mode-counting combinatorics.
Claim. The number of active modes (matter excitations participating in recognition) equals $5$, counted as $3$ face-pair/generation modes plus $2$ 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 reach equilibrium; the equilibrium vacuum fraction is identified with the passive-mode fraction of the $Q_3$ geometry.
Active modes are the matter side of that partition. The companion passive count is $11 = 8$ (vertex ground states) $+ 3$ (unexcited face-pair contributions). The total mode budget is their sum, and the geometric seed $11/16$ is the passive fraction before the $\alpha/\pi$ correction.
Upstream geometry supplies the face maps of the singular $2$-simplex and the topological face inclusions of the standard simplex; the Yang–Mills vacuum (all bonds at rung $0$) anchors the passive side. Dimension forcing ($D=3$) fixes the three face-pair/generation slots that enter the active count.
proof idea
Bare constant definition: the natural number is set equal to $5$. No tactics or lemmas are invoked. The arithmetic identity $3+2=5$ and the geometric reading (three face-pair modes from $D=3$, plus two charge/parity modes) are recorded in the doc-comment and discharged by reflexivity in the companion equality theorem.
why it matters
This constant is the numerator of the bare matter fraction. Downstream, $\Omega_m$ is defined as $(\mathrm{active\ modes})/(\mathrm{mode\ budget}) + \alpha/\pi$, i.e. $5/16 + \alpha/\pi$. The partition theorem states that active plus passive modes equal the mode budget; omega-closure then gives $\Omega_\Lambda + \Omega_m = 1$ by direct unfolding and ring. The certificate structure packages the partition and closure as fields of the phase-saturation vacuum certificate, dissolving the $10^{120}$ discrepancy by treating vacuum energy as a dimensionless $O(1)$ mode fraction rather than a density renormalized against $M_{\mathrm{Pl}}^4$.
The count sits on the forcing chain: $D=3$ (T8) supplies the three face-pair/generation modes. The remaining open pieces of the module are the cosmic-phase-equilibrium hypothesis and the vacuum-fraction bridge from ledger saturation to cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.