Physics Anomalous Magnetic Moment From Rs Gm Two Count

A count, not a value

The anomalous magnetic moment of the electron is the small deviation of the electron's magnetic strength from the value 2 that a simple quantum picture would predict. The measured difference, called g-2, is about 0.001159652, and explaining it requires the full machinery of quantum electrodynamics and the standard model. The Recognition Science library contains a theorem named gmTwoCount that is far narrower: it proves that a certain formal list of standard contributions has exactly five entries.

The five entries are named qed1loop, qed2loop, qed3loop, hadronic, and electroweak. These correspond to the five canonical families of corrections that physicists add up to get g-2: three successive rounds of quantum electrodynamics corrections, one set from hadronic (strong-force) effects, and one from electroweak (weak-force) effects. The theorem gmTwoCount states that the number of these entries is 5, and the proof is a direct computation by the machine-checked library of formal theorems. It does not compute any numerical value for g-2, and it does not claim that these five families are the only possible ones.

In Recognition Science, this count is part of a larger story about how the framework's cost function and its derived constants might connect to physics. The docstring in the source file sketches an attempt to relate g-2 to the framework's golden-ratio constant, but the numbers do not match the measured value, and the docstring itself records that the naive estimate is too large. The declaration gmTwoCount does not rescue that estimate; it only certifies the count of five contribution families.

The declaration also bundles a second, unrelated fact: a definition wolfensteinA sets a rational number to 9/11, and a theorem proves that this definition equals 9/11 by reflexivity. This is a definitional choice, not a derivation. The structure GMTwoCert packages the count and the Wolfenstein value together, and the definition gmTwoCert constructs that package. None of these declarations assert that the Wolfenstein parameter in the standard model is actually 9/11, nor that the five families produce the measured g-2.

What the declaration does establish, cleanly and verifiably, is a structural claim: the standard list of g-2 correction families, as formalized in this library, has exactly five members. That is a small but precise fact, and it is the whole content of gmTwoCount. The page should be read as a record of what the framework's library has checked, not as a claim about the measured value of g-2.

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

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

/-- Wolfenstein A = 9/11, leading to α_s predictions. -/
def wolfensteinA : ℚ := 9 / 11

What this page does not claim

gmTwoCount does not compute or predict any numerical value for g-2. The declaration does not assert that the five listed families are the only possible contributions to g-2. The definition wolfensteinA does not claim that the standard model's Wolfenstein parameter equals 9/11.

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: