ae_leading
plain-language theorem explainer
The leading Schwinger correction to the electron anomalous magnetic moment is set to alpha over two pi using the RS inverse fine-structure constant. Precision QED researchers cite this when isolating the first-order contribution to the electron g-factor in Recognition Science calculations. It enters as a direct alias to the module Schwinger term.
Claim. The leading term of the electron anomalous magnetic moment is defined by $a_e^{(1)} = 1/ (r_s^{-1} 2 pi)$, where $r_s^{-1}$ denotes the Recognition Science value of the inverse fine-structure constant.
background
The module derives the electron anomalous magnetic moment from the RS phi-ladder and eight-tick structure, per the paper RS_Electron_g_minus_2.tex. The Schwinger term supplies the leading QED correction $a_e^{(1)} = alpha/(2 pi)$. Upstream, Experimental.MuonGMinusTwo.schwinger_term states the standard form alpha_em / (2 * Real.pi), while the local version substitutes the RS alpha inverse as 1 / (rs_alpha_inverse * (2 * Real.pi)).
proof idea
This is a one-line wrapper that aliases the local schwinger_term definition.
why it matters
It supplies the base value for ae_leading_positive and the electron g-factor definition g = 2 + 2 a_e. This embeds the classic Schwinger result inside the Recognition Science framework, connecting the alpha band (137.030 to 137.039) to the eight-tick octave. It touches the open question of deriving alpha from the phi-ladder rather than importing it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.