Physics Anomalous Moments Rs Correction

The RS correction term

The anomalous magnetic moment of a particle measures how its spin responds to a magnetic field, deviating from the simple value a classical spinning charge would have. For the electron, this deviation, written a_e = (g-2)/2, is one of the most precisely measured quantities in physics: the CODATA 2018 value is 0.00115965218073, a number known to better than one part in a trillion. The standard theoretical prediction sums contributions from quantum electrodynamics (QED), beginning with the famous Schwinger term, which alone gives about 0.0011614, with higher-order loop corrections bringing the total into agreement with experiment.

In the Recognition Science framework, the anomalous moment is modeled as a sum of two parts: the Schwinger term plus a correction term called rs_correction, a framework-specific adjustment. The framework defines this correction using a quantity called the gap, which is a discrete number derived from a particle's charge structure. For all three charged leptons (electron, muon, tau), the framework assigns the same charge-related integer, Z = 1332, and therefore the same gap and the same rs_correction value. The declaration rs_correction is simply this definition: it sets the correction equal to the gap for the given lepton.

In Recognition Science, the framework's library of machine-checked formal theorems proves one statement about this definition: the anomalous moment of the electron equals the anomalous moment of the tau lepton. This is a theorem because both are defined with the same Schwinger term and the same rs_correction, since Z is identical for both. The theorem is a formal consequence of the definitions, not an empirical claim about measured values. The framework's own documentation notes that the measured values differ: a_e is about 0.001159652, while a_tau is about 0.00117, a difference attributed to mass-dependent higher-order loops that the simplified model does not include.

What rs_correction does not claim is important. It does not claim to derive the full measured anomalous moment, nor does it claim that the electron and tau actually have identical measured moments. The declaration only establishes a definitional equality within the framework's model. The framework's library does not prove that rs_correction matches any experimental value; the empirical comparison is left as a note, not a theorem. The declaration also does not claim to derive the Schwinger term itself, which is taken as an external anchor from CODATA data.

The practical consequence is that the framework offers a universal, charge-based correction for all leptons, but the model's simplicity means it cannot account for the mass-dependent loop corrections that distinguish the electron from the tau in reality. The theorem about equality between electron and tau holds within the framework's definitions, but it does not survive contact with the full measured physics.

noncomputable def rs_correction (l : Lepton) : ℝ := gap_lepton l

-- Full anomalous moment: Schwinger + placeholder higher + universal RS

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

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

What this page does not claim

The rs_correction declaration does not derive the full measured anomalous moment from first principles. The theorem anomalous_e_tau_universal does not claim that the measured electron and tau moments are equal. The Schwinger term is taken as an external anchor, not derived within the framework.

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: