partialWidth_nonneg
plain-language theorem explainer
The theorem establishes non-negativity of the Higgs partial width into any channel whenever the phase-space factor is non-negative. Collider physicists checking tree-level RS-SM matching would cite it to guarantee that all constructed observables remain physically admissible. The proof is a direct algebraic reduction that unfolds the definition and applies the elementary facts that squares and products of non-negative reals stay non-negative.
Claim. If the phase-space factor satisfies $0 ≤ ϕ$, then the partial width defined by $ϕ · A²$ is non-negative, where $A$ is the tree-level amplitude into the channel.
background
The Higgs Observable Skeleton module formalises partial widths, branching ratios and signal-strength modifiers as abstract structural objects parametrised by amplitudes and phase-space factors. Its purpose is to make precise what tree-level matching between Recognition Science and the Standard Model requires: when the RS-derived Higgs mass and couplings equal their SM values, the resulting partial widths must coincide numerically. The partial width into a channel is defined by the product of the phase-space factor and the square of the amplitude; both factors must be non-negative for a physical channel. Upstream results supply the eight-tick phase definitions and circle-phase lifts used elsewhere in the module, while the non-negativity statement itself rests on basic properties of the reals.
proof idea
The proof unfolds the definition of partialWidth to obtain the product phaseSpace · amp². It then applies the fact that the square of any real number is non-negative, followed by the fact that the product of two non-negative reals is non-negative, and concludes directly.
why it matters
This result is invoked by branchingRatio_nonneg, totalWidth_nonneg and the higgsObservableSkeletonCert that packages the full set of structural identities. It supplies one of the THEOREM-level guarantees listed in the module documentation that RS reproduces SM Higgs observables at tree level when couplings agree. The module flags loop-level partial widths (h → γγ, h → gg) as still open, so this non-negativity statement closes the tree-level skeleton while leaving the loop corrections untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.