ElectronGMinus2ScoreCardCert
plain-language theorem explainer
The structure packages two inequalities certifying that the leading Schwinger term alpha over 2 pi lies strictly between 0.001161 and 0.001162 while its relative deviation from the CODATA electron anomaly remains below 0.003. Researchers deriving QED observables from Recognition Science alpha intervals would cite this certificate to validate the P1-C05 row. It is realized as a structure definition whose fields are later instantiated by separate lemmas on the numerical bracket and the residual inequality.
Claim. Let $a_e^{(1)} := alpha / (2 pi)$ denote the leading Schwinger term and let $a_e^{codata} := 0.00115965218059$ be the CODATA value. The structure certifies the conjunction of $0.001161 < a_e^{(1)} < 0.001162$ and $|a_e^{(1)} - a_e^{codata}| / a_e^{codata} < 0.003$.
background
This module addresses Phase 1 row P1-C05 of the physical derivation plan, isolating the leading term of the electron anomalous magnetic moment. The leading term is defined as alpha divided by 2 pi using the certified RS alpha interval; the CODATA value is the experimental benchmark 0.00115965218059. Upstream, row_electron_ae_leading computes the RS prediction while row_electron_ae_codata records the measured anomaly; the structure packages the two inequalities that hold for these quantities.
proof idea
The declaration is a structure definition with two fields. The leading_bracket field asserts the open numerical interval for the leading term. The schwinger_residual field asserts the relative error bound below 0.003. No lemmas or tactics appear inside the definition; the fields are populated downstream by the theorem that constructs an explicit inhabitant.
why it matters
This structure supplies the concrete numerical certificate for the leading Schwinger term in the electron g-2 scorecard. It is consumed by the theorem electronGMinus2ScoreCardCert_holds, which witnesses nonemptiness. In the Recognition Science framework it validates the P1-C05 row by confirming that the alpha interval produces a_e^(1) inside the stated bracket and within 0.3 percent of experiment, consistent with the T5 J-uniqueness and the alpha band. The open question it touches is the RS derivation of the higher-order loop series that would complete the full anomaly prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.