signalStrength
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.