`amplitudeS2`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.LongitudinalVectorScattering
domain: StandardModel
line: 67 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.LongitudinalVectorScattering on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  64
  65    The Higgs cancellation is the statement that for the SM scalar
  66    coupling, `a_gauge + a_scalar = 0`. -/
  67def amplitudeS2 (a_gauge a_scalar v s : ℝ) : ℝ :=
  68  (a_gauge + a_scalar) * s ^ 2 / v ^ 4
  69
  70/-- Gauge-only amplitude (no scalar contribution): the dangerous
  71    `s²/v⁴` growth. -/
  72def amplitudeGaugeOnly (a_gauge v s : ℝ) : ℝ :=
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.