DatasetClass
plain-language theorem explainer
DatasetClass enumerates nine empirical dataset classes that pair with the C1-C9 cross-domain theorems. Researchers citing the Option A falsifier registry would reference this enumeration to attach concrete test data to each structural claim. The declaration is a plain inductive definition with DecidableEq, Repr and Fintype instances derived automatically.
Claim. Let $D$ be the finite set whose elements are the EEG/MEG decoder corpus, seismic atmospheric catalog, TCGA clinical trials, quantum chemistry benchmarks, attention blink MEG, ADNI longitudinal, cross-domain panel, working memory perturbation, and encode TCGA regulatory.
background
The module keeps a finite registry that pairs each of the nine cross-domain theorems with an empirical test class, a predicted observable, and a failure mode. DatasetClass supplies the carrier type for the test classes. It is referenced by the function that maps each CombinationID to its assigned dataset class and by the certificate that records Fintype.card DatasetClass = 9.
proof idea
Inductive definition that enumerates the nine constructors and derives the three type-class instances. No lemmas or tactics are applied.
why it matters
The definition supplies the dataset classes required by ProtocolFalsifiable and by FalsifierRegistryCert. It ensures each structural theorem remains attached to a concrete empirical test class, preventing the cross-domain work from drifting into unfalsifiable numerology. It closes one link between the Recognition Science forcing chain and observable predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.