Omega_matter
plain-language theorem explainer
The matter density parameter is the active-mode share of the D=3 ledger plus the EM correction, Ω_m = 5/16 + α/π. Cosmologists citing the RS phase-saturation derivation of dark energy use it as the exact complement of Ω_Λ. It is a one-line arithmetic definition from the combinatorial mode counts and the measured fine-structure constant.
Claim. The matter fraction is defined by $\Omega_m = \dfrac{5}{16} + \dfrac{\alpha}{\pi}$, where $5$ counts active (matter) modes, $16$ is the total mode budget of the $D=3$ ledger vacuum, and $\alpha$ is the fine-structure constant.
background
The module identifies the cosmological vacuum fraction with equilibrium phase saturation of the discrete ledger. At cosmic scale, matter excitations and vacuum modes share a finite mode budget fixed by D=3 cube geometry; the passive share supplies the geometric seed for dark energy, corrected by one measured EM input.
Total mode budget is $16 = 2^4$ (D=3 cube doubled by double-entry bookkeeping). Active modes are $5 = 3$ face-pair/generation modes $+,2$ charge/parity modes; passive modes are $11$. The same $\alpha$ that appears in $\Omega_\Lambda = 11/16 - \alpha/\pi$ is the CODATA fine-structure constant imported as the sole external anchor.
Thus the matter fraction is written as the complementary active share plus the opposite-sign $\alpha/\pi$ term, so that closure is pure arithmetic once both definitions are unfolded.
proof idea
Definition only: cast the naturals active_modes (=5) and mode_budget (=16) to reals, form their ratio, and add $\alpha/\pi$. No tactics or lemmas. Downstream closure later unfolds both density parameters and finishes by ring.
why it matters
Direct input to omega_closure ($\Omega_\Lambda + \Omega_m = 1$) and to coincidence_ratio_structural, which shows $\Omega_\Lambda/\Omega_m > 1$ so the coincidence problem is O(1) by construction. It is also a field of PhaseSaturationVacuumCert (closure and mode partition).
In the RS chain the $16$-mode budget and the $5$+$11$ split come from D=3 cube geometry forced at T8; the $\alpha/\pi$ correction is the same EM shift used for the vacuum side. The $10^{120}$ discrepancy is dissolved because both fractions are dimensionless mode ratios, not energies renormalized against $M_{\mathrm{Pl}}^4$. The identification still depends on the open hypotheses CosmicPhaseEquilibrium and vacuum_fraction_bridge that link ledger saturation to cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.