totalWidth_nonneg
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical values for any width.
- Does not address loop-level contributions to partial widths.
- Does not constrain the amplitude values themselves.
- Does not establish positivity of individual partial widths without the phase-space hypothesis.
Lean usage
have h : 0 ≤ totalWidth channels := totalWidth_nonneg channels hpsformal statement (Lean)
83theorem totalWidth_nonneg (channels : List (ℝ × ℝ))
84 (hps : ∀ p ∈ channels, 0 ≤ p.snd) :
85 0 ≤ totalWidth channels := by
proof body
Tactic-mode proof.
86 unfold totalWidth
87 induction channels with
88 | nil => simp
89 | cons head tail ih =>
90 simp only [List.map_cons, List.sum_cons]
91 have hhead_mem : head ∈ head :: tail := by simp
92 have hhead : 0 ≤ partialWidth head.fst head.snd :=
93 partialWidth_nonneg head.fst head.snd (hps head hhead_mem)
94 have htail : 0 ≤ (tail.map (fun p => partialWidth p.fst p.snd)).sum := by
95 apply ih
96 intro p hp
97 exact hps p (by simp [hp])
98 linarith
99
100/-- The branching ratio of a single channel is its partial width over the
101 total width. Defined to be zero if the total width is zero (a
102 degenerate, unphysical case). -/