amplitude_decomposition
plain-language theorem explainer
The amplitude decomposition identity asserts that the total leading high-energy coefficient in longitudinal WW scattering equals the sum of its gauge-exchange and scalar-exchange pieces. High-energy physicists studying perturbative unitarity in electroweak theory cite this when confirming the structural cancellation required by the Higgs mechanism. The proof proceeds by direct unfolding of the three amplitude definitions followed by field simplification after verifying that the fourth power of the vacuum expectation value is nonzero.
Claim. For real numbers $a_g, a_s, v, s$ with $v ≠ 0$, the high-energy scattering amplitude coefficient $(a_g + a_s) s^2 / v^4$ equals $a_g s^2 / v^4 + a_s s^2 / v^4$.
background
The module formalizes longitudinal vector-boson scattering $W_L^+ W_L^- → W_L^+ W_L^-$, where the amplitude grows as $s^2/v^4$ without a scalar resonance and violates unitarity above ~1 TeV. The Higgs scalar exchange supplies the exact counter-term. Upstream definitions give amplitudeS2$(a_g, a_s, v, s) := (a_g + a_s) s^2 / v^4$ as the leading coefficient, amplitudeGaugeOnly$(a_g, v, s) := a_g s^2 / v^4$ as the gauge piece, and amplitudeScalarOnly$(a_s, v, s) := a_s s^2 / v^4$ as the scalar piece. The module states that the cancellation condition is $a_g + a_s = 0$ and that boundedness as $s → ∞$ holds exactly when this condition is met.
proof idea
The term-mode proof unfolds amplitudeS2, amplitudeGaugeOnly, and amplitudeScalarOnly. It introduces the auxiliary fact that $v^4 ≠ 0$ from the hypothesis $v ≠ 0$, then applies field_simp to equate both sides.
why it matters
This decomposition is invoked by longitudinalVectorScatteringCert to assemble the full cancellation certificate. It supplies the schema-level additive identity in the module's formalization of the Lee-Quigg-Thacker cancellation. In the Recognition Science framework it supports the claim that the RS scalar coupling extracted from the J-cost geometry restores high-energy unitarity in the electroweak sector, consistent with the eight-tick octave and D = 3. 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.