`longitudinalVectorScatteringCert`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.LongitudinalVectorScattering
domain: StandardModel
line: 186 · 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 186.

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

 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
 201end IndisputableMonolith

papers checked against this theorem

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