TestClass
plain-language theorem explainer
TestClass enumerates nine coarse empirical domains that serve as falsifiers for the C1-C9 cross-domain theorems. A researcher auditing the Option A registry would cite this enumeration to confirm each combination carries a distinct empirical anchor. The declaration is a plain inductive type with nine constructors that derives DecidableEq, Repr, and Fintype.
Claim. An inductive type whose nine constructors label the empirical test classes: EEG decoder, seismic-atmospheric ratio, TCGA clinical response, quantum circuit depth, attention blink plateaus, ADNI dementia progression, cross-field equilibrium response, working memory span reduction, and encode TCGA regulatory module.
background
The Option A Falsifier Registry maintains a finite pairing between each of the nine cross-domain theorems (C1-C9) and an empirical test class. This structure ensures that the cross-domain work remains attached to concrete falsifiers rather than drifting into unfalsifiable numerology. The module declares zero sorry or axiom statements.
proof idea
The declaration is an inductive type with nine constructors deriving DecidableEq, Repr, and Fintype instances.
why it matters
This enumeration supplies the codomain for the falsifierClass mapping from CombinationID, supplies the nine_test_classes field of FalsifierRegistryCert, and is counted by the testClass_count theorem. It directly implements the module requirement that each theorem bundle carries an attached empirical test class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.