alpha_em_pos
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.