pith. machine review for the scientific record. sign in
theorem proved term proof

tree_level_branching_ratio_match

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.