totalWidth
plain-language theorem explainer
The total Higgs width is the sum of partial widths over a finite list of amplitude and phase-space channel pairs. Collider physicists checking Recognition Science tree-level matching to the Standard Model would cite this when assembling branching ratios or signal strengths. The definition is a direct one-line summation obtained by mapping each channel through partialWidth and adding the results.
Claim. The total Higgs decay width is defined by $Γ_{total} = ∑_i Γ_{partial}(a_i, ϕ_i)$, where each channel is a pair $(a_i, ϕ_i)$ of amplitude and phase-space factor.
background
The Higgs Observable Skeleton module treats partial widths, total widths, branching ratios and signal strengths as abstract structural objects parametrized by amplitudes and phase-space factors. Its purpose is to expose the precise conditions under which RS-derived Higgs mass, Yukawa couplings and gauge couplings reproduce the corresponding SM tree-level observables; loop-level channels such as h → γγ remain tagged LOOP_LEVEL_OPEN. Partial width for a single channel is supplied by the sibling definition partialWidth; total width is then their sum over the supplied list.
proof idea
One-line wrapper that applies partialWidth to each channel pair and sums the resulting list.
why it matters
This definition supplies the total width required by branchingRatio, totalWidth_nonneg and the master certificate HiggsObservableSkeletonCert. It completes the structural identity used in tree_level_total_width_match, which states that RS and SM total widths agree whenever the input channel lists agree. The construction directly supports the module's claim that RS reproduces SM Higgs phenomenology at tree level once couplings match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.