TestClass
The inductive type enumerates nine coarse empirical test classes for attachment to the C1-C9 cross-domain combinations. Cross-domain theorists cite it when mapping each theorem to a concrete falsifiable check inside the Option A registry. The definition is introduced directly as an inductive with nine constructors and derives DecidableEq, Repr, and Fintype.
claimThe type of coarse empirical test classes is the inductive type whose nine constructors are 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 keeps a finite pairing between each of the nine cross-domain theorems and an empirical test class. This attachment prevents the theoretical claims from drifting into unfalsifiable numerology while the Lean bundle remains zero-sorry. TestClass supplies the codomain for the mapping that assigns one test class to each CombinationID.
proof idea
The declaration is a direct inductive definition that lists the nine constructors explicitly and derives the type classes DecidableEq, Repr, and Fintype.
why it matters in Recognition Science
The definition supplies the nine test classes required by falsifierClass, FalsifierRegistryCert, and testClass_count. It anchors the registry so that each C1-C9 theorem stays paired with a concrete empirical check, directly supporting the module goal of keeping cross-domain work falsifiable.
scope and limits
- Does not prove the validity or outcome of any listed empirical test.
- Does not specify experimental protocols or data sources for the test classes.
- Does not link the classes to the J-cost function, phi-ladder, or other Recognition Science derivations.
- Does not assert the existence of corresponding datasets or observables.
formal statement (Lean)
35inductive TestClass where
36 | eegDecoder
37 | seismicAtmosphericRatio
38 | tcgaClinicalResponse
39 | quantumCircuitDepth
40 | attentionBlinkPlateaus
41 | adniDementiaProgression
42 | crossFieldEquilibriumResponse
43 | workingMemorySpanReduction
44 | encodeTcgaRegulatoryModule
45 deriving DecidableEq, Repr, Fintype
46