CancellationCondition

formal source

  89
  90/-- The high-energy cancellation condition: gauge and scalar exchange
  91    sum to zero at the leading `s²/v⁴` order. -/
  92def CancellationCondition (a_gauge a_scalar : ℝ) : Prop :=
  93  a_gauge + a_scalar = 0
  94
  95/-- When the cancellation condition holds, the leading `s²` term vanishes
  96    identically. -/
  97theorem amplitude_vanishes_under_cancellation
  98    (a_gauge a_scalar v s : ℝ)
  99    (hC : CancellationCondition a_gauge a_scalar) :
 100    amplitudeS2 a_gauge a_scalar v s = 0 := by
 101  unfold amplitudeS2 CancellationCondition at *
 102  rw [hC]
 103  ring
 104
 105/-- The amplitude is bounded (in fact identically zero at this order) as
 106    `s → ∞` whenever the cancellation condition holds.
 107
 108    The converse direction — that high-energy boundedness implies
 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