amplitudeS2
plain-language theorem explainer
The leading high-energy s²/v⁴ coefficient in longitudinal WW → WW scattering is defined as the sum of gauge-exchange and scalar-exchange residues times s²/v⁴. High-energy physicists studying perturbative unitarity in electroweak theory cite this when deriving the Lee-Quigg-Thacker bound. The definition is a direct algebraic combination of the two amplitude contributions without further computation.
Claim. The coefficient of the leading high-energy term in the longitudinal vector-boson scattering amplitude is $(a_0 + a_1) s^2 / v^4$, where $a_0$ is the gauge-exchange residue and $a_1$ is the scalar-exchange residue.
background
In the Recognition Science treatment of the Standard Model, longitudinal vector-boson scattering provides a direct test of the Higgs mechanism. The module parametrizes the high-energy amplitude by a gauge-exchange residue and a scalar-exchange residue. The total leading coefficient is their sum. The local setting is the high-energy limit of W_L W_L → W_L W_L scattering, where without cancellation the amplitude grows as s²/v⁴ and violates unitarity above the TeV scale. The Higgs scalar must cancel this growth exactly. Upstream results supply the generic S-matrix element definition and the superposition principle for amplitudes.
proof idea
This declaration is a direct definition that encodes the sum of the gauge and scalar contributions to the s² term in the amplitude. No lemmas are applied; the expression is written explicitly as (a_gauge + a_scalar) * s² / v⁴.
why it matters
This definition supplies the explicit form of the dangerous s²/v⁴ term that is cancelled by the Higgs in the Standard Model. It is used by the theorems amplitude_bounded_of_cancellation and amplitude_bounded_under_SM_hypothesis to establish boundedness when a_gauge + a_scalar = 0. It also appears in the master certificate LongitudinalVectorScatteringCert. In the Recognition framework this captures the structural identity behind the Lee-Quigg-Thacker cancellation, linking the scalar coupling from the J-cost geometry to electroweak gauge symmetry. It supports the claim that RS preserves longitudinal unitarity. The open question is a full kinematic four-point amplitude with Mandelstam variables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.