electron_g_factor
plain-language theorem explainer
The definition sets the electron g-factor to 2 plus twice the leading anomalous moment term taken from the Recognition Science phi-ladder. Physicists comparing RS predictions against the Dirac value and the Schwinger result would cite this when establishing the excess g-2. It is realized as a direct one-line algebraic definition that composes the ae_leading term.
Claim. The electron g-factor is defined by $g_e = 2 + 2 a_e^{(1)}$ where $a_e^{(1)} = 1/ (r_s^{-1} 2 pi)$ is the leading Schwinger term with $r_s^{-1}$ the RS alpha inverse.
background
The module derives the electron anomalous magnetic moment from the RS phi-ladder and eight-tick structure. The upstream ae_leading definition is exactly the Schwinger term $1/(rs_alpha_inverse * 2 pi)$, which supplies the leading correction in RS-native units where alpha inverse lies in (137.030, 137.039). The local theoretical setting is the paper RS_Electron_g_minus_2.tex that extracts g-2 from the Recognition Composition Law and the T5 J-uniqueness step of the forcing chain.
proof idea
One-line definition that directly adds twice the ae_leading term to the Dirac baseline of 2.
why it matters
This definition supplies the explicit value used by the downstream theorem g_exceeds_dirac to prove 2 < electron_g_factor. It fills the leading-order slot in the RS derivation of the anomalous moment and connects to the alpha band and the eight-tick octave in the T0-T8 chain. The parent result is the excess-over-Dirac theorem that supports consistency with QED at the Schwinger level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.