rs_counter_positive
plain-language theorem explainer
The RS counter-term for the muon g-2 anomaly equals the product of the fine-structure constant over pi, phi to the negative power of the muon rung, and the gap-1332 factor; this product is strictly positive. Modelers of the anomaly inside the Recognition Science framework cite the result to fix the sign of the phi-ladder correction. The proof unfolds the term definition then chains three positivity facts through two multiplications.
Claim. $ (α / π) ⋅ φ^{-r} ⋅ g > 0 $, where α ≈ 1/137.036 is the fine-structure constant, r = 13 is the muon rung on the φ-ladder, and g = 1/(1332 φ) is the gap-1332 resonance factor.
background
The EA-001 module derives the muon g-2 anomaly resolution via φ-ladder calibration. The fine-structure constant is introduced as the constant 1/137.036. The muon rung is fixed at 13. The gap-1332 factor is defined as the reciprocal of 1332 times phi. The counter-term is assembled as their product with division by pi. Upstream results establish positivity of the fine-structure constant, positivity of phi to any real power, and positivity of the gap factor itself.
proof idea
Unfold the counter-term definition. Prove positivity of alpha_em over pi by norm_num on the numerator and positivity on the denominator. Prove positivity of phi to the negative muon rung by rpow_pos_of_pos using the known positivity of phi. Import positivity of the gap factor directly. Apply mul_pos twice to the three positive factors.
why it matters
The result is invoked by rs_exceeds_sm to show the RS prediction lies above the SM reference and by anomaly_dissolved to conclude the anomaly dissolves. It supplies the sign confirmation required at step EA-001.4 of the muon g-2 derivation. The argument sits inside the φ-ladder construction that forces D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.