`acceptable_all_default_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.PDG.Fits
domain: PDG
line: 205 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.PDG.Fits on GitHub at line 205.

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

 202  · exact acceptable_mono (L:=D.baryons) hZ hC hB
 203
 204/-- Baseline: default dataset satisfies thresholds (0,0). -/
 205lemma acceptable_all_default_zero : acceptable_all defaultDataset { zMax := 0, chi2Max := 0 } := by
 206  refine And.intro ?hl (And.intro ?hq (And.intro ?hb ?hB))
 207  · simpa [defaultDataset] using acceptable_leptons
 208  · simpa [defaultDataset] using acceptable_quarks
 209  · simpa [defaultDataset] using acceptable_bosons
 210  · simpa [defaultDataset] using acceptable_baryons
 211
 212namespace External
 213
 214/-- Placeholder: load a dataset from a JSON file (to be implemented).
 215    Currently returns the `defaultDataset`. -/
 216def loadDatasetFromJson (_path : System.FilePath) : IO Dataset :=
 217  pure defaultDataset
 218
 219end External
 220
 221end Fits
 222end PDG
 223end IndisputableMonolith
 224
 225

papers checked against this theorem

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