partialWidth_match
plain-language theorem explainer
The theorem asserts that partial widths coincide exactly when the input amplitudes and phase-space factors are identical. Collider modelers verifying tree-level equivalence between Recognition Science and Standard Model Higgs phenomenology cite it as the base identity for observable matching. The proof is a direct one-line rewrite that substitutes the two equality hypotheses into the partialWidth definition.
Claim. If the amplitudes satisfy $a_1 = a_2$ and the phase-space factors satisfy $p_1 = p_2$, then the partial width satisfies $w(a_1, p_1) = w(a_2, p_2)$.
background
The Higgs Observable Skeleton module abstracts collider observables (partial widths, branching ratios, signal strengths) as structural objects parametrized by amplitudes and phase-space factors. Its purpose is to make precise the statement that Recognition Science reproduces Standard Model Higgs phenomenology at tree level once masses and couplings match via the EFT and Yukawa bridges. Partial width is the basic building block; non-negativity and matching properties are proved in sibling declarations within the same module.
proof idea
The proof is a one-line wrapper that applies the rewrite tactic to the hypotheses hamp and hps, substituting them directly into the partialWidth expression.
why it matters
It is invoked inside higgsObservableSkeletonCert to assemble the full certification bundle and inside tree_level_partial_width_match to establish the decisive structural matching. This supplies the tree-level matching step required by the module documentation for RS to reproduce SM observables when amplitudes and phase spaces agree. Loop-level channels remain tagged open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.