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

amplitude_bounded_of_cancellation

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)

 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

proof body

Term-mode proof.

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

depends on (12)

Lean names referenced from this declaration's body.