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

signalStrength_zero_of_RS_zero

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)

 139theorem signalStrength_zero_of_RS_zero
 140    (y : ℝ) (hy : y ≠ 0) :
 141    signalStrength 0 y = 0 := by

proof body

Term-mode proof.

 142  unfold signalStrength
 143  simp [hy]
 144
 145/-! ## §4. Tree-Level Matching Theorem -/
 146
 147/-- The decisive structural matching theorem: if the RS amplitude and
 148    phase space for a channel equal their SM counterparts, then the RS
 149    partial width equals the SM partial width.
 150
 151    The hypothesis is exactly the content of "RS reproduces the SM tree
 152    amplitude in this channel."  In practice this hypothesis is satisfied
 153    once the canonical-normalisation map of `HiggsEFTBridge` and the
 154    Yukawa map of `HiggsYukawaBridge` are closed for the channel of
 155    interest. -/

depends on (21)

Lean names referenced from this declaration's body.