theorem
proved
empiricalStatus_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
78 | tensorRank125
79 | strataRatioPhiPower
80 | multiplicativeTherapyResponse
81 | fiveBitAddressBound
82 | fortyStableFiveTransient
83 | reverseEriksonOrder
84 | unitResponseCoefficient
85 | qSpaceSpanSequence
86 | regulatoryCeiling70
87 deriving DecidableEq, Repr, Fintype