datasetClass_count
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the empirical success or failure of any listed dataset.
- Does not define the measurement protocols or observables within each dataset class.
- Does not connect to the specific J-cost or phi-ladder computations in the Recognition Science core.
- Does not prove uniqueness or completeness of the nine classes beyond the inductive definition.
Lean usage
def registryCert : FalsifierRegistryCert := { nine_combinations := combinationID_count, nine_test_classes := testClass_count, three_statuses := empiricalStatus_count, nine_dataset_classes := datasetClass_count, nine_observables := predictedObservable_count }formal statement (Lean)
73theorem datasetClass_count : Fintype.card DatasetClass = 9 := by
proof body
Decided by rfl or decide.
74 decide
75
76/-- Observable predicted by the Lean structural theorem plus RS hypothesis. -/