Physics Anomalous Magnetic Moment Schwinger In Range

The Schwinger bound

The electron's magnetic moment is not exactly twice its spin, as the Dirac equation predicts. The tiny difference is the anomalous magnetic moment, and its leading correction was computed by Julian Schwinger in 1948 as α/(2π), where α is the fine-structure constant, the dimensionless number near 1/137 that sets the strength of electromagnetic interactions. This first term is so small that it contributes roughly one part in a thousand to the electron's g-factor, the ratio that measures how strongly the electron responds to a magnetic field.

In the Recognition Science framework's machine-checked library of formal theorems, a declaration named schwinger_in_range (a verified statement in a formal proof system) establishes only a coarse bound on this Schwinger term. The theorem proves that the term is positive and that it is less than 0.002. That is the entire content: the correction is a small positive number below two thousandths. The proof uses the measured CODATA 2018 value of the inverse fine-structure constant, 137.035999084(21), as an input, and it relies on the elementary fact that π is greater than 3.

The framework does not derive the fine-structure constant itself. Its own documentation is explicit on this point: the w₈ projection route gives 137.036766, which differs from the measured value in the fourth decimal, and a separate theorem in the library proves that route is excluded by the measurement at more than 30000 sigma. The library also proves it does not derive this constant at all. The declaration schwinger_in_range therefore does not predict the electron's anomaly; it takes the measured coupling as given and proves a trivial inequality about the first QED coefficient.

What the declaration does establish, within the framework, is a structural consistency check. The library defines the electron g-factor as 2 + 2aₑ, where aₑ is the Schwinger term, and proves this exceeds 2, matching the experimental fact that the electron's g-factor is slightly above the Dirac value. It also records the known QED coefficients for higher-order terms. But the bound itself is deliberately weak: it says nothing about where in the interval (0, 0.002) the true value lies, and it does not supply the α that would pin that value down.

For a reader, the honest takeaway is simple. The declaration proves a small, true, and unsurprising fact: Schwinger's leading correction is a positive number less than 0.002. It does not prove the correction equals 0.00116, the measured value, nor does it derive α from first principles. The framework's contribution here is not a new number but a verified check that its own construction stays inside the right ballpark.

/-- 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⟩

/-- **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")]

/-- **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")]

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

What this page does not claim

The declaration does not prove the Schwinger term equals its measured value of about 0.00116. The declaration does not derive the fine-structure constant from the framework's own principles. The declaration does not establish the full electron g-factor or any higher-order QED correction.

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: