theorem
proved
testClass_count
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
44 | encodeTcgaRegulatoryModule
45 deriving DecidableEq, Repr, Fintype
46
47theorem testClass_count : Fintype.card TestClass = 9 := by
48 decide
49
50/-- Status of the Lean theorem relative to the empirical claim. -/
51inductive EmpiricalStatus where
52 | theoremOnly
53 | theoremPlusHypothesis
54 | scaffoldPlusHypothesis
55 deriving DecidableEq, Repr, Fintype
56
57theorem empiricalStatus_count : Fintype.card EmpiricalStatus = 3 := by
58 decide
59
60/-- Dataset class expected to carry the empirical test. -/
61inductive DatasetClass where
62 | eegMegDecoderCorpus
63 | seismicAtmosphericCatalog
64 | tcgaClinicalTrials
65 | quantumChemistryBenchmarks
66 | attentionBlinkMeg
67 | adniLongitudinal
68 | crossDomainPanel
69 | workingMemoryPerturbation
70 | encodeTcgaRegulatory
71 deriving DecidableEq, Repr, Fintype
72
73theorem datasetClass_count : Fintype.card DatasetClass = 9 := by
74 decide
75
76/-- Observable predicted by the Lean structural theorem plus RS hypothesis. -/
77inductive PredictedObservable where