theorem
proved
datasetClass_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
88
89theorem predictedObservable_count : Fintype.card PredictedObservable = 9 := by
90 decide
91
92/-- What empirical pattern would count as a failure of the associated claim. -/
93inductive FailureMode where
94 | singleAxisDecoderSuffices
95 | noSmallPhiPowerRatio
96 | additiveTherapyResponse
97 | depthExceedsFiveBits
98 | nonFortyPlateauSpectrum
99 | nonReverseDementiaOrder
100 | nonUnitSharedCoefficient
101 | nonQSpaceSpanCollapse
102 | moduleExceedsCeiling70
103 deriving DecidableEq, Repr, Fintype