amplitude_bounded_under_SM_hypothesis
plain-language theorem explainer
Under the assumption that the scalar-exchange residue exactly cancels the gauge-exchange residue, the longitudinal vector-boson scattering amplitude remains bounded for all center-of-mass energies. High-energy physicists verifying perturbative unitarity in the Standard Model would cite this when confirming the Higgs mechanism restores high-energy behavior. The proof is a one-line wrapper that rewrites the amplitude via the vanishing lemma under the SM cancellation hypothesis and simplifies the absolute value to zero.
Claim. If $a_ {scalar} = -a_{gauge}$, then there exists a real number $M$ such that for every real $s$, $|A_2(a_{gauge}, a_{scalar}, v, s)| ≤ M$.
background
Longitudinal vector-boson scattering $W_L W_L → W_L W_L$ grows as $s^2/v^4$ without a scalar counter-term and violates perturbative unitarity above the TeV scale. The module parametrizes the amplitude by a gauge-exchange residue $a_{gauge}$ and a scalar-exchange residue $a_{scalar}$, with the cancellation condition $a_{gauge} + a_{scalar} = 0$. The SM cancellation hypothesis is the proposition that the scalar residue equals the negative of the gauge residue, as required by the Higgs mechanism for mass generation and unitarity restoration.
proof idea
The proof is a one-line wrapper. It supplies the bound zero, then for arbitrary $s$ rewrites the amplitude using the lemma amplitude_vanishes_under_cancellation instantiated by cancellation_of_SM_hypothesis, and applies simp to obtain the zero bound.
why it matters
This theorem is invoked inside longitudinalVectorScatteringCert to assemble the full certificate that the RS Higgs EFT bridge preserves longitudinal unitarity. It supplies the conditional statement that under the canonical normalization map of HiggsEFTBridge the RS scalar coupling produces exactly the opposite residue to the gauge term, realizing the Lee-Quigg-Thacker cancellation at the schema level. It closes one link in the RS-to-SM bridge while leaving a fully kinematic four-point amplitude open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.