tree_level_branching_ratio_match
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical values for SM partial widths.
- Does not formalize loop-induced channels such as h to gamma gamma.
- Does not assume concrete functional forms for amplitude or phase space.
- Does not address higher-order corrections or signal-strength modifiers beyond the matching case.
formal statement (Lean)
174theorem tree_level_branching_ratio_match
175 (amp1 phaseSpace1 amp2 phaseSpace2 : ℝ)
176 (rsChannels smChannels : List (ℝ × ℝ))
177 (hamp : amp1 = amp2) (hps : phaseSpace1 = phaseSpace2)
178 (hch : rsChannels = smChannels) :
179 branchingRatio amp1 phaseSpace1 rsChannels
180 = branchingRatio amp2 phaseSpace2 smChannels := by
proof body
Term-mode proof.
181 rw [hamp, hps, hch]
182
183/-! ## §5. Master Skeleton Certificate -/
184
185/-- Master certificate for the Higgs observable skeleton.
186
187 Tags:
188 - `THEOREM`: structural identities for partial widths, total widths,
189 branching ratios, and signal strengths.
190 - `TREE_LEVEL_CONDITIONAL`: the matching theorems are conditional on
191 the underlying amplitude/phase-space agreement between RS and SM.
192 - `LOOP_LEVEL_OPEN`: loop-induced channels (`h → γγ`, `h → Zγ`,
193 `h → gg`) are not formalised here. -/