def definition def or abbrev

`datasetClass`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 134def datasetClass : CombinationID → DatasetClass
 135  | .c1CognitiveTensor => .eegMegDecoderCorpus
 136  | .c2PlanetStrata => .seismicAtmosphericCatalog
 137  | .c3OncologyTensor => .tcgaClinicalTrials
 138  | .c4QuantumMolecularDepth => .quantumChemistryBenchmarks
 139  | .c5AttentionTensor => .attentionBlinkMeg
 140  | .c6EriksonReverse => .adniLongitudinal
 141  | .c7UniversalResponse => .crossDomainPanel
 142  | .c8MillerSpan => .workingMemoryPerturbation
 143  | .c9RegulatoryCeiling => .encodeTcgaRegulatory
 144
 145/-- Predicted observable assigned to each implemented combination. -/

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

ProtocolFalsifiable in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
protocolFalsifiable_all in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
ProtocolMatches in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
protocolSpec in IndisputableMonolith.Foundation.OptionAEmpiricalProtocol decl_use
c8_dataset in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
datasetClass_injective in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
FalsifierRegistryCert in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use

depends on (2)

Lean names referenced from this declaration's body.

CombinationID in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use
DatasetClass in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use