electronGMinus2ScoreCardCert_holds
plain-language theorem explainer
The theorem proves that the ElectronGMinus2ScoreCardCert structure is inhabited, confirming the leading Schwinger term a_e^(1) = α/(2π) satisfies 0.001161 < a_e^(1) < 0.001162 with relative residual below 0.003 to the CODATA electron anomaly. Precision QED researchers would cite it when testing the RS-derived alpha interval against experimental data. The proof is a term that directly assembles the certificate from the bracket and residual lemmas.
Claim. There exists a certificate such that the leading Schwinger term satisfies $0.001161 < a_e^{(1)} < 0.001162$ and $|a_e^{(1)} - a_e^{CODATA}| / a_e^{CODATA} < 0.003$, where $a_e^{(1)} = α/(2π)$ and α lies in the certified RS interval.
background
The module treats the electron g-2 anomaly as phase 1 row P1-C05, isolating the leading term a_e^(1) = α/(2π) computed from the RS alpha inverse interval. The ElectronGMinus2ScoreCardCert structure packages two properties: the leading term must lie in (0.001161, 0.001162) and its relative deviation from the CODATA value must stay below 0.003. Upstream results supply the bracket via separate lower and upper bounds on the leading term and the residual via an absolute-value inequality that reduces to the codata positivity fact.
proof idea
The proof is a one-line term that constructs the ElectronGMinus2ScoreCardCert structure by supplying row_electron_ae_leading_bracket for the leading_bracket field and row_electron_ae_schwinger_relative_residual for the schwinger_residual field.
why it matters
This theorem certifies the leading-term slice of the electron g-2 score card in the Recognition Science plan, showing the Schwinger term matches CODATA within 0.3% once the RS alpha band is inserted. It sits downstream of the alpha constant derivation and the interval bounds on alpha inverse. The full g-2 row remains partial because higher-order loop terms have not yet been derived from RS primitives; the module explicitly flags this gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.