`LongitudinalVectorScatteringCert`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.LongitudinalVectorScattering
domain: StandardModel
line: 170 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.LongitudinalVectorScattering on GitHub at line 170.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 167/-! ## §5. Master Bridge Certificate -/
 168
 169/-- Master certificate for longitudinal vector-boson scattering. -/
 170structure LongitudinalVectorScatteringCert where
 171  /-- THEOREM: amplitude decomposes additively into gauge + scalar pieces. -/
 172  decomposition       : ∀ a_g a_s v s, v ≠ 0 →
 173    amplitudeS2 a_g a_s v s = amplitudeGaugeOnly a_g v s + amplitudeScalarOnly a_s v s
 174  /-- THEOREM: the leading-order amplitude vanishes under the cancellation. -/
 175  cancels_under_cond  : ∀ a_g a_s v s,
 176    CancellationCondition a_g a_s → amplitudeS2 a_g a_s v s = 0
 177  /-- THEOREM: SM hypothesis implies cancellation. -/
 178  sm_implies_cancel   : ∀ a_g a_s,
 179    SMCancellationHypothesis a_g a_s → CancellationCondition a_g a_s
 180  /-- CONDITIONAL_THEOREM: RS preservation of unitarity implies the
 181      cancellation holds (and hence the amplitude is bounded). -/
 182  rs_implies_bounded  : ∀ a_g a_RS v,
 183    RSPreservesLongitudinalUnitarity a_g a_RS →
 184    ∃ M, ∀ s, |amplitudeS2 a_g a_RS v s| ≤ M
 185
 186def longitudinalVectorScatteringCert : LongitudinalVectorScatteringCert where
 187  decomposition       := amplitude_decomposition
 188  cancels_under_cond  := amplitude_vanishes_under_cancellation
 189  sm_implies_cancel   := cancellation_of_SM_hypothesis
 190  rs_implies_bounded  := fun a_g a_RS v h =>
 191    amplitude_bounded_under_SM_hypothesis a_g a_RS v h
 192
 193theorem longitudinalVectorScatteringCert_inhabited :
 194    Nonempty LongitudinalVectorScatteringCert :=
 195  ⟨longitudinalVectorScatteringCert⟩
 196
 197end
 198
 199end LongitudinalVectorScattering
 200end StandardModel

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.