row_electron_ae_leading_eq
plain-language theorem explainer
The equality equates the leading Schwinger term for the electron anomaly to the reciprocal of twice pi times the RS inverse fine-structure constant. QED precision tests and Recognition Science constant derivations would cite it to anchor the anomaly formula in the certified alphaInv. The proof is a one-line algebraic reduction that unfolds the leading-term definition and alpha then cancels via field simplification.
Claim. The leading electron anomaly term satisfies $a_e^{(1)} = 1/(2 pi alpha^{-1})$, where $alpha^{-1}$ is the Recognition Science inverse fine-structure constant.
background
The Electron g-2 Score Card module treats the leading Schwinger term as the Phase 1 row P1-C05. The definition row_electron_ae_leading expands to alpha divided by 2 pi, with alpha defined as the reciprocal of alphaInv. The constant alphaInv is the dimensionless inverse fine-structure constant obtained from the structural seed via alpha_seed times exp of minus f_gap over alpha_seed. Positivity of alphaInv is supplied by the local alphaInv_pos theorem, which reduces to linarith on alphaInv_gt.
proof idea
The term-mode proof first unfolds row_electron_ae_leading and alpha to expose the rational expression 1/alphaInv over 2 pi. It then invokes field_simp with the hypotheses ne_of_gt alphaInv_pos and Real.pi_ne_zero to clear the nonzero denominators and obtain the target reciprocal form.
why it matters
The equality is invoked directly by the downstream bounds row_electron_ae_leading_lower and row_electron_ae_leading_upper that certify the interval 0.001161 < a_e^(1) < 0.001162. It realizes the P1-C05 slice of the physical derivation plan by linking the RS-derived alphaInv to the textbook Schwinger formula. The module notes that the full electron g-2 row stays PARTIAL_THEOREM until the higher-order loop series is derived from RS primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.