row_electron_ae_leading_lower
plain-language theorem explainer
row_electron_ae_leading_lower establishes that the leading Schwinger term a_e^(1) = α/(2π) exceeds 0.001161 when evaluated at the Recognition Science inverse fine-structure constant. Physicists validating RS-derived QED predictions against CODATA data would cite this bound. The tactic proof rewrites the definition, converts via division inequality, and chains explicit upper bounds on π and alphaInv to discharge the claim with linarith.
Claim. $0.001161 < α / (2π)$ where $α = 1/α_{inv}$ and $α_{inv}$ is the Recognition Science inverse fine-structure constant satisfying $α_{inv} < 137.039$.
background
The Electron g-2 Score Card module treats Phase 1 row P1-C05. It isolates the leading Schwinger term a_e^(1) = α/(2π) and proves the numerical interval 0.001161 < a_e^(1) < 0.001162 using the certified RS value of α_inv. The definition row_electron_ae_leading := α / (2 * Real.pi) supplies the explicit expression, with α = 1/α_inv.
proof idea
The proof rewrites via row_electron_ae_leading_eq, applies lt_div_iff₀ using ae_den_pos, then builds upper bounds: π < 3.142 from Real.pi_lt_d6, 2π < 2*3.142, multiplication by α_inv via mul_lt_mul_of_pos_right with alphaInv_pos, further multiplication by 137.039 via alphaInv_lt, and a numerical check that 0.001161 times the resulting upper bound is less than 1. The final product inequality and linarith close the argument.
why it matters
This lower bound pairs with row_electron_ae_leading_upper to produce row_electron_ae_leading_bracket, which supplies the full interval for the Schwinger term inside the electron g-2 scorecard. It verifies that the RS alphaInv band (137.030, 137.039) yields a one-loop prediction within 0.3 % of CODATA. The full g-2 row stays partial because higher-order loop terms have not yet been derived from RS primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.