Physics Anomalous Moments Anomalous Moment

The anomalous moment

The anomalous magnetic moment of a charged lepton, written a_l = (g-2)/2, is the fractional deviation of a particle's magnetic strength from the value a simple quantum mechanical equation predicts. For the electron, muon, and tau, this tiny number is one of the most precisely measured quantities in physics. The leading contribution, the Schwinger term, comes from a single virtual photon loop and equals alpha/(2*pi), about 0.00116. Higher-order loops and mass-dependent effects add further corrections, so the measured values differ slightly between the three leptons: the electron's is about 0.001159652, the muon's about 0.0011659, and the tau's about 0.001177.

The Recognition Science (RS) framework, a formal system built from a discrete ledger of recognition events, models this quantity in its machine-checked library of formal theorems. Its declaration anomalous_moment defines the value as the Schwinger term plus a correction term that depends on a charge-derived integer Z. For all three leptons, which share the same electric charge Q = -1, this Z equals 1332, and therefore the correction term is identical. The framework proves a theorem, anomalous_e_tau_universal, stating that the anomalous moment of the electron equals that of the tau, purely from this shared Z. This is a statement about the framework's model, not a direct measurement of nature.

The framework's library also notes an empirical check: the measured electron and tau values, roughly 1.16e-3 and 1.17e-3, fall within the same broad band, consistent with a universal correction. But the framework does not claim to reproduce the precise measured values. Its model explicitly omits the mass-dependent higher-order loops that cause the electron and tau values to differ at the level of parts per million. The theorem proves equality in the model; the real-world difference is a known limitation, not a contradiction.

What the declaration does not claim is as important as what it proves. It does not derive the fine-structure constant alpha from first principles; the Schwinger term uses an external measured value as an anchor. It does not predict the exact measured anomalous moments of any lepton. It does not even claim that the electron and tau moments are equal in nature, only that the framework's universal correction term is identical for them. The single theorem is a statement about the model's internal consistency, a formal consequence of assigning the same charge to all leptons.

For a reader, the practical takeaway is a sharp one: the framework offers a structural explanation for why the anomalous moments of different leptons share a common correction, but it stops well short of a numerical prediction. The precise values remain the province of standard quantum electrodynamics and experiment. The framework's contribution is a formal, machine-checked statement of universality, not a new calculation of g-2.

/-- Universality: same dimless target from equal Z (φ-ladder). -/
theorem anomalous_e_tau_universal : anomalous_moment Lepton.e = anomalous_moment Lepton.tau := by
  simp [anomalous_moment, rs_correction, gap_lepton, Z_lepton]
  -- Z same ⇒ gap same

noncomputable def anomalous_moment (l : Lepton) : ℝ :=
  schwinger + rs_correction l  -- Higher loops mass-dependent, but RS universal

def Z_lepton (l : Lepton) : ℤ := 1332  -- From lepton map: q̃=-6, Z = q̃² + q̃⁴ = 36 + 1296 = 1332

What this page does not claim

The framework does not derive the fine-structure constant alpha from first principles. The framework does not predict the exact measured anomalous moments of any lepton. The theorem does not claim that electron and tau moments are equal in nature, only in the model.

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