datasetClass_count
plain-language theorem explainer
The cardinality theorem asserts that the DatasetClass inductive type, which enumerates nine empirical test datasets for cross-domain recognition theorems, contains precisely nine elements. Falsifiability auditors in the Recognition Science framework cite this result to confirm the registry structure. Its proof reduces to a single decide tactic that evaluates the finite type cardinality from the inductive constructors.
Claim. Let $D$ be the inductive type whose nine constructors are the empirical datasets eegMegDecoderCorpus, seismicAtmosphericCatalog, tcgaClinicalTrials, quantumChemistryBenchmarks, attentionBlinkMeg, adniLongitudinal, crossDomainPanel, workingMemoryPerturbation, and encodeTcgaRegulatory. Then the cardinality satisfies $|D| = 9$.
background
The Option A Falsifier Registry maintains a finite collection of test classes paired with cross-domain theorems to ensure empirical falsifiability. DatasetClass is defined as an inductive type listing nine specific datasets expected to carry the empirical tests for these theorems. This registry operates alongside Observable structures from RecognitionForcing, RSNative.Core, and Quantum.Observables, which define how recognition events and measurements extract values from states. The module documentation states that the registry keeps the falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic computes the Fintype.card directly from the nine constructors of the DatasetClass inductive type, confirming the cardinality without further lemmas.
why it matters
This result populates the nine_dataset_classes field in falsifierRegistryCert, which bundles the counts for combinations, test classes, statuses, dataset classes, and observables. It supports the framework's requirement that each C1-C9 theorem has an attached empirical test class, preventing drift from the forcing chain into unfalsifiable claims. The module explicitly notes zero sorry or axiom in the Lean status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.