signalStrength
The signal strength modifier for a Higgs decay channel is the ratio of the RS-predicted rate (cross-section times branching ratio) to the Standard Model rate, returning zero when the SM denominator vanishes. Collider physicists testing RS extensions against LHC data would cite this to quantify deviations from SM predictions. The definition is a direct conditional division that enforces equality to one under exact rate matching.
claimThe signal strength modifier for a channel is defined by $μ = (σ · BR)_{RS} / (σ · BR)_{SM}$ when the SM value is nonzero and $μ = 0$ otherwise.
background
This module formalises abstract structural objects for Higgs collider observables: partial widths, total widths, branching ratios, and signal-strength modifiers. These objects are parametrised by amplitudes and phase-space factors to expose what it means for an RS theory to match SM Higgs phenomenology at tree level. If the RS Higgs mass, Yukawa couplings, and gauge couplings equal the SM values, then the tree-level partial widths computed from the same amplitude formula must be identical; loop-level channels remain tagged open.
proof idea
The declaration is a definition that directly encodes the ratio with an explicit zero-check guard on the denominator. It is a one-line wrapper implementing the piecewise function for the signal strength modifier.
why it matters in Recognition Science
This definition supplies the signal strength component inside the HiggsObservableSkeletonCert master certificate that collects structural identities for partial widths, total widths, branching ratios, and signal strengths. It fills the tree-level matching requirement stated in the module status for RS reproducing SM observables when couplings agree. It supports the downstream theorems establishing that the modifier equals one under matching rates and equals zero when the RS rate vanishes.
scope and limits
- Does not derive numerical cross sections or branching ratios from underlying amplitudes.
- Does not incorporate loop-level corrections for channels such as h → γγ.
- Does not address experimental uncertainties or detector effects.
- Does not depend on specific RS mass or coupling ladder formulas.
formal statement (Lean)
127def signalStrength (sigma_BR_RS sigma_BR_SM : ℝ) : ℝ :=
proof body
Definition body.
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. -/