alpha_over_pi_bounds
plain-language theorem explainer
The fine-structure constant over π lies strictly between 0.0023 and 0.0024. Cosmology and verification modules cite this to control the EM correction in the RS dark-energy formula Ω_Λ = 11/16 − α/π. The proof chains the existing α interval (0.00729, 0.00731) with crude π bounds (3.14, 3.15) through two short division inequalities.
Claim. With $\alpha$ the RS fine-structure constant, one has $0.0023 < \alpha/\pi < 0.0024$.
background
This module runs preregistered Hubble tests: a relative-error check on the early-to-late H ratio, and a 1σ check on Ω_Λ. The Ω_Λ test needs a tight numeric handle on the EM correction term α/π.
In RS, α is the derived fine-structure constant (α = 1/α_Inv, with α_Inv forced near 137.036 and certified inside (137.030, 137.039)). Upstream, Physics.CKMGeometry supplies the working interval 0.00729 < α < 0.00731 used throughout CKM and cosmology proofs. Mathlib supplies decimal bounds on π: 3.14 < π < 3.15.
The same bound appears in the cosmology layer as the lemma needed for the dark-energy match: with α ∈ (0.00729, 0.00731) and π ∈ (3.14, 3.15), one gets α/π ∈ (0.00729/3.15, 0.00731/3.14) ≈ (0.002314, 0.002328), which sits inside (0.0023, 0.0024).
proof idea
Pull in the CKMGeometry lower and upper bounds on α, and Mathlib's six-decimal π inequalities (strengthened by linarith to 3.14 < π < 3.15). Record positivity of α and π.
Lower half: 0.0023 < 0.00729/3.15 by norm_num, then 0.00729/3.15 < α/3.15 by dividing the α-lower bound by the positive constant 3.15, then α/3.15 < α/π because π < 3.15 and α > 0.
Upper half: α/π < α/3.14 because 3.14 < π, then α/3.14 < 0.00731/3.14 by the α-upper bound, then 0.00731/3.14 < 0.0024 by norm_num.
why it matters
The RS dark-energy prediction is Ω_Λ = 11/16 − α/π (cube-geometry seed minus the measured-α EM correction). This lemma freezes α/π inside a two-digit window so that Ω_Λ_pred ≈ 0.6852 can be compared to the observational central value 0.6847 with error 0.0073.
Downstream, dark_energy_match applies it directly to prove |Ω_Λ_pred − Ω_Λ_exp| < Ω_Λ_err (within 1σ). The preregistered test omega_lambda_passes_1sigma and the certificate structure HubbleTensionCert both depend on that match. The sibling Hubble-ratio test (0.05% relative error) is independent; this bound is the arithmetic gate for the Ω_Λ side of the verification suite.
Framework landmark: α itself sits in the RS-native band α^{-1} ∈ (137.030, 137.039); the present result only packages that band into the α/π form required by the cosmological-constant formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.