pith. sign in
module module high

IndisputableMonolith.StandardModel.LongitudinalVectorScattering

show as:
view Lean formalization →

This module isolates the leading high-energy s²/v⁴ coefficient in longitudinal WW scattering and encodes the Higgs cancellation condition that sets the gauge plus scalar contributions to zero. Collider physicists checking perturbative unitarity in the electroweak sector would cite these objects when mapping RS cost geometry onto SM phenomenology. The module consists of definitions for amplitudeS2 together with lemmas that establish vanishing and boundedness once the cancellation hypothesis holds.

claimDefine the leading coefficient by $a_{S2}(a_g,a_s,v,s)=(a_g+a_s)s^2/v^4$. The SM Higgs cancellation is the relation $a_g+a_s=0$ for the scalar coupling that appears in the canonical Higgs EFT.

background

The module belongs to the six-module Standard-Model chain that converts RS cost geometry into the low-energy Higgs EFT. Upstream, ElectroweakMassBridge supplies the tree-level masses $m_W^2=g^2v^2/4$ and $m_Z^2=(g^2+g'^2)v^2/4$ from the recognition scale $v$ and positive gauge couplings. HiggsEFTBridge introduces the dimensionless coordinate $ε=h/v$ that identifies the RS effective scalar with the canonically normalized collider field.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the amplitude objects required by the Higgs EFT Low-Energy Limit master certificate. It thereby completes the segment of the chain that runs from RS cost geometry through the electroweak mass bridge to the cancellation that preserves longitudinal unitarity. The parent result is the bundled certificate in HiggsEFTLowEnergyLimit that formalizes the full sequence requested for the companion paper.

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)