pith. sign in
module module high

IndisputableMonolith.StandardModel.LongitudinalVectorScattering

show as:
view Lean formalization →

This module defines the leading s²/v⁴ coefficient in longitudinal WW to WW scattering as the sum of gauge and scalar contributions, together with the cancellation condition that makes the coefficient vanish. High-energy physicists matching effective theories to unitarity bounds would cite it when checking consistency of the recognition-scale Higgs sector. The module consists of direct algebraic definitions for the decomposed amplitudes and short lemmas that substitute the SM hypothesis to obtain vanishing and boundedness.

claimThe high-energy coefficient of longitudinal vector-boson scattering is $A_{S2}(a_g,a_s,v,s)=(a_g+a_s)s^2/v^4$. Cancellation holds when $a_g+a_s=0$ for the Standard-Model scalar coupling, making the amplitude vanish at order $s^2$.

background

The module belongs to the Standard-Model Higgs-EFT chain that begins with the RS cost geometry mapped to the dimensionless scalar coordinate ε=h/v in HiggsEFTBridge. It imports the electroweak mass relations m_W²=g²v²/4 and m_Z²=(g²+g'²)v²/4 from ElectroweakMassBridge, together with the fundamental RS time quantum τ₀=1 from Constants. These supply the vacuum expectation value v that normalizes the high-energy expansion of the longitudinal amplitude.

proof idea

This is a definition module. It introduces amplitudeS2 as the explicit sum (a_gauge + a_scalar) s²/v⁴, defines the gauge-only and scalar-only pieces, and states the CancellationCondition. The three main lemmas follow by direct substitution: amplitude_vanishes_under_cancellation, amplitude_bounded_of_cancellation, and the two preservation statements under the SM and RS hypotheses.

why it matters in Recognition Science

It supplies the high-energy unitarity check required by the five-module Higgs-EFT low-energy-limit bundle in HiggsEFTLowEnergyLimit and is re-exported by the root IndisputableMonolith module. The construction closes the link from RS cost geometry through the effective scalar to the cancellation that restores longitudinal unitarity, exactly as needed for the T5–T8 forcing chain to remain consistent with observed electroweak scattering.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (15)