DatasetClass
An inductive enumeration of nine empirical test classes supports the falsifier registry for C1-C9 cross-domain theorems. Protocol designers cite this list when specifying the data sources required to test each combination. The definition proceeds by listing the classes explicitly and deriving decidable equality, representation, and finite-type instances.
claimThe type of dataset classes is the inductive type generated by the nine constructors: 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 establishes a finite registry that pairs each of the nine cross-domain theorems with a concrete empirical test class. This inductive type supplies the labels for those test classes, ensuring that every combination carries an attached dataset specification. The local setting requires that the registry remain falsifiable, with zero axioms or sorrys in the Lean development. This does not prove the empirical claims; it keeps the falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology.
proof idea
This is a direct inductive definition of the nine classes, with instances for decidable equality, pretty-printing representation, and finite cardinality derived automatically by the Lean compiler.
why it matters in Recognition Science
The enumeration feeds the ProtocolFalsifiable definition, which asserts that each combination has a dataset class, observable, and failure mode. It realizes the module's goal of attaching empirical falsifiers to the theorem bundle so that cross-domain claims cannot become unfalsifiable. The FalsifierRegistryCert later verifies that exactly nine dataset classes are present, matching the nine combinations.
scope and limits
- Does not encode the actual empirical data or analysis methods.
- Does not establish any mapping from theorems to observables.
- Does not prove the existence of the predicted observables.
- Does not address statistical power or experimental feasibility.
- Does not extend beyond the nine listed classes.
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