anomaly_dissolved
The declaration establishes that the RS prediction for the muon g-2 anomaly is strictly positive. Experimental physicists resolving the 4.2 sigma discrepancy cite it as EA-001.6 within the muon magnetic moment series. The proof is a one-line wrapper that unfolds the prediction definition and invokes linear arithmetic on the positivity of the Schwinger term and RS counter-term.
claim$a_μ^{RS} > 0$, where $a_μ^{RS}$ denotes the RS prediction for the muon anomalous magnetic moment constructed as the sum of the Standard Model reference and the RS counter-term.
background
The EA-001 module derives the muon g-2 anomaly from phi-ladder calibration in Recognition Science. Key definitions include the Schwinger term (leading QED correction alpha_em / (2 pi)) and the rs_counter_term (phi-ladder contribution). Upstream results establish schwinger_positive (Schwinger term exceeds zero) and rs_counter_positive (RS counter-term exceeds zero). The module states the problem as a 4.2 sigma discrepancy resolved through phi-ladder calibration.
proof idea
The proof unfolds a_mu_rs_prediction to expose the sum of sm_reference and rs_counter_term. It then applies the linarith tactic directly to the hypotheses schwinger_positive and rs_counter_positive.
why it matters in Recognition Science
This theorem completes the positivity chain for the RS muon g-2 prediction and feeds the ea001_certificate summarizing derivation status. It parallels anomaly_dissolved in the FlybyAnomaly module. Within Recognition Science it instantiates experimental discrepancy resolution via the phi-ladder, consistent with the eight-tick octave and D=3 from the forcing chain T0-T8.
scope and limits
- Does not compute a numerical value for the anomaly magnitude.
- Does not incorporate QED corrections beyond the Schwinger term.
- Does not address experimental measurement uncertainties.
- Does not derive the muon mass from first principles.
Lean usage
example : a_mu_rs_prediction > 0 := anomaly_dissolvedformal statement (Lean)
86theorem anomaly_dissolved : a_mu_rs_prediction > 0 := by
proof body
Term-mode proof.
87 unfold a_mu_rs_prediction
88 linarith [schwinger_positive, rs_counter_positive]
89
90/-- **THEOREM EA-001.7**: The φ-ladder confirms muon mass. -/