rs_exceeds_sm
plain-language theorem explainer
The RS prediction for the muon anomalous magnetic moment exceeds the Standard Model reference by the positive RS counter-term. Experimental physicists resolving the g-2 anomaly would cite this result to establish the RS resolution of the discrepancy. The proof is a one-line wrapper that unfolds the RS prediction definition and applies linear arithmetic to the positivity of the counter-term.
Claim. $a_μ^{RS} > a_μ^{SM}$, where $a_μ^{RS} := a_μ^{SM} + Δ_{RS}$ and $Δ_{RS} > 0$ is the RS counter-term.
background
In the EA-001 module the muon g-2 anomaly is treated by φ-ladder calibration of the RS prediction. The RS prediction is defined as the SM reference (Schwinger term plus hadronic seed 0.000711317) plus the RS counter-term. The separate positivity theorem shows the counter-term exceeds zero by verifying that the electromagnetic fine-structure constant divided by π is positive.
proof idea
The proof is a one-line wrapper. It unfolds the definition of the RS prediction to expose the addition of the positive counter-term to the SM reference, then invokes linarith on the positivity theorem for the counter-term.
why it matters
This theorem completes EA-001.5 and feeds directly into the EA-001 certificate declaring the anomaly derived in RS. It relies on φ-ladder calibration from the Recognition Science framework (T5 J-uniqueness and T6 phi fixed point) to produce the positive counter-term. It touches the open question of precise numerical agreement with experimental data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.