anomaly_dissolved
plain-language theorem explainer
Recognition Science predicts a positive muon g-2 anomaly value under φ-ladder calibration. Experimentalists auditing the 4.2σ discrepancy would cite this when arguing the excess is accounted for by the RS counter-term. The proof unfolds the composite prediction and applies linear arithmetic to two established positivity results.
Claim. The Recognition Science prediction for the muon anomalous magnetic moment satisfies $a_μ^{RS} > 0$, where $a_μ^{RS}$ is the sum of the Standard Model reference and the RS counter-term.
background
The module EA-001 treats the muon g-2 anomaly as a ~4.2σ discrepancy resolved by φ-ladder calibration of the muon mass rung. The key definition constructs the RS prediction as the Standard Model reference plus an RS counter-term derived from the ladder gap factor at the muon rung. Upstream results establish the required positivity: the Schwinger term exceeds zero by direct division of positive α_em over π, and the RS counter-term exceeds zero by the same positivity argument on α_em.
proof idea
The proof unfolds a_mu_rs_prediction to expose the sum of the SM reference and RS counter-term. It then applies the linarith tactic directly to the lemmas schwinger_positive and rs_counter_positive, which together force the linear combination to be positive.
why it matters
This theorem finishes the EA-001 derivation and is invoked by the EA-001 certificate as well as the parallel anomaly_dissolved result in the FlybyAnomaly module. It realizes the RS resolution of the muon discrepancy through the φ-ladder mass formula, consistent with the eight-tick octave and D=3 in the forcing chain. The result supports the broader claim that the counter-term accounts for the observed excess without beyond-Standard-Model additions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.