module module high

`IndisputableMonolith.StandardModel.LongitudinalVectorScattering`

The module defines the leading high-energy s²/v⁴ coefficient in longitudinal WW → WW scattering as (a_gauge + a_scalar) s² / v⁴ and isolates the cancellation condition a_gauge + a_scalar = 0 required for SM unitarity. Particle physicists studying high-energy behavior in RS-derived EFTs would cite it as part of the Standard Model chain. The module consists entirely of definitions and hypotheses with no theorems or proofs.

claim$a_{S2}(a_g, a_s, v, s) = (a_g + a_s) s^2 / v^4$, where the Higgs cancellation condition is $a_g + a_s = 0$ for the SM scalar coupling.

background

This module belongs to the six-module Standard-Model Higgs EFT low-energy-limit chain. It imports the Electroweak Mass Bridge, which derives the gauge-boson mass relations m_W² = g² v² / 4 and m_Z² = (g² + g'²) v² / 4 from the recognition-substrate scale v, and the Higgs EFT Bridge, which formalizes the link RS cost geometry → effective scalar coordinate ε = h / v → canonical Higgs EFT.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by the root IndisputableMonolith and by HiggsEFTLowEnergyLimit, completing the longitudinal scattering segment of the RS-to-SM-EFT chain. Its doc-comment states that the Higgs cancellation is the statement that for the SM scalar coupling, a_gauge + a_scalar = 0.

scope and limits

Does not derive explicit values of a_gauge or a_scalar from RS parameters.
Does not prove unitarity preservation or cancellation in a full model.
Does not address higher-order terms beyond the s² coefficient.
Does not include collider phenomenology or numerical checks.

used by (2)

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

IndisputableMonolith module_import
IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.StandardModel.ElectroweakMassBridge module_import
IndisputableMonolith.StandardModel.HiggsEFTBridge module_import

declarations in this module (15)

def amplitudeS2 L67
def amplitudeGaugeOnly L72
def amplitudeScalarOnly L76
theorem amplitude_decomposition L80
def CancellationCondition L92
theorem amplitude_vanishes_under_cancellation L97
theorem amplitude_bounded_of_cancellation L112
def SMCancellationHypothesis L126
theorem cancellation_of_SM_hypothesis L130
theorem amplitude_bounded_under_SM_hypothesis L137
def RSPreservesLongitudinalUnitarity L157
theorem cancellation_of_RS_preservation L161
structure LongitudinalVectorScatteringCert L170
def longitudinalVectorScatteringCert L186
theorem longitudinalVectorScatteringCert_inhabited L193