schwinger_term
plain-language theorem explainer
The declaration defines the Schwinger term as the fine-structure constant divided by 2π. Researchers modeling the muon g-2 anomaly cite this when assembling the leading QED piece of the RS prediction. The construction is a direct algebraic assignment from the module-local alpha_em value.
Claim. The Schwinger term is defined by $a^{(1)} = {a_e}^{(1)} = {a_μ}^{(1)} = α / (2π)$, where $α$ denotes the fine-structure constant.
background
Module EA-001 treats the muon g-2 anomaly as resolved through φ-ladder calibration in Recognition Science. The fine-structure constant is supplied by the sibling definition alpha_em = 1/137.036. This term isolates the leading QED contribution in the anomalous magnetic moment expansion.
proof idea
The definition is a direct assignment of the quotient alpha_em / (2 * Real.pi). It functions as a one-line wrapper with no lemmas or tactics applied.
why it matters
This supplies the base term for the positivity theorem and the SM reference value inside the same module, and for the suite of results in AnomalousMagneticMoment. It anchors the leading contribution in the RS treatment of the g-2 discrepancy, consistent with the alpha band in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.