Physics Electron Gminus2 Score Card

The electron's magnetic moment

The electron's magnetic moment is a measure of how strongly the particle responds to a magnetic field. The anomaly, usually written a_e, is the tiny difference between the electron's actual magnetic moment and the value a simple spinning ball would have. It is one of the most precisely measured numbers in all of science. The CODATA 2022 value is a_e = 0.00115965218059, a number known to about one part in a trillion.

The theoretical prediction for this anomaly comes from quantum electrodynamics, the quantum theory of light and matter. The first and largest correction to the simple value was calculated by Julian Schwinger in 1948. It is a_e^(1) = α / (2π), where α is the fine-structure constant, the number that sets the strength of electromagnetic interactions. This single term already gets within 0.3% of the measured value. Adding more terms from higher-order loops in the theory improves the agreement dramatically, but those terms require a full QED calculation.

In Recognition Science, the framework's machine-checked library of formal theorems contains a module that proves the Schwinger term and brackets it. The module takes the framework's own certified interval for α and proves that 0.001161 < a_e^(1) < 0.001162. It then proves the relative difference between this leading term and the CODATA value is less than 0.003. Both statements are theorems, checked with zero errors and zero axioms beyond the standard logical ones.

The module is honest about its scope. It does not derive the full electron g-2 value. The higher-order loop series that would complete the prediction has not yet been derived from the framework's primitives. The status is PARTIAL_THEOREM. The falsifier is explicit: if CODATA a_e moved outside the stated residual band for the Schwinger-only slice, or if the missing loop terms could not be derived from the framework's bridge to QED, the claim would fail.

What this establishes in plain language is that the framework's derived value of α, when fed into the standard first-order formula, lands within a few parts per thousand of the measured electron anomaly. It is a consistency check between two independent parts of the framework: the derived coupling constant and the physics of the electron. It does not claim to explain the full anomaly, only to certify the first term.

theorem row_electron_ae_leading_bracket :
    (0.001161 : ℝ) < row_electron_ae_leading ∧
      row_electron_ae_leading < (0.001162 : ℝ) :=
  ⟨row_electron_ae_leading_lower, row_electron_ae_leading_upper⟩

theorem row_electron_ae_schwinger_relative_residual :
    |row_electron_ae_leading - row_electron_ae_codata| /
      row_electron_ae_codata < (0.003 : ℝ) := by
  have hb := row_electron_ae_leading_bracket
  rw [div_lt_iff₀ row_electron_ae_codata_pos, abs_lt]
  unfold row_electron_ae_codata
  constructor <;> nlinarith [hb.1, hb.2]

What this page does not claim

This module does not derive the full electron g-2 value, only the leading Schwinger term. The framework's α is not a free parameter fitted to the electron anomaly; it is derived elsewhere and used here. The 0.3% agreement is a consistency check, not a derivation of the complete anomaly.

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/ElectronGMinus2ScoreCard.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: