Physics Anomalous Moments Lepton

The Lepton Declaration

The magnetic moment of a charged particle measures how strongly it responds to a magnetic field. For a point-like electron, quantum electrodynamics predicts a value slightly different from the classical Dirac value; that difference is the anomalous magnetic moment, written a = (g-2)/2. The electron's measured value is about 0.001159652, and the muon's is about 0.0011659, while the tau's is far harder to measure directly. In 1948, Julian Schwinger calculated the first and largest correction, the famous one-loop term α/(2π), where α is the fine-structure constant.

In Recognition Science, the ledger (a discrete record of recognition events) assigns each charged lepton a charge number Z = 1332, the same for all three because they share the same electric charge. The framework's library, a machine-checked collection of formal statements, defines the Lepton type with three members, e, mu, and tau, and defines the anomalous moment as the Schwinger term plus a correction derived from that shared Z. The central result, anomalous_e_tau_universal, proves that the electron and tau receive exactly the same correction: anomalous_moment e = anomalous_moment tau. This is a formal equality, not a numerical coincidence, because the correction depends only on Z, and Z is identical for both.

The framework's claim is narrow. It does not derive the full measured anomalous moments, which differ measurably between leptons because of mass-dependent higher-order loop corrections. The library includes the measured electron value as a placeholder and notes that the predicted universal correction lands near the measured values for the electron and tau, within their experimental bands, but this is an empirical observation, not a formal result. The declaration establishes a structural universality: equal charge implies equal correction in this model. It leaves the full mass-dependent story to conventional physics, which the framework treats as itself derived from deeper structure.

What this means for a reader is that the Lepton declaration is a proof of a clean symmetry, not a complete theory of anomalous moments. The formal result guarantees that any difference between the electron and tau anomalies must come from something other than the shared charge structure, namely the mass-dependent loops. The framework's contribution is to isolate one universal piece and prove it identical across all three leptons, a fact that would be invisible if the Schwinger term were the whole story.

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

inductive Lepton | e | mu | tau

/-- Empirical note: RS predicts universal correction; full a differs by mass-dependent loops (PDG a_e ≈ 1.16e-3, a_τ ≈ 1.17e-3 within bands). -/
@[simp] noncomputable def pdg_a_e : ℝ := 0.00115965218073  -- Placeholder CODATA

What this page does not claim

The declaration does not prove the full measured anomalous moments, which differ due to mass-dependent loops. The declaration does not derive the fine-structure constant α from first principles. The declaration does not claim the empirical agreement with PDG values is a formal result.

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: