ae_den_pos
plain-language theorem explainer
This establishes strict positivity of twice pi times the RS-derived inverse fine-structure constant. Bounds on the leading Schwinger term of the electron anomalous magnetic moment cite it to justify division steps. The proof is a one-line wrapper that applies nonlinear arithmetic to the known positivity of pi and of alpha inverse.
Claim. $0 < 2π α^{-1}$, where $α^{-1}$ denotes the dimensionless inverse fine-structure constant obtained from the structural seed and gap via exponential resummation.
background
The module supplies certified bounds on the leading Schwinger contribution $a_e^{(1)} = α/(2π)$ to the electron g-2 anomaly, using the RS value of $α^{-1}$. The definition $α^{-1} := α_seed · exp(−f_gap/α_seed)$ supplies a parameter-free number near 137.036. Upstream theorems establish its positivity by linear arithmetic on the seed-gap inequality.
proof idea
The proof is a one-line wrapper that invokes nlinarith on Real.pi_pos and the local alphaInv_pos fact.
why it matters
The result supplies the denominator positivity needed by row_electron_ae_leading_lower and row_electron_ae_leading_upper to bound the Schwinger term between 0.001161 and 0.001162. It closes the arithmetic step for the Phase 1 row P1-C05 slice inside the Recognition Science constants derivation, while the full g-2 series remains open because higher-loop terms have not yet been obtained from RS primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.