pdg_a_e
plain-language theorem explainer
This definition supplies the CODATA placeholder value 0.00115965218073 for the electron anomalous magnetic moment a_e. Researchers comparing RS universal corrections to experimental lepton data would reference it when testing mass-independent predictions. It is introduced as a direct noncomputable constant assignment with no derivation steps.
Claim. The empirical reference value for the electron anomalous magnetic moment is defined by $a_e = 0.00115965218073$.
background
The module treats anomalous moments a_l = (g-2)/2 for charged leptons via the φ-ladder residue mechanism. All leptons carry the same gauge charge Q = -1 and therefore the same Z = 1332, so the RS correction term is identical for e, μ, and τ. The full a_l combines the Schwinger term, higher QED loops, and this universal RS_correction; observed values differ only through mass-dependent loops.
proof idea
This is a direct constant definition that assigns the literal real number 0.00115965218073 to pdg_a_e with no lemmas or tactics applied.
why it matters
The constant anchors the empirical side of the module's universality claim that the RS correction to a_e equals the correction to a_τ. It supports the φ-ladder prediction of a mass-independent RS contribution to lepton moments, with the small observed difference (PDG a_e ≈ 1.16e-3, a_τ ≈ 1.17e-3) attributed to loops outside the RS core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.