LongitudinalVectorScatteringCert
plain-language theorem explainer
LongitudinalVectorScatteringCert packages four properties establishing that the total amplitude decomposes additively into gauge and scalar contributions, vanishes when the residues sum to zero, follows from the SM normalisation hypothesis, and remains bounded when the RS theory satisfies the opposite-residue condition. High-energy physicists checking unitarity restoration by a scalar resonance would cite the certificate when auditing the Lee-Quigg-Thacker mechanism inside an EFT bridge. The structure is assembled directly from four sibling le
Claim. Let $A(a_g,a_s,v,s)$ denote the longitudinal vector-boson scattering amplitude, $A_g(a_g,v,s)$ the gauge-exchange piece and $A_s(a_s,v,s)$ the scalar-exchange piece. The certificate asserts: (i) for $v≠0$, $A(a_g,a_s,v,s)=A_g(a_g,v,s)+A_s(a_s,v,s)$; (ii) if $a_g+a_s=0$ then $A(a_g,a_s,v,s)=0$; (iii) if $a_s=-a_g$ then $a_g+a_s=0$; (iv) if $a_s^{RS}=-a_g$ then there exists $M$ such that $|A(a_g,a_s^{RS},v,s)|≤M$ for all $s$.
background
The module encodes the high-energy behaviour of longitudinal vector-boson scattering $W_L^+W_L^-→W_L^+W_L^-$ (and ZZ analogues) as a test of the Higgs sector. CancellationCondition requires the gauge and scalar exchange residues to sum to zero at leading $s^2/v^4$ order. SMCancellationHypothesis encodes the canonical SM normalisation in which the scalar residue exactly negates the gauge residue. RSPreservesLongitudinalUnitarity states the analogous opposite-residue relation for the RS scalar coupling extracted from the J-cost geometry via the HiggsEFTBridge normalisation map.
proof idea
The declaration is a structure definition with no proof body. Its four fields are supplied by direct reference to the sibling lemmas amplitude_decomposition, amplitude_vanishes_under_cancellation, cancellation_of_SM_hypothesis and amplitude_bounded_under_SM_hypothesis; the downstream construction longitudinalVectorScatteringCert simply assembles those four lemmas into the certificate record.
why it matters
The certificate is consumed by HiggsEFTLowEnergyLimitCert as one component of the cost-geometry to SM-EFT bridge. It supplies the structural content of the claim that the RS scalar coupling (fixed by the J-cost Taylor expansion) restores longitudinal unitarity, thereby closing the loop from the Recognition Science forcing chain through the HiggsEFTBridge to perturbative consistency of the electroweak sector. The module doc notes that a fully kinematic four-point amplitude remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.