schwinger_positive
The theorem establishes that the Schwinger term, defined as the fine-structure constant divided by 2π, is strictly positive. Researchers resolving the muon g-2 discrepancy via the Recognition Science φ-ladder would cite it as the second step in the EA-001 positivity chain. The proof is a one-line wrapper that unfolds the definition and invokes the positivity of division together with the already-proved positivity of alpha_em.
claim$α / (2π) > 0$, where $α$ is the fine-structure constant.
background
In the EA-001 module the muon g-2 anomaly is addressed by deriving the RS prediction for the anomalous magnetic moment from the φ-ladder. The Schwinger term is introduced as the leading QED contribution α/(2π). Its positivity is established immediately after the companion result that alpha_em itself is positive. The local setting is the full RS derivation that replaces the 4.2σ discrepancy with an explicit ladder-based expression.
proof idea
The term-mode proof unfolds the definition of schwinger_term to obtain alpha_em / (2 * Real.pi), then applies the library lemma div_pos. The first hypothesis is discharged by the upstream theorem alpha_em_pos; the second hypothesis is discharged by the tactic positivity on the constant 2π.
why it matters in Recognition Science
This result feeds directly into anomaly_dissolved, which concludes that the RS prediction a_mu_rs_prediction is positive and thereby dissolves the g-2 anomaly. It occupies the second slot in the EA-001 certificate and supplies the positivity needed for the subsequent comparison with the standard-model reference. The step aligns with the Recognition Science forcing chain at the point where electromagnetic constants are fixed on the φ-ladder.
scope and limits
- Does not compute a numerical value for the Schwinger term.
- Does not incorporate higher-order QED or electroweak corrections.
- Does not address experimental measurement uncertainties or lattice-QCD inputs.
- Does not derive the full muon anomalous moment expression.
Lean usage
theorem anomaly_dissolved : a_mu_rs_prediction > 0 := by unfold a_mu_rs_prediction; linarith [schwinger_positive, rs_counter_positive]formal statement (Lean)
31theorem schwinger_positive : schwinger_term > 0 := by
proof body
Term-mode proof.
32 unfold schwinger_term
33 apply div_pos
34 · exact alpha_em_pos
35 · positivity
36
37/-! ## II. The RS Counter-Term -/
38
39/-- The muon rung on the φ-ladder. -/