Physics Anomalous Magnetic Moment

The electron g-factor

The electron anomalous magnetic moment is the small measured excess of the electron's g-factor above the Dirac value of 2. In Recognition Science the module AnomalousMagneticMoment.lean takes the CODATA 2018 inverse fine-structure constant, 137.035999084, as a physical input and derives the leading correction to the g-factor from it. The module does not derive that coupling constant; it uses the measured value because Recognition Science does not supply one.

The leading term is the Schwinger term, defined as 1 divided by the product of the inverse coupling and 2π. The module proves this term is positive and less than 0.002, and that the electron g-factor, defined as 2 plus twice this term, is strictly greater than 2. These are theorems, statements checked by the Lean kernel, not empirical fits.

The module also records the known quantum electrodynamics coefficients for the anomalous moment: 0.5 at first order, -0.32848 at second, and 1.18124 at third. It proves the first coefficient is exactly one half. The eight-tick structure of Recognition Science appears as a lemma that the eight phase exponentials sum to zero, with the first phase equal to one, which is a structural fact about the framework's cycle, not a contribution to the magnetic moment value.

The plain-language consequence is that Recognition Science can reproduce the leading quantum correction to the electron's magnetic moment, but only by taking the fine-structure constant as an input. The module establishes bounds and positivity for that correction, and it does not claim to derive the coupling or the full experimental value.

MODEL codata_alpha_inverse · schwinger_term · IndisputableMonolith/Physics/AnomalousMagneticMoment.lean

THEOREM schwinger_in_range · IndisputableMonolith/Physics/AnomalousMagneticMoment.lean

THEOREM g_exceeds_dirac · IndisputableMonolith/Physics/AnomalousMagneticMoment.lean

THEOREM c1_half · IndisputableMonolith/Physics/AnomalousMagneticMoment.lean

What this page does not claim

Not a derivation of the fine-structure constant from Recognition Science principles. Not a derivation of the full measured electron anomalous magnetic moment. Not a claim that the eight-tick structure contributes numerically to the magnetic moment.

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