row_electron_ae_leading_bracket
plain-language theorem explainer
The theorem establishes that the leading Schwinger term of the electron anomalous magnetic moment satisfies 0.001161 < α/(2π) < 0.001162. A physicist comparing RS-derived QED predictions to precision measurements would cite this interval for the first-order contribution. The proof is a one-line term that directly pairs the independently proved lower and upper bounds on the same quantity.
Claim. $0.001161 < α/(2π) < 0.001162$, where α is the fine-structure constant.
background
The Electron g-2 Score Card module addresses Phase 1 row P1-C05 by isolating the leading Schwinger term a_e^(1) = α/(2π). The noncomputable definition row_electron_ae_leading sets this equal to alpha / (2 * Real.pi). The module uses the certified RS interval for α^{-1} to obtain the numerical bracket, noting that this term alone lies within 0.3% of the CODATA electron anomaly while the full g-2 row remains partial pending higher-order terms.
proof idea
The proof is a term-mode construction that supplies the conjunction by pairing row_electron_ae_leading_lower with row_electron_ae_leading_upper.
why it matters
This bracket supplies the leading_bracket field inside the ElectronGMinus2ScoreCardCert constructed by electronGMinus2ScoreCardCert_holds and is invoked to bound the relative residual in row_electron_ae_schwinger_relative_residual. It fills the P1-C05 step of the physical derivation plan by delivering a certified numerical interval for the Schwinger term. In the Recognition framework it anchors the comparison of the RS alpha interval to the electron g-2, leaving derivation of the higher-order loop series as an open task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.