`TestClass`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAFalsifierRegistry
domain: Foundation
line: 35 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 35.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  32  decide
  33
  34/-- Coarse empirical test class attached to a combination. -/
  35inductive TestClass where
  36  | eegDecoder
  37  | seismicAtmosphericRatio
  38  | tcgaClinicalResponse
  39  | quantumCircuitDepth
  40  | attentionBlinkPlateaus
  41  | adniDementiaProgression
  42  | crossFieldEquilibriumResponse
  43  | workingMemorySpanReduction
  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

papers checked against this theorem

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