PhaseSaturationVacuumCert
plain-language theorem explainer
Certificate bundling the RS dark-energy package: Ω_Λ = 11/16 − α/π is positive, below 1 and below the geometric seed 11/16; active and passive modes partition the budget; closure and coincidence hold; w = −1 exactly; and Ω_Λ equals the passive-mode fraction minus α/π. Cosmologists citing the phase-saturation origin of Λ would reference this bundle. It is a pure structure definition; the inhabitant is assembled by a separate theorem.
Claim. A certificate asserting that the dark-energy fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$ satisfies $0 < \Omega_\Lambda < 1$ and $\Omega_\Lambda < 11/16$; that active plus passive modes equal the mode budget; that $\Omega_\Lambda + \Omega_m = 1$ with $\Omega_\Lambda / \Omega_m > 1$; that the vacuum equation of state is exactly $w = -1$; and that $\Omega_\Lambda$ equals the passive-mode fraction minus $\alpha/\pi$.
background
This module identifies the cosmological dark-energy fraction with the equilibrium vacuum share of a finite discrete ledger under phase saturation. The RS prediction is $\Omega_\Lambda = 11/16 - \alpha/\pi$: a cube-geometry seed $11/16$ corrected by the measured fine-structure constant over $\pi$. Numerically this is about $0.685$.
Mode counting is combinatorial. Active modes (matter excitations) equal $5$ (three face-pair/generation modes plus two charge/parity modes). Passive modes (vacuum) equal $11$ (eight vertex ground states plus three unexcited face-pair contributions). The mode budget is their sum, $16$. Matter is the complement: $\Omega_m = 5/16 + \alpha/\pi$.
The equation of state is fixed at $w = -1$ because the vacuum recognition cost $J(1) = 0$ is tick-independent, so the vacuum energy density is constant. The structure packages positivity, upper bounds, partition, closure, coincidence ($\Omega_\Lambda > \Omega_m$), exact $w$, and the mode-fraction identity into one certificate type.
proof idea
No proof body: this is a structure definition whose fields are propositions. Each field names a claim already proved (or defined) elsewhere in the module: positivity and bounds on $\Omega_\Lambda$, the natural-number partition of the mode budget, algebraic closure $\Omega_\Lambda + \Omega_m = 1$, the coincidence inequality, the integer identity $w = -1$, and the mode-fraction rewrite of $\Omega_\Lambda$. Inhabitation is deferred to the constructor theorem that supplies proofs for every field.
why it matters
The structure is the formal checklist for the phase-saturation account of the cosmological constant. Its sole downstream user is the theorem that builds a concrete inhabitant, discharging every field with the module's positivity, bound, partition, closure, coincidence, EOS, and mode-fraction lemmas.
In the framework this is the cosmology-side packaging of the claim that vacuum energy is a dimensionless $O(1)$ mode fraction, not an $M_{\mathrm{Planck}}^4$ density needing renormalization—the route by which the module dissolves the $10^{120}$ discrepancy. The geometric seed $11/16$ comes from $Q_3$ mode counting; $\alpha/\pi$ is the single measured EM correction. Upstream hypotheses still separate from this certificate (cosmic phase equilibrium and the vacuum-fraction bridge) remain the open links between ledger saturation and cosmology; the certificate itself only records the closed algebraic and combinatorial side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.