em_correction_small
plain-language theorem explainer
The electromagnetic vacuum correction α/π is strictly less than 0.004 when α is the CODATA fine-structure constant. Cosmologists deriving the RS dark-energy fraction Ω_Λ = 11/16 − α/π cite this to pin the lower edge of the predicted band. The proof is a short real-arithmetic comparison: α < 0.004·3.14 and π > 3.14 force α/π < 0.004.
Claim. With the CODATA fine-structure constant $\alpha$ and the real number $\pi$, the electromagnetic correction $\alpha/\pi$ satisfies $\alpha/\pi < 0.004$.
background
The module derives the dark-energy density fraction from phase saturation on the eight-tick DFT. The raw saturated fraction is the combinatorial ratio $11/16 = 0.6875$ (eleven $Q_3$-symmetric modes out of the $2^4$ tick-addressing budget). Electromagnetic coupling then subtracts a one-loop correction of size $\alpha/\pi$, so $\Omega_\Lambda = 11/16 - \alpha/\pi$.
Here the correction is defined with the external CODATA anchor $\alpha = 7.2973525643\times 10^{-3}$, not a constructed RS value. The module doc records that an earlier attempt to replace CODATA $\alpha$ by an internal construction was reverted: the seed $4\pi\cdot 11$ is an identification, not a derived coupling. Bounding $\alpha/\pi$ from above is the elementary real-analysis step needed before the final interval for $\Omega_\Lambda$ can be closed.
proof idea
Unfold the definition $\mathrm{em_correction} = \alpha_{\mathrm{CODATA}}/\pi$. Use $\pi > 3.14$ and $\pi > 0$ to rewrite $\alpha/\pi < 0.004$ as $\alpha < 0.004\cdot\pi$. Monotonicity of multiplication by the positive constant $0.004$ gives $0.004\cdot 3.14 < 0.004\cdot\pi$. A direct norm_num check shows the literal CODATA value is strictly less than $0.004\cdot 3.14$. Transitivity via linarith finishes the bound.
why it matters
This upper bound is half of the correction sandwich fed into the certificate omegaLambdaCert (paired with the matching lower bound $> 0.002$). It is applied directly in omega_lambda_gt_683, which proves $\Omega_\Lambda > 0.683$ by subtracting less than $0.004$ from the raw fraction $0.6875$. Together these place $\Omega_\Lambda$ inside $(0.680, 0.700)$, consistent with Planck 2018. In the broader RS picture the $11/16$ piece comes from the eight-tick octave and the forced three spatial dimensions; the $\alpha/\pi$ term is the sole measured input retained after the 2026-07-06 reversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.