g_exceeds_dirac
plain-language theorem explainer
The theorem establishes that the electron g-factor exceeds 2, confirming a positive anomalous magnetic moment within the Recognition Science phi-ladder derivation. Physicists comparing RS predictions to QED data would cite this when verifying the sign of the leading correction. The proof is a one-line wrapper that unfolds the g-factor definition and applies linear arithmetic to the positivity of the anomalous term.
Claim. $2 < g_e$ where $g_e := 2 + 2 a_e$ and $a_e$ is the leading anomalous magnetic moment coefficient.
background
The module derives the electron anomalous magnetic moment from the RS phi-ladder and eight-tick structure, as outlined in the paper RS_Electron_g_minus_2.tex. The definition electron_g_factor sets the g-factor to 2 plus twice the leading anomaly term ae_leading. The upstream theorem ae_leading_positive establishes that ae_leading exceeds zero and follows directly from schwinger_term_positive.
proof idea
The proof is a one-line wrapper. It unfolds the definition of electron_g_factor to obtain the expression 2 + 2 * ae_leading, then invokes linarith on the hypothesis ae_leading_positive.
why it matters
This result places the RS g-factor strictly above the Dirac value of 2, consistent with the positive Schwinger correction extracted from the J-cost and Recognition Composition Law. It supports the framework claim that the anomaly originates at the eight-tick octave scale. The theorem feeds into later numerical comparisons with experiment, though higher-order terms are deferred to sibling declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.