amplitude_bounded_of_cancellation

formal source

 109    cancellation — is true but requires explicit unbounded-coefficient
 110    machinery and is left out of the present formalization; it is not
 111    needed for the RS-to-SM bridge below. -/
 112theorem amplitude_bounded_of_cancellation
 113    (a_gauge a_scalar v : ℝ)
 114    (hC : CancellationCondition a_gauge a_scalar) :
 115    ∃ M : ℝ, ∀ s : ℝ, |amplitudeS2 a_gauge a_scalar v s| ≤ M := by
 116  refine ⟨0, ?_⟩
 117  intro s
 118  rw [amplitude_vanishes_under_cancellation a_gauge a_scalar v s hC]
 119  simp
 120
 121/-! ## §3. SM-Normalisation Hypothesis -/
 122
 123/-- Standard-Model normalisation hypothesis for longitudinal-VV scattering:
 124    in the canonical SM, the scalar-exchange residue exactly cancels the
 125    gauge-exchange residue. -/
 126def SMCancellationHypothesis (a_gauge a_scalar : ℝ) : Prop :=
 127  a_scalar = -a_gauge
 128
 129/-- The SM cancellation hypothesis implies the cancellation condition. -/
 130theorem cancellation_of_SM_hypothesis
 131    (a_gauge a_scalar : ℝ) (h : SMCancellationHypothesis a_gauge a_scalar) :
 132    CancellationCondition a_gauge a_scalar := by
 133  unfold CancellationCondition SMCancellationHypothesis at *
 134  rw [h]; ring
 135
 136/-- Under the SM cancellation hypothesis, the amplitude is bounded. -/
 137theorem amplitude_bounded_under_SM_hypothesis
 138    (a_gauge a_scalar v : ℝ)
 139    (h : SMCancellationHypothesis a_gauge a_scalar) :
 140    ∃ M : ℝ, ∀ s : ℝ, |amplitudeS2 a_gauge a_scalar v s| ≤ M := by
 141  refine ⟨0, ?_⟩
 142  intro s