cancellation_of_SM_hypothesis
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not compute numerical values of the residues.
- Does not address full four-point kinematics or Mandelstam variables.
- Does not prove unitarity without the normalization hypothesis on v.
- Does not cover loop corrections or non-perturbative effects.
Lean usage
theorem use_cancellation (a_g a_s : ℝ) (h : SMCancellationHypothesis a_g a_s) : CancellationCondition a_g a_s := cancellation_of_SM_hypothesis a_g a_s hformal statement (Lean)
130theorem cancellation_of_SM_hypothesis
131 (a_gauge a_scalar : ℝ) (h : SMCancellationHypothesis a_gauge a_scalar) :
132 CancellationCondition a_gauge a_scalar := by
proof body
Term-mode proof.
133 unfold CancellationCondition SMCancellationHypothesis at *
134 rw [h]; ring
135
136/-- Under the SM cancellation hypothesis, the amplitude is bounded. -/