row_electron_ae_schwinger_relative_residual
plain-language theorem explainer
The theorem establishes that the absolute relative residual between the leading Schwinger term for the electron anomalous magnetic moment and the CODATA experimental value is strictly less than 0.003. A researcher comparing Recognition Science QED predictions to precision measurements would reference this bound to quantify one-loop agreement. The short term-mode proof invokes the certified interval on the leading term, rewrites the target inequality using positivity of the CODATA constant, and discharges both sides by linear arithmetic.
Claim. Let $a_e^{(1)} = α/(2π)$ be the leading Schwinger term and let $a_e^{CODATA} = 0.00115965218059$ be the CODATA electron anomalous magnetic moment. Then $|a_e^{(1)} - a_e^{CODATA}| / a_e^{CODATA} < 0.003$.
background
In the Electron g-2 Score Card module the leading term is defined as row_electron_ae_leading := alpha / (2 * Real.pi), the one-loop Schwinger contribution. The CODATA reference value is the constant row_electron_ae_codata := 0.00115965218059. The module proves that this leading term lies inside the open interval (0.001161, 0.001162) by the bracket theorem row_electron_ae_leading_bracket, which is assembled from separate lower and upper bounds. The local setting is Phase 1 row P1-C05 of the physical derivation plan, where the Schwinger term alone is shown to lie within 0.3 percent of the measured anomaly before higher-order loops are incorporated.
proof idea
The proof names the bracket theorem row_electron_ae_leading_bracket as hb. It rewrites the target inequality with div_lt_iff₀ applied to the positivity theorem row_electron_ae_codata_pos and expands the absolute value via abs_lt. After unfolding the definition of row_electron_ae_codata, the two-sided inequality is discharged by constructor and nlinarith on the two bounds supplied by hb.
why it matters
This result is invoked directly by electronGMinus2ScoreCardCert_holds to populate the schwinger_residual field of the ElectronGMinus2ScoreCardCert structure, thereby certifying that the scorecard is nonempty. It closes the Phase 1 claim that the RS-derived leading term a_e^(1) = α/(2π) agrees with CODATA to better than 0.3 percent, using the certified alpha interval. The full g-2 series remains partial because higher-order terms have not yet been derived from RS primitives; the present bound quantifies the residual for the Schwinger slice alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.