tree_level_total_width_match
plain-language theorem explainer
Equal lists of (amplitude, phase-space) channel pairs produce identical total Higgs widths. A physicist checking tree-level RS-SM matching would cite it to confirm summed observables agree once inputs coincide. The proof is a one-line rewrite that substitutes the channel-list equality into the sum definition of total width.
Claim. If two lists of pairs $(A_i,Phi_i)$ for RS and SM channels are identical, then the total Higgs width $Gamma=sum_i partialWidth(A_i,Phi_i)$ computed from the RS list equals the width computed from the SM list.
background
The module formalizes Higgs collider observables as abstract objects parametrized by amplitudes and phase-space factors. Total width is the sum of partial widths over a finite list of such pairs. The upstream totalWidth definition is exactly that sum, and the module states that RS reproduces SM tree-level partial widths once Higgs mass, Yukawa couplings, and gauge couplings agree.
proof idea
One-line wrapper that rewrites the hypothesis rsChannels = smChannels directly into the two totalWidth applications.
why it matters
The theorem supplies the structural identity for total-width matching inside the Higgs observable skeleton. It closes one step of the tree-level equivalence claim in the module documentation, where RS-SM agreement on input couplings forces agreement on summed observables. Loop-level channels such as h to gamma gamma remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.