Physics Anomalous Magnetic Moment From Rs Gmtwo Cert

What GMTwoCert records

The anomalous magnetic moment of the electron, written g-2, is the small measured departure of the electron's magnetic behavior from the value a simple Dirac equation predicts. The leading term is α/(2π), about 0.00116, and the full measured value is about 0.001159652. In the Recognition Science framework, the declaration GMTwoCert (a machine-checked certificate, a formal record that a proof checker has verified) records two structural facts about this quantity.

First, it names the five standard physical contributions that enter the calculation: one-loop QED, two-loop QED, three-loop QED, hadronic, and electroweak. The certificate proves the count is exactly five, as a theorem in the framework's machine-checked library of formal theorems. Second, it fixes the Wolfenstein parameter A to the rational value 9/11. The Wolfenstein parametrization is a standard way of writing the Cabibbo-Kobayashi-Maskawa matrix, which describes how quarks mix between mass and flavor states.

The certificate does not derive the measured g-2 value. The framework's own exploratory estimate, using its golden-ratio cost function, lands at about 0.0172, which is far from the measured 0.001159652, and the docstring says so plainly. The certificate instead records the number of contributions and the Wolfenstein choice as a structural scaffold. The five-way split matches the standard physics decomposition; the 9/11 choice is a definitional identification, not a derived result.

What the certificate establishes is a clean, machine-checked statement about the shape of the calculation: five named pieces, one rational parameter. It is a small piece of bookkeeping, not a numerical prediction. The measured value remains an empirical input, and the gap between the framework's rough estimate and experiment is openly acknowledged in the source itself.

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

theorem wolfensteinA_eq : wolfensteinA = 9 / 11 := rfl

structure GMTwoCert where
  five_contributions : Fintype.card GmTwoContribution = 5
  wolfenstein : wolfensteinA = 9 / 11

What this page does not claim

The certificate does not prove the measured value of the anomalous magnetic moment. The Wolfenstein value 9/11 is not derived from the framework's axioms. The five contributions are named, not shown to be complete or sufficient for the full calculation.

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: