module module

`IndisputableMonolith.StandardModel.LongitudinalVectorScattering`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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