Physics Anomalous Magnetic Moment From Rs Gm Two Contribution

The five contributions

The anomalous magnetic moment of the electron is the small deviation of the electron's magnetic strength from the value a simple quantum theory would predict. Measured to about one part per trillion, the number g-2 ≈ 0.001159652 is one of the most precisely tested predictions in physics. Standard quantum electrodynamics (QED) builds it as a series of corrections: the first term is α/(2π), with α the fine-structure constant, and later terms add smaller refinements.

In the Recognition Science framework, a machine-checked library of formal theorems organizes these corrections into a single inductive type named GmTwoContribution. The type has exactly five constructors: qed1loop, qed2loop, qed3loop, hadronic, and electroweak. These correspond to the five canonical sources of the electron's anomalous moment: the first, second, and third loop orders of QED, the hadronic (quark and gluon) contributions, and the electroweak (W and Z boson) contributions. The library proves a theorem, gmTwoCount, that the cardinality of this type is exactly 5, by a direct computation with no axioms beyond the standard three.

The declaration also carries a separate definition, wolfensteinA, set to the rational number 9/11. This value is named after the Wolfenstein parameterization of the Cabibbo-Kobayashi-Maskawa matrix, which describes quark mixing; the library proves wolfensteinA_eq that this definition equals 9/11 by reflexivity. The structure GMTwoCert bundles both facts, the five-contribution count and the Wolfenstein value, into a single certificate object, and gmTwoCert constructs that certificate.

What the declaration does not do is compute the numerical value of g-2. The docstring notes a rough RS estimate, g-2 ≈ J(φ)/φ⁴ ≈ 0.0172, which is far too large compared to the measured value; it also sketches α ≈ 2/17 as a correction factor. Neither of these is a theorem in the library. The pack contains no proof that the RS expression equals the measured anomalous moment, and no claim that the five contributions sum to the accepted value. The formal content is limited to the count of five and the definition of 9/11.

What the declaration establishes, then, is a structural claim: the standard physics of the electron's anomalous moment has exactly five recognized sources, and the framework encodes that fact in a machine-checked way. It is a classification of contributions, not a derivation of the number. A reader should take from this page that the framework can mirror the accepted anatomy of a precision measurement, and that the numerical agreement, if any, remains an open question rather than a proved result.

theorem gmTwoCount : Fintype.card GmTwoContribution = 5 := by decide

def gmTwoCert : GMTwoCert where
  five_contributions := gmTwoCount
  wolfenstein := wolfensteinA_eq

inductive GmTwoContribution where
  | qed1loop | qed2loop | qed3loop | hadronic | electroweak
  deriving DecidableEq, Repr, BEq, Fintype

What this page does not claim

The declaration does not prove that the RS expression equals the measured anomalous magnetic moment. The declaration does not compute a numerical value for g-2 that matches experiment. The declaration does not derive the fine-structure constant α from first principles.

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