`tree_level_partial_width_match`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.HiggsObservableSkeleton
domain: StandardModel
line: 156 · 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 156.

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

formal source

 153    once the canonical-normalisation map of `HiggsEFTBridge` and the
 154    Yukawa map of `HiggsYukawaBridge` are closed for the channel of
 155    interest. -/
 156theorem tree_level_partial_width_match
 157    (amp_RS amp_SM phaseSpace_RS phaseSpace_SM : ℝ)
 158    (hamp : amp_RS = amp_SM)
 159    (hps : phaseSpace_RS = phaseSpace_SM) :
 160    partialWidth amp_RS phaseSpace_RS = partialWidth amp_SM phaseSpace_SM :=
 161  partialWidth_match amp_RS amp_SM phaseSpace_RS phaseSpace_SM hamp hps
 162
 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

papers checked against this theorem

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