pith. machine review for the scientific record. sign in
theorem proved term proof

amplitude_bounded_under_SM_hypothesis

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (25)

Lean names referenced from this declaration's body.