alpha_em_pos
The theorem establishes that the fine-structure constant defined as 1/137.036 is strictly positive. Researchers deriving the muon g-2 anomaly in Recognition Science cite this result to confirm the electromagnetic coupling is well-defined before Schwinger corrections. The proof reduces to unfolding the constant definition followed by numerical normalization.
claim$α_{em} > 0$ where $α_{em} := 1/137.036$.
background
The module EA-001 treats the muon g-2 anomaly, which shows a 4.2σ discrepancy, as resolved through φ-ladder calibration of constants. The upstream definition introduces alpha_em as the noncomputable real 1/137.036, serving as the base electromagnetic coupling for all subsequent positivity and correction steps in the derivation.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of alpha_em to expose the explicit fraction and applies norm_num to confirm the numerical inequality.
why it matters in Recognition Science
This result initiates the EA-001 certificate for the muon g-2 anomaly. It is invoked directly in the proof of schwinger_positive and appears in the ea001_certificate string. Within the Recognition framework it anchors the electromagnetic sector positivity before φ-ladder adjustments, consistent with the α^{-1} band near 137.
scope and limits
- Does not derive the numerical value of alpha_em from the Recognition functional equation.
- Does not incorporate φ-ladder rungs or mass formulas.
- Does not address higher-order QED corrections or the full anomaly calculation.
- Does not establish uniqueness of the constant within the RS framework.
Lean usage
theorem schwinger_positive : schwinger_term > 0 := by unfold schwinger_term; apply div_pos; exact alpha_em_pos; positivityformal statement (Lean)
23theorem alpha_em_pos : alpha_em > 0 := by
proof body
Term-mode proof.
24 unfold alpha_em
25 norm_num
26
27/-- The Schwinger term: α/(2π). -/