alpha_em
plain-language theorem explainer
alpha_em supplies the fine-structure constant as the fixed numerical input 1/137.036 for the RS muon g-2 counter-term. Experimental groups calibrating the anomaly against the φ-ladder would cite this value directly. The declaration is a plain constant assignment that downstream positivity and term lemmas unfold without further reduction.
Claim. The fine-structure constant satisfies $α = 1/137.036$.
background
The module derives the muon g-2 anomaly resolution via φ-ladder calibration, with the observed 4.2σ discrepancy addressed by RS-native constants. alpha_em enters the RS counter-term definition together with phi to the muon rung power and the gap_1332_factor. Upstream results supply the structural positivity and ledger properties that later theorems apply to this constant.
proof idea
Direct numerical definition with no lemmas or tactics applied.
why it matters
The definition anchors the EA-001 derivation by providing the input to alpha_em_pos, schwinger_term, rs_counter_term and rs_counter_positive. It sits inside the framework alpha band (137.030, 137.039) and supports the T5 J-uniqueness and eight-tick octave steps that calibrate the counter-term against the anomaly. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.