em_correction_pos2
plain-language theorem explainer
The electromagnetic vacuum correction α/π is strictly larger than 0.002 when α is the CODATA fine-structure constant. Cosmologists bounding the RS dark-energy fraction cite this lower bound when subtracting the one-loop EM mode correction from the raw 11/16 saturation. The proof is a short numerical comparison: α exceeds 0.002·3.15 while π is less than 3.15.
Claim. With $\alpha$ the CODATA 2022 fine-structure constant, the electromagnetic correction satisfies $\alpha/\pi > 0.002$.
background
In the Ω_Λ derivation module, the dark-energy fraction is obtained from phase-mode saturation on the eight-tick cycle. The raw saturated fraction is the combinatorial ratio 11/16 (eleven Q₃-symmetric modes out of the 2⁴ addressing budget). A one-loop electromagnetic correction then reduces the effective saturation: the fraction of EM-active modes is taken as α/(2π), which subtracts α/π from the raw fraction.
The correction itself is defined as the external CODATA anchor α divided by π (one measured input; the module deliberately does not substitute a constructed α). Sibling bounds pin the correction from above and below so that Ω_Λ lands in a Planck-compatible interval. The present lemma is the strict positive lower bound used on the upper side of that interval.
proof idea
Unfold the correction to α_CODATA/π. Use the library facts π < 3.15 and π > 0, rewrite the goal via the positive-denominator form of division, and reduce to showing 0.002 · 3.15 < α_CODATA. That numerical inequality is discharged by unfolding the CODATA decimal and norm_num; nlinarith closes the chain.
why it matters
The upper bound Ω_Λ < 0.686 applies this lemma directly: raw fraction 0.6875 minus a correction larger than 0.002 forces the result below 0.686. The certificate omegaLambdaCert packages the same lower bound together with the matching upper bound on the correction as the pair of correction bounds that underwrite the final interval and Planck consistency. Within the broader RS cosmology story this is the quantitative control on Step 3 of the module derivation (EM one-loop reduction of the 11/16 saturation), keeping Ω_Λ inside (0.680, 0.700) and near the Planck 2018 central value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.