totalWidth_nonneg
plain-language theorem explainer
Non-negativity of the total Higgs decay width follows when every channel supplies a non-negative phase-space factor. A physicist checking structural consistency of Recognition Science Higgs observables would cite the result to guarantee physical branching ratios. The proof is a list induction that applies the partial-width non-negativity lemma to the head, invokes the induction hypothesis on the tail, and closes with linear arithmetic.
Claim. Let channels be a list of pairs (amplitude, phase-space factor). If every phase-space factor satisfies $0 ≤ p_2$, then the total width, defined as the sum of partial widths over the list, satisfies $0 ≤ Γ_{tot}(channels)$.
background
The HiggsObservableSkeleton module formalizes abstract structural objects for partial widths, total widths, branching ratios and signal strengths. These objects capture what RS-SM matching means at tree level: when RS-derived mass, Yukawa and gauge couplings equal their SM counterparts, the tree-level partial widths must coincide. Partial width is a function of amplitude and phase space; total width is their sum. The module flags loop-level corrections (h → γγ, h → gg) as open. Upstream results supply J-cost structures from PhiForcingDerived and ledger factorization, though the immediate dependency is the non-negativity lemma for single partial widths.
proof idea
Unfold the totalWidth definition. Proceed by induction on the channel list. The nil case simplifies directly. For a cons cell, establish head membership by simplification, apply partialWidth_nonneg to the head using the supplied hypothesis, invoke the induction hypothesis on the tail after adjusting the membership predicate, and conclude by linarith.
why it matters
The result is invoked by branchingRatio_nonneg and collected inside higgsObservableSkeletonCert, which packages all non-negativity and matching properties required for the RS-SM tree-level claim. It therefore supports the module's stated purpose that RS reproduces SM Higgs phenomenology when couplings agree. The lemma touches the open question of loop-level partial widths left explicit in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.