tree_level_branching_ratio_match
plain-language theorem explainer
Branching ratios computed from amplitudes and phase spaces are identical when the input amplitudes, phase spaces, and channel lists agree between RS and SM. Collider physicists verifying tree-level Higgs decay consistency would cite this identity to confirm structural matching. The argument is a direct substitution of the three equality hypotheses into the branching-ratio definition.
Claim. Let $a_1, a_2, p_1, p_2$ be real amplitudes and phase-space factors, and let $C_{RS}, C_{SM}$ be lists of channel pairs. If $a_1 = a_2$, $p_1 = p_2$, and $C_{RS} = C_{SM}$, then the branching ratio formed from $a_1$, $p_1$, $C_{RS}$ equals the branching ratio formed from $a_2$, $p_2$, $C_{SM}$.
background
The module abstracts Higgs collider observables as structural objects: partial widths depend on an amplitude and phase-space factor, total width sums partial widths over a channel list, and branching ratio is the normalized partial width. The local setting encodes what tree-level RS-SM matching requires: agreement of RS-derived couplings with SM values forces identical tree-level observables, while loop channels remain open. Upstream primitives include eight-tick phase definitions and finite summation operators that treat channel lists uniformly.
proof idea
The proof is a one-line wrapper that rewrites the branching-ratio expressions by substituting the three equality hypotheses for amplitude, phase space, and channel lists.
why it matters
The result supplies the branching-ratio component of the master certificate higgsObservableSkeletonCert. It realizes the tree-level matching step in the Standard Model embedding of the Recognition Science framework, where input agreement forces observable agreement. The module documentation flags loop-level channels such as h to gamma gamma as remaining open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.