cancellation_of_SM_hypothesis
plain-language theorem explainer
The SM cancellation hypothesis sets the scalar-exchange residue equal to the negative of the gauge-exchange residue, which forces their sum to zero. High-energy physicists studying longitudinal vector-boson scattering cite this identity when checking perturbative unitarity above the TeV scale. The proof is a one-line algebraic reduction that unfolds the two definitions and applies ring simplification.
Claim. If the scalar-exchange residue satisfies $a_ {scalar} = -a_ {gauge}$, then the cancellation condition $a_ {gauge} + a_ {scalar} = 0$ holds.
background
In longitudinal vector-boson scattering the high-energy amplitude is parametrized by a gauge-exchange residue $a_ {gauge}$ and a scalar-exchange residue $a_ {scalar}$. The cancellation condition requires their sum to vanish, eliminating the leading $s^2/v^4$ growth. The SM cancellation hypothesis asserts that in the canonical Standard Model the scalar residue exactly equals the negative of the gauge residue, restoring asymptotic boundedness. This module formalizes the Lee-Quigg-Thacker identity at the schema level, showing that the same scalar giving mass to longitudinal modes must couple so as to cancel the dangerous term.
proof idea
The proof is a one-line wrapper. It unfolds CancellationCondition and SMCancellationHypothesis at the goal and hypothesis, rewrites the hypothesis into the goal, and applies ring to verify the resulting equality.
why it matters
This theorem supplies the direct implication from the SM hypothesis to the cancellation condition. It is invoked by amplitude_bounded_under_SM_hypothesis to obtain boundedness and by cancellation_of_RS_preservation to transfer the result to the RS setting. Within the Recognition framework it closes the structural step that links the J-cost geometry of the scalar to electroweak unitarity preservation, consistent with the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.