schwinger
plain-language theorem explainer
The schwinger definition supplies the leading QED term α/(2π) as the baseline for lepton anomalous magnetic moments. Researchers modeling g-2 would cite it before layering φ-ladder residues that are universal across e, μ, τ. The definition is a direct one-line assignment that pulls the fine-structure constant from the Constants module and divides by 2π.
Claim. The Schwinger term is defined as $a_S = α / (2π)$, where $α$ is the fine-structure constant.
background
This module extends the φ-ladder residue mechanism to QED anomalous moments a_l = (g-2)/2. All charged leptons share gauge charge Q=-1 and thus the same Z=1332, so the RS correction term is identical for e, μ, τ. The full expression is a_l = Schwinger + higher loops + RS_correction, with the RS part drawn from the gap function (product of closure and Fibonacci factors, equal to 45) and the Z map (integer assignment for anchor relations by sector and charge).
proof idea
The definition is a one-line wrapper that divides the fine-structure constant α (imported from Constants.Alpha) by 2π.
why it matters
This supplies the baseline Schwinger term that feeds directly into the anomalous_moment definition for any lepton. It fills the QED component of the full a_l expression while the RS part remains universal from equal Z. In the Recognition framework it sits inside the alpha band and connects to the φ-ladder corrections that originate from T5 J-uniqueness and T6 phi fixed point; it touches the open question of matching the predicted a_e to PDG values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.