amplitudeScalarOnly
plain-language theorem explainer
Scalar-only amplitude isolates the Higgs-exchange contribution to longitudinal vector-boson scattering. High-energy physicists cite the expression when decomposing amplitudes to check perturbative unitarity above the TeV scale. The definition is a direct algebraic assignment of the kinematic factor s squared over v to the fourth, multiplied by the scalar residue.
Claim. The scalar-exchange contribution to the amplitude is given by $a_0 s^2 / v^4$, where $a_0$ denotes the scalar residue, $s$ is the Mandelstam variable, and $v$ is the electroweak vacuum expectation value.
background
The module formalizes the high-energy behavior of longitudinal vector-boson scattering $W_L^+ W_L^- → W_L^+ W_L^-$ in the Recognition Science framework. Without a scalar resonance the gauge-exchange diagrams produce an amplitude that grows as $s^2 / v^4$ and violates perturbative unitarity above roughly 1 TeV. The scalar-exchange residue is parametrized separately so that the cancellation condition $a_g + a_s = 0$ can be stated cleanly. Upstream results on phi-forcing and spectral emergence supply the structural constraints that later fix the residues under the normalization hypothesis.
proof idea
This declaration is a one-line definition that directly encodes the scalar residue multiplied by the leading kinematic factor $s^2 / v^4$.
why it matters
It supplies the scalar term required by the amplitude decomposition theorem and by the master certificate LongitudinalVectorScatteringCert. The definition completes the schema-level statement of the Lee-Quigg-Thacker cancellation inside the RS setting. Under the HiggsEFTBridge normalization the J-cost geometry forces the scalar residue to equal the gauge residue with opposite sign, thereby preserving longitudinal unitarity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.