`tree_level_total_width_match`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.HiggsObservableSkeleton
domain: StandardModel
line: 166 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.HiggsObservableSkeleton on GitHub at line 166.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

totalWidth IndisputableMonolith.StandardModel.HiggsObservableSkeleton

formal source

 163/-- If every channel's RS amplitude and phase space match the SM
 164    counterparts, then the total widths are equal channel by channel and
 165    therefore equal in sum. -/
 166theorem tree_level_total_width_match
 167    (rsChannels smChannels : List (ℝ × ℝ))
 168    (h : rsChannels = smChannels) :
 169    totalWidth rsChannels = totalWidth smChannels := by
 170  rw [h]
 171
 172/-- Branching ratios match channel-wise when the underlying channel
 173    structures match. -/
 174theorem tree_level_branching_ratio_match
 175    (amp1 phaseSpace1 amp2 phaseSpace2 : ℝ)
 176    (rsChannels smChannels : List (ℝ × ℝ))
 177    (hamp : amp1 = amp2) (hps : phaseSpace1 = phaseSpace2)
 178    (hch : rsChannels = smChannels) :
 179    branchingRatio amp1 phaseSpace1 rsChannels
 180      = branchingRatio amp2 phaseSpace2 smChannels := by
 181  rw [hamp, hps, hch]
 182
 183/-! ## §5. Master Skeleton Certificate -/
 184
 185/-- Master certificate for the Higgs observable skeleton.
 186
 187    Tags:
 188    - `THEOREM`: structural identities for partial widths, total widths,
 189      branching ratios, and signal strengths.
 190    - `TREE_LEVEL_CONDITIONAL`: the matching theorems are conditional on
 191      the underlying amplitude/phase-space agreement between RS and SM.
 192    - `LOOP_LEVEL_OPEN`: loop-induced channels (`h → γγ`, `h → Zγ`,
 193      `h → gg`) are not formalised here. -/
 194structure HiggsObservableSkeletonCert where
 195  /-- THEOREM: partial widths are non-negative on physical phase space. -/
 196  pw_nonneg     : ∀ amp ps, 0 ≤ ps → 0 ≤ partialWidth amp ps

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.