signalStrength_zero_of_RS_zero

formal source

 136  simp [hx]
 137
 138/-- Signal strength of zero RS rate is zero. -/
 139theorem signalStrength_zero_of_RS_zero
 140    (y : ℝ) (hy : y ≠ 0) :
 141    signalStrength 0 y = 0 := by
 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. -/
 156theorem tree_level_partial_width_match
 157    (amp_RS amp_SM phaseSpace_RS phaseSpace_SM : ℝ)
 158    (hamp : amp_RS = amp_SM)
 159    (hps : phaseSpace_RS = phaseSpace_SM) :
 160    partialWidth amp_RS phaseSpace_RS = partialWidth amp_SM phaseSpace_SM :=
 161  partialWidth_match amp_RS amp_SM phaseSpace_RS phaseSpace_SM hamp hps
 162
 163/-- If every channel's RS amplitude and phase space match the SM
 164    counterparts, then the total widths are equal channel by channel and
 165    therefore equal in sum. -/
 166theorem tree_level_total_width_match
 167    (rsChannels smChannels : List (ℝ × ℝ))
 168    (h : rsChannels = smChannels) :
 169    totalWidth rsChannels = totalWidth smChannels := by