RSPreservesLongitudinalUnitarity

formal source

 154    map of `HiggsEFTBridge` fixes `Λ(v)`, the scalar coupling fixed by
 155    the J-cost Taylor expansion produces exactly the same residue as in
 156    the SM, with the opposite sign of the gauge residue. -/
 157def RSPreservesLongitudinalUnitarity (a_gauge a_scalar_RS : ℝ) : Prop :=
 158  a_scalar_RS = -a_gauge
 159
 160/-- If RS preserves longitudinal unitarity, the cancellation holds. -/
 161theorem cancellation_of_RS_preservation
 162    (a_gauge a_scalar_RS : ℝ)
 163    (h : RSPreservesLongitudinalUnitarity a_gauge a_scalar_RS) :
 164    CancellationCondition a_gauge a_scalar_RS :=
 165  cancellation_of_SM_hypothesis a_gauge a_scalar_RS h
 166
 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