branchingRatio_nonneg
plain-language theorem explainer
Branching ratios for Higgs decays remain non-negative whenever the input phase-space factors are non-negative. Phenomenologists working on RS-SM matching would invoke this result to confirm that the derived observables stay physical. The proof proceeds by unfolding the branching-ratio definition, splitting on whether the total width vanishes, and applying the non-negativity of partial and total widths together with the division lemma.
Claim. Let $a, s, s_i, a_i, s_i' in mathbb{R}$ and let $mathcal{C}$ be a finite list of pairs $(a_i, s_i')$. If $0 leq s$ and $0 leq s_i'$ for every pair in $mathcal{C}$, then $0 leq mathrm{BR}(a, s, mathcal{C})$, where $mathrm{BR}$ is the ratio of the channel partial width $s cdot a^2$ to the sum of all partial widths (or zero when that sum vanishes).
background
In the Higgs Observable Skeleton module, partial widths are defined abstractly as partialWidth(amp, phaseSpace) = phaseSpace * amp^2, with the phase-space factor required to be non-negative for physical channels. The total width is the sum of partial widths over a list of channels. The branching ratio is then the partial width of a given channel divided by the total width, defaulting to zero if the total width is zero. This setup allows formal verification of structural properties without committing to explicit Standard Model computations. Upstream, the non-negativity of partial widths follows from the square being non-negative and multiplication preserving non-negativity, while totalWidth_nonneg aggregates the same property over the channel list.
proof idea
The proof unfolds the definition of branchingRatio. It performs a case distinction on whether the total width is zero. In the zero case the result is immediate by the definition. Otherwise it invokes partialWidth_nonneg to obtain non-negativity of the numerator and totalWidth_nonneg for the denominator, then applies the lemma that a non-negative number divided by a positive number is non-negative.
why it matters
This theorem supplies the non-negativity property for branching ratios that is recorded in the HiggsObservableSkeletonCert. The certificate aggregates non-negativity and matching statements to certify that the RS-derived Higgs observables reproduce the required structural features of the Standard Model at tree level. It closes one of the structural identities listed in the module status as THEOREM.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.