falsifierClass
plain-language theorem explainer
This definition maps each of the nine implemented Option A combinations to its designated empirical test class. Cross-domain researchers in Recognition Science cite it to keep theoretical claims tethered to specific observables such as EEG decoding or TCGA response data. The mapping is realized by exhaustive case analysis on the inductive constructors of the combination type.
Claim. Let $C$ be the inductive type of implemented Option A combinations and $T$ the inductive type of coarse empirical test classes. The function $f: C → T$ satisfies $f($cognitive tensor combination$) =$ EEG decoder, $f($planet strata combination$) =$ seismic-atmospheric ratio, $f($oncology tensor combination$) =$ TCGA clinical response, and likewise for the remaining six combinations.
background
The Option A Falsifier Registry module supplies a finite pairing between cross-domain theorems and their empirical test classes. CombinationID enumerates the nine implemented combinations (C1–C9), while TestClass enumerates the attached observables such as EEG decoder, seismic-atmospheric ratio, and TCGA clinical response. The module documentation states that the registry keeps falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology.
proof idea
The definition is realized by direct pattern matching on the nine constructors of CombinationID, returning the matching constructor of TestClass in each branch. No lemmas or tactics are invoked; the construction is purely structural.
why it matters
The definition is invoked by the eight reflexivity theorems c1_falsifier through c8_falsifier that record the concrete assignments. It operationalizes the module goal of anchoring each Option A claim to an empirical test class, thereby supporting the cross-domain verification step that follows the forcing chain and phi-ladder constructions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.