omega_lambda_one_measured_input
plain-language theorem explainer
The dark-energy fraction equals the saturated phase-mode ratio minus the CODATA fine-structure constant over π. Anyone citing the RS Ω_Λ derivation uses this identity to isolate the single external measured input from pure combinatorics. The proof is definitional: unfold the raw fraction and EM correction, then reflexivity.
Claim. The RS dark-energy fraction satisfies $\Omega_\Lambda = N_{\mathrm{sat}}/N_{\mathrm{addr}} - \alpha_{\mathrm{CODATA}}/\pi$, where $N_{\mathrm{sat}}=11$ is the $Q_3$-saturated mode count and $N_{\mathrm{addr}}=16$ is the 8-tick addressing bit count ($2^4$).
background
This module derives the cosmological constant fraction $\Omega_\Lambda$ from phase saturation on the eight-tick cycle. The core claim is $\Omega_\Lambda = 11/16 - \alpha/\pi \in (0.680, 0.700)$, consistent with Planck 2018.
The raw saturated fraction is the ratio of $Q_3$-saturated modes ($N_{\mathrm{sat}} = 11$, from the $[4,2,2]$ Gray-code plus gauge structure) to the 8-tick addressing bits ($N_{\mathrm{addr}} = 2^4 = 16$). The electromagnetic correction is the one-loop vacuum-mode shift $\alpha_{\mathrm{CODATA}}/\pi$, using the external CODATA 2022 anchor $\alpha = 7.2973525643 \times 10^{-3}$. Locally, $\Omega_\Lambda$ is defined as raw fraction minus that correction.
An earlier revision tried to replace CODATA $\alpha$ by a constructed RS $\alpha$; that was reverted because the construction seed is an identification, not a derived coupling. The present certificate therefore keeps exactly one measured input.
proof idea
Term-mode definitional equality. Unfold the three defining abbreviations ($\Omega_\Lambda$ as raw minus EM correction, raw as the saturated-mode ratio, EM correction as $\alpha_{\mathrm{CODATA}}/\pi$). The goal is then identical on both sides, so rfl closes it. No arithmetic lemmas are required.
why it matters
This is the structural decomposition that makes the "one measured input" claim precise: integer combinatorics from the eight-tick octave (T7) and $Q_3$ mode count, minus a single external $\alpha$. Downstream, omega_lambda_canonical_form rewrites the same identity to the textbook shape $11/16 - \alpha_{\mathrm{CODATA}}/\pi$ by unfolding the two natural-number constants and normalizing. That canonical form is what the module bounds against Planck 2018 and what sibling inequalities ($\Omega_\Lambda < 0.686$, $\Omega_\Lambda > 0.683$) rest on. The result therefore sits at the hinge between the phase-mode budget and the observational certificate for dark energy in RS units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.