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

acceptable_all_default_zero

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)

 205lemma acceptable_all_default_zero : acceptable_all defaultDataset { zMax := 0, chi2Max := 0 } := by

proof body

Term-mode proof.

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

depends on (7)

Lean names referenced from this declaration's body.