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

amplitude_decomposition

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)

  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

proof body

Term-mode proof.

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

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.