cancellation_of_SM_hypothesis

formal source

 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
 143  rw [amplitude_vanishes_under_cancellation a_gauge a_scalar v s
 144        (cancellation_of_SM_hypothesis a_gauge a_scalar h)]
 145  simp
 146
 147/-! ## §4. RS-to-SM Bridge -/
 148
 149/-- The RS Higgs EFT bridge satisfies the cancellation hypothesis exactly
 150    when its scalar-exchange residue is the negative of the gauge residue.
 151
 152    This is the structural statement that the RS theory preserves
 153    longitudinal unitarity.  Concretely: once the canonical-normalisation
 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. -/