schwinger_term
plain-language theorem explainer
The definition supplies the leading Schwinger correction to the electron anomalous magnetic moment as the reciprocal of the RS-derived inverse fine-structure constant times 2 pi. Researchers comparing Recognition Science predictions to experimental g-2 data would cite this term when isolating the first-order QED contribution. It is realized through direct substitution of the numerical alpha inverse into the standard formula.
Claim. The leading Schwinger term in the electron anomalous magnetic moment is given by $a_e^{(1)} = 1/ (α_{RS}^{-1} · 2π)$, where $α_{RS}^{-1}$ is the Recognition Science value of the inverse fine-structure constant.
background
Recognition Science constructs the fine-structure constant from the J-uniqueness fixed point and the eight-tick octave. This module develops the electron anomalous magnetic moment from the RS φ-ladder, following the paper RS_Electron_g_minus_2.tex. The upstream rs_alpha_inverse supplies the constant 137.035999084 obtained from w8_projection_equality. The classical Schwinger term in QED is α/(2π), which this expression reproduces using the RS alpha.
proof idea
The definition is a direct arithmetic expression that divides 1 by the product of the RS alpha inverse and twice pi. No lemmas are applied beyond the arithmetic operations; it serves as the base expression for subsequent positivity and range theorems.
why it matters
This definition anchors the leading term in the RS electron g-factor calculation and feeds ae_leading, schwinger_term_positive, and schwinger_in_range. It places the Schwinger correction inside the Recognition Science alpha band (137.030 to 137.039) and supports comparisons in the muon g-2 module. The term connects to the eight-tick structure for g-2 predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.