testClass_count
plain-language theorem explainer
The declaration establishes that the Option A Falsifier Registry enumerates exactly nine coarse empirical test classes. Researchers auditing cross-domain Recognition Science theorems cite it to confirm registry completeness before linking theorems to observables. The proof is a one-line wrapper that applies the decide tactic to the inductive definition of TestClass.
Claim. The finite cardinality of the set of coarse empirical test classes attached to combinations equals nine: $|TestClass| = 9$.
background
The module maintains a finite registry that pairs each of the nine C1-C9 cross-domain theorems with an empirical test class. TestClass is the inductive type whose nine constructors label these coarse empirical tests: eegDecoder, seismicAtmosphericRatio, tcgaClinicalResponse, quantumCircuitDepth, attentionBlinkPlateaus, adniDementiaProgression, crossFieldEquilibriumResponse, workingMemorySpanReduction, and encodeTcgaRegulatoryModule. The module documentation states that this attachment prevents the cross-domain work from drifting into unfalsifiable numerology while leaving the empirical claims themselves unproved.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic directly computes Fintype.card by enumerating the nine constructors of the TestClass inductive type, which is supplied by the sibling definition in the same module.
why it matters
The result supplies the nine_test_classes field inside the falsifierRegistryCert definition, which certifies the full registry structure containing nine combinations, nine test classes, three statuses, nine dataset classes, and nine observables. It closes the bookkeeping step that keeps empirical falsifiers bound to the phi-ladder derivations and the eight-tick octave structure, addressing the framework requirement that cross-domain claims remain testable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.