em_correction
plain-language theorem explainer
The electromagnetic correction to the dark-energy fraction is α/π, using the CODATA 2022 fine-structure constant as the single measured input. Cosmologists deriving Ω_Λ from the eight-tick phase budget cite it when subtracting the one-loop EM vacuum shift from the combinatorial 11/16 saturation. The declaration is a one-line noncomputable real definition, not an inequality.
Claim. Define the electromagnetic vacuum-mode correction by $\delta_{\mathrm{EM}} := \alpha/\pi$, where $\alpha = 7.2973525643\times 10^{-3}$ is the CODATA 2022 fine-structure constant (external anchor).
background
In the Ω_Λ derivation module, dark energy is read as a saturated fraction of the eight-tick DFT mode budget. Of 44 forced frequency modes, 11 are Q₃-symmetric (three spatial axes plus gauge sector under the [4,2,2] Gray-code asymmetry). The raw saturated fraction is therefore the pure combinatorial ratio 11/16 = 0.6875, coming from 2⁴ tick addressing of the octave cycle.
Electromagnetism does not sit outside that budget: the module treats the fine-structure constant as a one-loop correction to the vacuum mode count. The fraction of EM-active modes is taken as α/(2π), which halves once more when written as a reduction of the saturation fraction, yielding the shift α/π.
The only external number is the CODATA 2022 anchor α = 7.2973525643×10⁻³ (relative uncertainty 1.5×10⁻¹⁰). An earlier attempt to replace it by a constructed RS α was reverted: that seed is an identification, not a derived coupling, and is excluded by measurement at huge significance. Hence the correction is deliberately one measured input.
proof idea
Pure definition: the real is the quotient of the external CODATA anchor by Real.pi. No tactics, no lemmas, no unfolding beyond that assignment. Downstream positivity and smallness proofs unfold this name and compare α and π against decimal bounds (π > 3.14, π < 3.15, α in a thin window around 0.0073).
why it matters
This is Step 3 of the module's core claim: Ω_Λ = 11/16 − α/π. It is subtracted from omega_raw to form omega_lambda, and appears in the certificate structure OmegaLambdaCert (correction_bounds and the canonical-form identity). Sibling inequalities pin 0.002 < δ_EM < 0.004, which with raw = 0.6875 immediately give Ω_Λ ∈ (0.683, 0.686).
Downstream, CosmologicalConstantDerivation.Omega_Lambda_interval (THEOREM C-010.4b) identifies Omega_Lambda_RS with this omega_lambda and restores the tight numeric window used by Planck-check and BIT-kernel modules. Framework landmarks: the eight-tick octave (T7) supplies the 2⁴ addressing and the 44-mode/Q₃ count behind 11/16; α enters only as the measured EM coupling, consistent with the RS alpha band being a separate construction not used here. The open policy choice is explicit: keep one external anchor rather than claim zero free parameters with a false α seed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.