SMCancellationHypothesis
plain-language theorem explainer
The declaration introduces the standard-model cancellation hypothesis as the equality of the scalar residue to the negative gauge residue in longitudinal vector scattering. Researchers formalising unitarity restoration in the Higgs sector would invoke it to prove amplitude bounds. The definition is a direct equality that downstream results apply without further reduction.
Claim. The standard-model normalisation hypothesis asserts that the scalar-exchange residue equals the negative of the gauge-exchange residue: $a_ {scalar} = -a_{gauge}$.
background
The module decomposes the high-energy amplitude for longitudinal vector-boson scattering into gauge-exchange and scalar-exchange residues. The cancellation condition requires their sum to vanish so that the amplitude remains bounded rather than growing as $s^2/v^4$. This hypothesis encodes the canonical SM normalisation in which the Higgs scalar supplies the precise counter-term required by the Lee-Quigg-Thacker mechanism. The module states that under the normalisation map from HiggsEFTBridge the RS scalar coupling satisfies the same relation.
proof idea
The declaration is a direct definition of the proposition as the equality $a_{scalar} = -a_{gauge}$. No lemmas are applied; it functions as the hypothesis interface for the cancellation theorems.
why it matters
This hypothesis is the key assumption in amplitude_bounded_under_SM_hypothesis and cancellation_of_SM_hypothesis, which establish boundedness when the condition holds. It connects to the Recognition Science claim that the RS scalar coupling derived from the J-cost geometry satisfies the same cancellation, thereby preserving longitudinal unitarity. The module leaves open the full four-point kinematic amplitude with Mandelstam variables and helicity decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.