schwinger_term
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of alpha_em.
- Does not include higher-order QED or hadronic corrections.
- Does not establish positivity or numerical bounds.
- Does not reference the φ-ladder or rung structure.
formal statement (Lean)
28noncomputable def schwinger_term : ℝ := alpha_em / (2 * Real.pi)
proof body
Definition body.
29
30/-- **THEOREM EA-001.2**: The Schwinger term is positive. -/