`CombinationID`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 19.

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

  16namespace OptionAFalsifierRegistry
  17
  18/-- The implemented Option A combinations. C10 was left as commentary. -/
  19inductive CombinationID where
  20  | c1CognitiveTensor
  21  | c2PlanetStrata
  22  | c3OncologyTensor
  23  | c4QuantumMolecularDepth
  24  | c5AttentionTensor
  25  | c6EriksonReverse
  26  | c7UniversalResponse
  27  | c8MillerSpan
  28  | c9RegulatoryCeiling
  29  deriving DecidableEq, Repr, Fintype
  30
  31theorem combinationID_count : Fintype.card CombinationID = 9 := by
  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

papers checked against this theorem

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