branchingRatio
plain-language theorem explainer
The branching ratio for a Higgs decay channel is the partial width of that channel divided by the total width summed over all channels, returning zero when the total width vanishes. Collider physicists verifying tree-level RS-SM matching would cite this when amplitudes and phase spaces agree between the two theories. The definition is a direct case split on whether the summed partial widths equal zero.
Claim. Let $a$ be the amplitude and $φ$ the phase-space factor for a given channel, and let the list of all channels be pairs $(a_j, φ_j)$. The branching ratio is $φ a^2 / ∑_j φ_j a_j^2$ when the denominator is positive and equals 0 otherwise.
background
This module formalizes the target surface of Higgs collider observables—partial widths, branching ratios, and signal-strength modifiers—as abstract objects parametrized by amplitudes and phase-space factors. The point is not to recompute SM widths but to make precise what RS-SM matching means at tree level: when RS-derived masses and couplings equal their SM counterparts, the tree-level partial widths must coincide numerically. Partial width is defined as phase-space factor times amplitude squared; total width is the sum of partial widths over a finite list of channels.
proof idea
One-line definition by cases that invokes totalWidth on the channel list and, when nonzero, divides the partialWidth of the supplied amplitude and phase space by that total.
why it matters
Supplies the branching-ratio identity used by branchingRatio_nonneg, the master certificate HiggsObservableSkeletonCert, and the tree-level matching theorem tree_level_branching_ratio_match. In the Recognition framework it closes the structural part of tree-level Higgs observable matching (MODULE_DOC), leaving loop-induced channels such as h → γγ tagged LOOP_LEVEL_OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.