alpha_em
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from the Recognition functional equation.
- Does not incorporate experimental uncertainty bounds on the muon anomaly.
- Does not compute QED corrections beyond the leading Schwinger term.
- Does not address higher-rung mass formulas or Berry thresholds.
formal statement (Lean)
20noncomputable def alpha_em : ℝ := 1 / 137.036
proof body
Definition body.
21
22/-- **THEOREM EA-001.1**: alpha_em is positive. -/