`higgsObservableSkeletonCert`

definition

show as: view math explainer →

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

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

used by

formal source

 212                   a1 = a2 → p1 = p2 → c_rs = c_sm →
 213                   branchingRatio a1 p1 c_rs = branchingRatio a2 p2 c_sm
 214
 215def higgsObservableSkeletonCert : HiggsObservableSkeletonCert where
 216  pw_nonneg     := partialWidth_nonneg
 217  tw_nonneg     := totalWidth_nonneg
 218  br_nonneg     := branchingRatio_nonneg
 219  signal_unity  := signalStrength_one_of_match
 220  tree_pw_match := partialWidth_match
 221  tree_br_match := tree_level_branching_ratio_match
 222
 223theorem higgsObservableSkeletonCert_inhabited : Nonempty HiggsObservableSkeletonCert :=
 224  ⟨higgsObservableSkeletonCert⟩
 225
 226end
 227
 228end HiggsObservableSkeleton
 229end StandardModel
 230end IndisputableMonolith

papers checked against this theorem

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