CancellationCondition
plain-language theorem explainer
The high-energy cancellation condition requires the gauge-exchange residue to equal the negative of the scalar-exchange residue at leading s² order in longitudinal vector-boson scattering. Particle physicists and Recognition Science formalizers cite it when proving that amplitudes remain bounded as s grows. The definition is introduced as a direct equality that immediately enables vanishing theorems for the leading term.
Claim. The cancellation condition holds precisely when $a_ {gauge} + a_{scalar} = 0$, where $a_{gauge}$ and $a_{scalar}$ are the residues of the gauge-exchange and scalar-exchange diagrams in the leading high-energy term of longitudinal vector-boson scattering amplitudes.
background
The module formalizes the Lee-Quigg-Thacker cancellation for processes such as $W_L^+ W_L^- → W_L^+ W_L^-$. Without a scalar, gauge and contact diagrams produce an amplitude that grows as $s^2 / v^4$ and violates perturbative unitarity above roughly 1 TeV. The Higgs scalar supplies an opposing residue that cancels this growth, leaving a bounded amplitude. The module parametrizes the high-energy amplitude by separate gauge and scalar residues and isolates the condition under which their sum vanishes.
proof idea
Direct definition of the equality $a_{gauge} + a_{scalar} = 0$. No lemmas or tactics are invoked; the body is the literal statement of the Prop.
why it matters
This definition supplies the hypothesis for amplitude_vanishes_under_cancellation and amplitude_bounded_of_cancellation, and is invoked by cancellation_of_RS_preservation and cancellation_of_SM_hypothesis. It encodes the structural identity that restores longitudinal unitarity in the Recognition Science setting, where the scalar coupling extracted from the J-cost geometry matches the gauge residue with opposite sign. The module documentation notes that a full kinematic four-point amplitude with Mandelstam variables remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.