DatasetClass
DatasetClass enumerates the nine empirical test classes attached to the C1-C9 cross-domain theorems inside the Option A falsifier registry. Researchers formalizing empirical protocols cite this type when they need a finite, decidable collection of datasets to pair with each structural theorem. The declaration is a direct inductive enumeration of nine constructors that derives DecidableEq, Repr, and Fintype.
claimLet $D$ be the finite inductive type whose constructors are the EEG/MEG decoder corpus, seismic atmospheric catalog, TCGA clinical trials, quantum chemistry benchmarks, attention blink MEG, ADNI longitudinal study, cross-domain panel, working memory perturbation, and encode TCGA regulatory.
background
The Option A Falsifier Registry module maintains a finite pairing between each of the nine cross-domain theorems and a concrete empirical test class. DatasetClass supplies the type of those test classes so that downstream protocol definitions can reference them without leaving the Lean bundle. The module documentation states that this attachment prevents the cross-domain work from drifting into unfalsifiable numerology. The type is equipped with Fintype so that cardinality statements such as nine dataset classes can be decided by computation.
proof idea
The declaration is an inductive definition that introduces exactly nine constructors, one for each listed dataset class, and immediately derives the instances DecidableEq, Repr, and Fintype.
why it matters in Recognition Science
DatasetClass supplies the dataset component required by ProtocolFalsifiable, which states that a combination is protocol-falsifiable precisely when it possesses a dataset class, a predicted observable, and a failure mode. It is also referenced by the FalsifierRegistryCert structure that certifies the existence of nine dataset classes. The definition therefore realizes the module's stated purpose of keeping falsifiers attached to the theorem bundle for the Recognition Science cross-domain claims. No open scaffolding remains; the enumeration is closed and finite.
scope and limits
- Does not assign any dataset class to a specific combination.
- Does not contain empirical data or test outcomes.
- Does not extend the list beyond the nine enumerated classes.
- Does not prove that any listed class is sufficient to falsify its paired theorem.
formal statement (Lean)
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