 124
 125    By construction, `μ = 1` when both the cross-section and the branching
 126    ratio match the SM. -/
 127def signalStrength (sigma_BR_RS sigma_BR_SM : ℝ) : ℝ :=
 128  if sigma_BR_SM = 0 then 0 else sigma_BR_RS / sigma_BR_SM
 129
 130/-- The signal-strength modifier equals 1 when both numerator and
 131    denominator agree. -/
 132theorem signalStrength_one_of_match
 133    (x : ℝ) (hx : x ≠ 0) :
 134    signalStrength x x = 1 := by
 135  unfold signalStrength
 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 : ℝ)

papers checked against this theorem

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