alpha_over_pi_bounds
plain-language theorem explainer
The theorem establishes that the fine-structure constant over pi satisfies 0.0023 < alpha/pi < 0.0024. Dark energy modelers working in the Recognition Science ledger geometry cite it to close the numerical error budget for the Omega_Lambda prediction. The proof obtains separate bounds on alpha from CKM geometry and on pi from the reals library, then transfers them to the ratio by monotonicity of division in two calc chains.
Claim. Let α denote the fine-structure constant. Then 0.0023 < α/π < 0.0024.
background
The Cosmology.HubbleTension module develops T13, the derivation of the Hubble tension and dark energy density from ledger geometry. Dark energy density takes the form Ω_Λ = 11/16 − α/π, where the base term 11/16 arises from the passive-field volume fraction E_passive/(2 V_total) with V_total = 8 vertices of the 3-cube, and the α/π term supplies the geometric correction. The fine-structure constant α is defined in Constants.Alpha as the reciprocal of its inverse, with the module importing numerical bounds from Physics.CKMGeometry.
proof idea
The tactic proof first records the alpha lower and upper bounds from CKMGeometry together with the pi inequalities 3 < π, 3.14 < π < 3.15 and positivity of both quantities. For the lower bound on α/π a calc block inserts the numerical comparison 0.0023 < 0.00729/3.15, lifts the alpha lower bound across division by 3.15, and finally replaces the denominator by the larger π. The upper bound reverses the steps: first shrink the denominator to 3.14, then lift the alpha upper bound, and finish with a numerical comparison to 0.0024.
why it matters
The result is invoked directly by the downstream dark_energy_match theorem to verify |Ω_L_pred − Ω_L_exp| < Ω_L_err. It supplies the missing numerical interval for the α/π correction in the T13 formula Ω_Λ = 11/16 − α/π, guaranteeing the predicted value 0.6852 lies within 1σ of the Planck observation 0.6847. In the broader Recognition Science chain it anchors the alpha band inside the RS-native units and the geometric origin of dark energy as a ledger correction term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.