row_electron_ae_codata_pos
plain-language theorem explainer
The theorem asserts strict positivity of the CODATA electron anomalous magnetic moment value. Precision QED comparisons cite it to bound relative residuals against the leading Schwinger term. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. $0 < a_e^{CODATA}$ where $a_e^{CODATA} := 0.00115965218059$ denotes the dimensionless CODATA electron anomalous magnetic moment.
background
The declaration belongs to the Electron g-2 Score Card module, which treats Phase 1 row P1-C05. The module proves bounds on the leading Schwinger term $a_e^{(1)} = α/(2π)$ via the certified RS alphaInv interval, yielding $0.001161 < a_e^{(1)} < 0.001162$, while the full CODATA anomaly is given as $a_e = 0.00115965218059...$. The upstream definition supplies the numerical constant: row_electron_ae_codata is the CODATA electron anomalous magnetic moment, dimensionless.
proof idea
The proof is a one-line wrapper that unfolds row_electron_ae_codata and applies norm_num to confirm positivity of the explicit constant 0.00115965218059.
why it matters
This result is invoked by row_electron_ae_schwinger_relative_residual to show that the absolute residual between the leading Schwinger term and the CODATA value, normalized by the CODATA value, is less than 0.003. It completes the basic positivity step inside the partial theorem for the electron g-2 row in the Recognition Science framework, where the Schwinger term alone lies within 0.3% of CODATA but the higher-order loop series has not yet been derived from RS primitives. The module notes the open question of constructing the missing loop terms from the RS/QED bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.