amplitude_bounded_of_cancellation
plain-language theorem explainer
In longitudinal vector-boson scattering the high-energy amplitude remains bounded for all Mandelstam s precisely when the gauge-exchange residue and scalar-exchange residue sum to zero. Particle physicists studying perturbative unitarity bounds or the structural role of the Higgs would cite the result to confirm that cancellation is necessary and sufficient at this order. The proof is a one-line term wrapper that invokes the vanishing lemma under the cancellation hypothesis and concludes with the trivial bound zero.
Claim. Let $a_g, a_s, v$ be real numbers satisfying the cancellation condition $a_g + a_s = 0$. Then there exists a real constant $M$ such that for every real $s$ the absolute value of the high-energy amplitude function satisfies $|A_2(a_g, a_s, v, s)| ≤ M$.
background
The module treats the high-energy limit of longitudinal vector-boson scattering $W_L^+ W_L^- → W_L^+ W_L^-$. The amplitude is parametrized by a gauge-exchange residue $a_g$ and a scalar-exchange residue $a_s$; the CancellationCondition is the proposition that these residues sum to zero, which removes the leading $s^2/v^4$ growth term. The local setting is the schema-level formalization of the Lee-Quigg-Thacker identity: the same scalar that generates longitudinal masses must couple so as to cancel the gauge contribution exactly.
proof idea
The term proof exhibits the bound constant zero. For arbitrary $s$ it rewrites the amplitude via the sibling lemma amplitude_vanishes_under_cancellation applied to the given CancellationCondition hypothesis, after which simp reduces the expression to zero and the inequality holds.
why it matters
The declaration supplies the general boundedness direction required for the RS-to-SM bridge. It feeds the conditional theorem amplitude_bounded_under_SM_hypothesis and the preservation statement RSPreservesLongitudinalUnitarity. In the Recognition framework it records that the J-cost geometry forces the scalar residue to match the gauge residue with opposite sign, thereby restoring high-energy unitarity without additional tuning. The module doc notes that a fully kinematic four-point amplitude with Mandelstam variables and helicity decomposition remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.