Physics Anomalous Magnetic Moment Schwinger Is Alpha Over 2pi

The Schwinger term

The electron behaves like a tiny magnet. In the simplest quantum theory, its magnetic strength, expressed by the g-factor, would be exactly 2. Measurements show it is slightly larger: about 2.002319. The excess, written g minus 2, is called the anomalous magnetic moment. In 1948 Julian Schwinger computed the leading contribution to this excess using quantum electrodynamics. His result, the Schwinger term, is alpha divided by 2 pi, where alpha is the fine-structure constant, a number near 1/137 that sets the strength of electromagnetic interactions.

In the Recognition Science framework, the same term appears as a defined quantity. The framework's machine-checked library of formal theorems contains a declaration named schwinger_is_alpha_over_2pi. That declaration proves, in the formal system, that the framework's Schwinger term equals (1 / alpha_inverse) / (2 pi), which is just alpha over 2 pi when alpha is written as the reciprocal of its inverse. The proof is a direct algebraic manipulation; it does not derive alpha from any deeper principle. The framework takes the measured value of alpha as an input, using CODATA 2018's 137.035999084(21) for the inverse fine-structure constant. The declaration also proves the term is positive and less than 0.002, and that the electron g-factor exceeds 2.

What the declaration does not claim is more important than what it proves. It does not derive the fine-structure constant. The framework explicitly acknowledges that it does not derive alpha at all; an earlier attempt to derive it from a route called w8 produced 137.036766, which differs from the measured value in the fourth decimal and is excluded by the measurement at more than 30000 sigma. The Schwinger term is a definition built on the measured alpha, not a prediction of alpha. It also does not prove the full anomalous magnetic moment, which requires higher-order terms; the framework lists known coefficients for those terms but does not derive them.

The practical consequence is modest but real: within the framework, the leading quantum correction to the electron's magnetic moment is a theorem, but it is a theorem about arithmetic, not about the origin of alpha. The framework's contribution here is to formalize a known physics result, not to explain where the coupling constant comes from. That origin remains an open target.

theorem schwinger_is_alpha_over_2pi :
    schwinger_term = (1 / codata_alpha_inverse) / (2 * Real.pi) := by
  unfold schwinger_term; field_simp

/-- **The measured coupling, CODATA 2018 `137.035999084(21)`.** Used as the
    physical input the Schwinger term needs; computing `g−2` requires a value of
    α and RS does not supply one.

    Renamed from `rs_alpha_inverse` on 2026-07-25. That name, and its docstring
    claiming the number came from `w8_projection_equality`, were both wrong: the
    w₈ route gives `137.036766`, which differs from this literal in the fourth
    decimal, and `Constants/AlphaGenesis/MeasurementVerdict.lean` proves it is
    excluded by this very measurement at more than 30000 sigma. Recognition
    Science proves it does not derive this constant at all; see
    `Constants/AlphaGenesis/AlphaStatus.lean`. -/
abbrev codata_alpha_inverse : ℝ := 137.035999084

@[deprecated codata_alpha_inverse (since := "2026-07-25")]

/-- Schwinger term is a small positive number less than 0.002. -/
theorem schwinger_in_range : 0 < schwinger_term ∧ schwinger_term < 0.002 :=
  ⟨schwinger_term_positive, schwinger_lt_002⟩

theorem g_exceeds_dirac : 2 < electron_g_factor := by
  unfold electron_g_factor; linarith [ae_leading_positive]

What this page does not claim

The framework does not derive the fine-structure constant alpha; it uses the measured value as input. The declaration does not prove the full anomalous magnetic moment, only the leading Schwinger term. The framework's earlier w8 route for alpha is excluded by measurement, not a valid derivation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/AnomalousMagneticMoment.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: