Physics Anomalous Magnetic Moment Schwinger Term Positive

The positive Schwinger term

The electron's magnetic moment is not exactly the value the simplest quantum theory predicts. A one-loop correction, first computed by Julian Schwinger in 1948, shifts it by a small amount proportional to the fine-structure constant α divided by 2π. That shift, called the Schwinger term, is the leading contribution to the famous "g minus 2" anomaly. For the electron it is about 0.00116, a number so small that it requires precise measurement to detect, yet it is one of the most accurately verified predictions in physics.

In the Recognition Science framework, this term is defined using the measured value of the inverse fine-structure constant, 137.035999084, which is taken from the CODATA 2018 adjustment. The framework does not derive this constant; it uses it as an input. The term is then defined as 1 divided by (137.035999084 times 2π), which is exactly α/(2π). The framework's machine-checked library of formal theorems proves that this number is positive, that it is less than 0.002, and that the electron's g-factor, defined as 2 plus twice the Schwinger term, is therefore greater than 2.

In Recognition Science, the theorem schwinger_term_positive establishes that the Schwinger term is a positive real number. The proof is direct: the numerator 1 is positive, and the denominator is a product of positive numbers (137.035999084, 2, and π), so the quotient is positive. This is a formal, machine-checked result. The framework also proves the term is less than 0.002, using the fact that π is greater than 3, and combines these to show the term lies in the open interval (0, 0.002).

What this declaration does not claim is more important than what it does. It does not derive the value of α; the framework explicitly states it does not derive this constant at all. It does not prove that the Schwinger term is the correct physical prediction beyond the leading order, nor does it account for the many higher-order corrections that contribute to the measured anomaly. The positivity result is a formal property of a definition, not an empirical discovery. It is a small, exact step within a larger framework, not a new physical law.

/-- Schwinger term: a_e^(1) = α/(2π). -/
noncomputable def schwinger_term : ℝ :=
  1 / (codata_alpha_inverse * (2 * Real.pi))

theorem schwinger_term_positive : 0 < schwinger_term := by
  unfold schwinger_term
  exact div_pos one_pos (mul_pos (by norm_num) (mul_pos two_pos Real.pi_pos))

/-- Schwinger term is less than 0.002 (upper bound using π > 3). -/
theorem schwinger_lt_002 : schwinger_term < 0.002 := by
  unfold schwinger_term
  rw [div_lt_iff₀ (mul_pos (by norm_num) (mul_pos two_pos Real.pi_pos))]
  -- goal: 1 < 0.002 * (codata_alpha_inverse * (2 * π))
  -- = 0.002 × 137.036 × 2 × π = 0.548144π
  -- Since π > 3: 0.548144 × 3 = 1.6 > 1 ✓
  have hpi := Real.pi_gt_three
  nlinarith

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

What this page does not claim

This result does not prove the Schwinger term's numerical value matches experiment beyond the leading order. The framework does not derive the fine-structure constant from first principles. The positivity theorem does not imply the full electron anomaly is positive, as higher-order terms can be negative.

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: