partialWidth
plain-language theorem explainer
The partial width for a Higgs decay channel is defined as the product of the kinematic phase-space factor and the square of the tree-level amplitude. Collider physicists checking tree-level RS-SM agreement would cite this when amplitudes and phase spaces match between the two theories. The definition is a direct algebraic product with no lemmas or reductions applied.
Claim. The partial width into a channel is given by $Γ = Φ · A²$, where $Φ$ is the kinematic phase-space factor and $A$ is the tree-level amplitude.
background
The Higgs Observable Skeleton module supplies abstract structural objects for partial widths, total widths, branching ratios, and signal strengths. Its purpose is to encode what RS-SM matching means at tree level: when RS-derived masses and couplings equal their SM counterparts, the resulting partial widths must agree numerically. Partial width is the primitive object; total width sums the partial widths over a list of channels, and branching ratios are formed by dividing each partial width by the total.
proof idea
One-line definition that multiplies the phase-space factor by the squared amplitude.
why it matters
This definition is the base for every subsequent identity in the module. It is referenced by totalWidth, branchingRatio, partialWidth_match, partialWidth_nonneg, and the HiggsObservableSkeletonCert structure that records non-negativity and matching theorems. The module documentation states that tree-level partial widths must be identical once amplitudes and phase spaces agree, supplying the observable surface against which the Recognition Science forcing chain and phi-ladder mass formulas are tested. Loop-level channels remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.