amplitudeScalarOnly

formal source

  73  a_gauge * s ^ 2 / v ^ 4
  74
  75/-- Scalar-only amplitude. -/
  76def amplitudeScalarOnly (a_scalar v s : ℝ) : ℝ :=
  77  a_scalar * s ^ 2 / v ^ 4
  78
  79/-- The total amplitude is the sum of gauge and scalar contributions. -/
  80theorem amplitude_decomposition
  81    (a_gauge a_scalar v s : ℝ) (hv : v ≠ 0) :
  82    amplitudeS2 a_gauge a_scalar v s
  83      = amplitudeGaugeOnly a_gauge v s + amplitudeScalarOnly a_scalar v s := by
  84  unfold amplitudeS2 amplitudeGaugeOnly amplitudeScalarOnly
  85  have hv4 : v ^ 4 ≠ 0 := pow_ne_zero 4 hv
  86  field_simp
  87
  88/-! ## §2. The Cancellation Condition -/
  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.