Physics Anomalous Magnetic Moment Ae Leading Positive

The leading correction

The electron behaves like a tiny magnet, and its magnetic strength is described by a number called the g-factor. The Dirac equation, the relativistic quantum theory of the electron, predicts this factor is exactly 2. Measurements show it is actually a little more than 2, about 2.002319. The extra amount, written a_e, is the anomalous magnetic moment.

In 1948 Julian Schwinger calculated the first quantum correction to the g-factor. He found that a_e equals α/(2π), where α is the fine-structure constant, the number that sets the strength of electromagnetic interactions. This single term, about 0.00116, accounts for most of the measured anomaly. Later work added more terms in powers of α, and the full series now matches experiment to better than a part per trillion.

Inside the Recognition Science framework, the declaration ae_leading_positive states a simple fact about this first correction: it is greater than zero. The framework's machine-checked library of formal theorems proves this by taking the Schwinger term, defined as 1/(α_CODATA · 2π), and showing it is positive because α_CODATA and π are positive. The same library also proves the term is less than 0.002, using only the fact that π is greater than 3. Together these two bounds place the leading correction in a small positive interval.

The framework does not claim to derive the numerical value of α itself. Its library explicitly records that the fine-structure constant is an input taken from the CODATA 2018 measurement, not a number the framework produces. The declaration ae_leading_positive therefore does not predict the size of the anomaly; it only confirms the sign of the first term, a fact already known from physics for three quarters of a century.

theorem ae_leading_positive : 0 < ae_leading := schwinger_term_positive

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

What this page does not claim

The framework does not derive the fine-structure constant α; it takes the CODATA 2018 value as an input. The declaration does not predict the magnitude of the anomaly, only the sign of the leading term. The proof does not establish any value for higher-order terms in the α expansion.

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: