pith. machine review for the scientific record. sign in
structure definition def or abbrev

LongitudinalVectorScatteringCert

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

formal statement (Lean)

 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

used by (3)

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

depends on (20)

Lean names referenced from this declaration's body.