DatasetClass
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.