phase_saturation_vacuum_cert
plain-language theorem explainer
Certificate bundling eight proved facts about the RS dark-energy fraction Ω_Λ = 11/16 − α/π: positivity, subunitarity, seed upper bound, active/passive mode partition, flat closure with matter, coincidence ratio > 1, exact w = −1, and the mode-fraction identity. Cosmologists citing the phase-saturation origin of Λ would point here. The proof is pure structure assembly of already-proved component lemmas.
Claim. There is a certificate that $\Omega_\Lambda = 11/16 - \alpha/\pi$ satisfies $0 < \Omega_\Lambda < 1$, $\Omega_\Lambda < 11/16$, active modes plus passive modes equal the mode budget $2^{D+1}$, $\Omega_\Lambda + \Omega_m = 1$, $\Omega_\Lambda/\Omega_m > 1$, equation of state $w = -1$, and $\Omega_\Lambda$ equals the passive-mode fraction minus $\alpha/\pi$.
background
This module treats dark energy as the equilibrium vacuum fraction of a discrete ledger under phase saturation. The core identification is $\Omega_\Lambda = 11/16 - \alpha/\pi \approx 0.6852$, read as the passive mode fraction of the $Q_3$ geometry corrected by the fine-structure term $\alpha/\pi$.
Spatial dimension is forced to $D = 3$ (T8/T9), so the mode budget is $2^{D+1} = 16$. Combinatorial counting splits that budget into active and passive modes; the passive share is the geometric seed $11/16$. Matter density is the complementary active share, giving exact flat closure $\Omega_\Lambda + \Omega_m = 1$ by algebra.
Upstream lemmas already prove positivity ($\Omega_\Lambda > 0$ from $\alpha/\pi < 11/16$), the seed bound ($\Omega_\Lambda < 11/16$ from $\alpha/\pi > 0$), subunitarity via the seed, the mode partition by native decision, structural coincidence $\Omega_\Lambda/\Omega_m > 1$, exact $w = -1$, and the mode-fraction rewrite of the definition.
proof idea
Term-mode structure instance: each field of the certificate is filled by a named lemma already in the module. Positivity, seed bound, and subunitarity come from Omega_Lambda_pos, Omega_Lambda_lt_seed, and Omega_Lambda_lt_one. Mode partition is mode_budget_partition (native_decide on the combinatorial counts). Closure is omega_closure (ring after unfolding). Coincidence is coincidence_ratio_structural (uses $\Omega_\Lambda > 1/2$ and complementary $\Omega_m < 1/2$). Exact $w = -1$ and the mode-fraction identity are the remaining two component theorems. No new arithmetic is performed at the certificate layer.
why it matters
This is the module-level seal that the phase-saturation derivation of $\Omega_\Lambda$ is fully certified on the proved side of the ledger. The structure doc states the payoff: the classic $10^{120}$ vacuum-energy discrepancy dissolves because vacuum energy is a dimensionless $O(1)$ mode fraction, not a density renormalized against $M_{\mathrm{Pl}}^4$.
It sits at the end of the combinatorial chain (mode budget $2^{D+1}$, passive fraction $11/16$, $\alpha/\pi$ correction) that the module summary marks PROVED, while leaving cosmic phase equilibrium and scale invariance as explicit hypotheses. Downstream use is not yet wired in-repo (used_by empty); the certificate is the natural handoff point for any later cosmology bridge that needs the full bundle rather than individual bounds.
Framework landmarks in play: $D = 3$ from the forcing chain, and $\alpha$ in the RS band that supplies the $\alpha/\pi$ shift off the pure geometric seed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.