row_electron_ae_codata
plain-language theorem explainer
The declaration supplies the CODATA experimental value for the dimensionless electron anomalous magnetic moment a_e. Researchers comparing Recognition Science predictions to precision QED measurements cite this constant as the benchmark in the g-2 scorecard. It is introduced as a direct numerical definition without further computation or derivation.
Claim. The CODATA value of the electron anomalous magnetic moment is $a_e = 0.00115965218059$.
background
In the Electron g-2 Score Card module the definition records the experimental reference for the anomaly. The module centers on the leading Schwinger term $a_e^{(1)} = α/(2π)$ obtained from the certified RS alpha inverse interval, which brackets between 0.001161 and 0.001162 and lies within 0.3 percent of the CODATA figure. The full g-2 row remains partial because higher-order loop terms have not yet been derived from RS primitives.
proof idea
The definition directly assigns the fixed numerical value 0.00115965218059. No lemmas or tactics are applied; the entry functions as a hardcoded experimental input for residual calculations.
why it matters
This constant anchors the ElectronGMinus2ScoreCardCert structure and the row_electron_ae_schwinger_relative_residual theorem, which certifies the bracket on the leading term and the relative residual below 0.003. It implements the experimental benchmark for Phase 1 row P1-C05, permitting direct comparison of the RS Schwinger term to measurement. The open question remains derivation of the complete QED series from the J-function and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.