datasetClass
plain-language theorem explainer
The datasetClass definition maps each of the nine implemented Option A combinations to its designated empirical dataset class. Protocol designers in the cross-domain falsification layer cite it to attach concrete test data to each C1-C9 claim. It is realized as a total function by exhaustive pattern matching on the constructors of CombinationID.
Claim. Define the map $datasetClass : CombinationID → DatasetClass$ by the assignments $datasetClass(c1CognitiveTensor) = eegMegDecoderCorpus$, $datasetClass(c2PlanetStrata) = seismicAtmosphericCatalog$, $datasetClass(c3OncologyTensor) = tcgaClinicalTrials$, and likewise for the remaining six combinations through $c9RegulatoryCeiling$.
background
CombinationID is the inductive type that enumerates the nine implemented Option A combinations (c1CognitiveTensor through c9RegulatoryCeiling). DatasetClass is the inductive type that enumerates the empirical test classes (eegMegDecoderCorpus, seismicAtmosphericCatalog, tcgaClinicalTrials, and so on). The Option A Falsifier Registry module maintains a finite pairing of each cross-domain theorem with its empirical test class so that the claims remain attached to concrete falsifiers and cannot drift into unfalsifiable numerology.
proof idea
Implemented directly as a total function by exhaustive pattern matching on each of the nine constructors of CombinationID.
why it matters
This definition supplies the dataset field required by ProtocolFalsifiable, ProtocolMatches, and protocolSpec in the empirical protocol layer. It ensures every combination carries an attached falsifier dataset, fulfilling the registry's role of keeping the C1-C9 theorems empirically grounded. The construction supports the Recognition Science requirement that theoretical derivations remain testable rather than purely formal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.