CancellationCondition
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical values for the residues from any concrete Lagrangian.
- Does not address subleading terms in the s-expansion of the amplitude.
- Does not incorporate full Mandelstam-variable or helicity dependence.
- Does not prove the converse implication from boundedness to cancellation.
formal statement (Lean)
92def CancellationCondition (a_gauge a_scalar : ℝ) : Prop :=
proof body
Definition body.
93 a_gauge + a_scalar = 0
94
95/-- When the cancellation condition holds, the leading `s²` term vanishes
96 identically. -/