longitudinalVectorScatteringCert
plain-language theorem explainer
Longitudinal vector-boson scattering amplitudes decompose additively into gauge and scalar contributions, vanishing exactly when the cancellation condition holds. High-energy physicists would cite the resulting certificate to confirm that the RS scalar coupling restores perturbative unitarity above the TeV scale. The definition constructs the master certificate by directly assigning the four component theorems to the structure fields.
Claim. The certificate asserts that the total amplitude equals the sum of the gauge-exchange term and the scalar-exchange term for nonzero vacuum expectation value, that the amplitude vanishes identically when the gauge and scalar residues sum to zero, that the standard-model hypothesis implies this cancellation condition, and that the amplitude remains bounded at high energies under the standard-model hypothesis.
background
The module formalizes the high-energy behavior of longitudinal vector-boson scattering. Without a scalar resonance the gauge diagrams produce an amplitude that grows as s squared over v to the fourth and violates perturbative unitarity above roughly 1 TeV. The Higgs scalar supplies an exact counter-term that cancels the leading growth, leaving a bounded amplitude. This is the Lee-Quigg-Thacker identity at the schema level. Key definitions are the total amplitude as the sum of gauge-only and scalar-only pieces, the cancellation condition requiring the two residues to sum to zero, and the SM cancellation hypothesis that forces the residues to be equal in magnitude and opposite in sign. Upstream theorems establish the additive decomposition, the vanishing under the cancellation condition, the implication from the SM hypothesis to that condition, and boundedness of the amplitude under the hypothesis.
proof idea
The definition is a record construction that populates the four fields of the certificate structure by direct assignment: the decomposition theorem supplies the additive decomposition field, the vanishing theorem supplies the cancellation field, the SM-implication theorem supplies the SM-to-cancellation field, and a lambda that applies the boundedness theorem supplies the RS-boundedness field.
why it matters
This certificate is assembled into the master Higgs EFT low-energy limit certificate, completing the bundle of normalization, mass, Yukawa, and scattering results. It encodes the structural identity that the RS scalar coupling, extracted from the J-cost geometry, exactly cancels the gauge contribution and thereby preserves longitudinal unitarity. The module notes that a fully kinematic four-point amplitude with Mandelstam variables remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.