amplitude_vanishes_under_cancellation
plain-language theorem explainer
The theorem establishes that the leading s² contribution to longitudinal vector-boson scattering vanishes identically once the gauge-exchange residue and scalar-exchange residue sum to zero. High-energy physicists studying electroweak unitarity bounds cite this identity to confirm the structural role of the Higgs in restoring perturbative consistency. The proof is a direct algebraic reduction obtained by unfolding the amplitude and cancellation definitions, rewriting the hypothesis, and simplifying with the ring tactic.
Claim. If the gauge-exchange residue $a_g$ and scalar-exchange residue $a_s$ satisfy $a_g + a_s = 0$, then the leading $s^2$ term in the longitudinal vector-boson scattering amplitude vanishes: $A_2(a_g, a_s, v, s) = 0$.
background
The module formalizes high-energy longitudinal vector-boson scattering $W_L^+ W_L^- → W_L^+ W_L^-$ (and ZZ analogs). Without a scalar resonance the gauge-exchange diagrams produce an amplitude that grows as $s^2/v^4$ and violates perturbative unitarity above roughly 1 TeV. The CancellationCondition is the algebraic requirement that the gauge-exchange residue plus the scalar-exchange residue equals zero, which exactly cancels the leading bad term and leaves a bounded amplitude.
proof idea
The proof is a one-line wrapper that unfolds the definitions of amplitudeS2 and CancellationCondition, rewrites the hypothesis into the expression, and reduces the resulting polynomial to zero via the ring tactic.
why it matters
The result is invoked by amplitude_bounded_of_cancellation to obtain the uniform bound and by longitudinalVectorScatteringCert to certify that the RS theory satisfies the cancellation under the HiggsEFTBridge normalization. It supplies the schema-level content of the Lee-Quigg-Thacker identity and of the claim that RS preserves longitudinal unitarity. The module leaves open a fully kinematic four-point amplitude with Mandelstam variables and helicity decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.