c8_falsifier
plain-language theorem explainer
The declaration assigns the working memory span reduction test class to the Miller span combination (c8) inside the Option A falsifier registry. Recognition Science researchers cite the mapping when confirming that each cross-domain theorem carries an attached empirical test. The equality follows by direct reflexivity on the case definition of falsifierClass.
Claim. The empirical test class assigned to the Miller span combination $c_8$ equals the working memory span reduction: $falsifierClass(c_8) = workingMemorySpanReduction$.
background
The Option A Falsifier Registry supplies a finite pairing of each C1-C9 cross-domain theorem with a concrete empirical test class. The module keeps these falsifiers attached to the Lean theorems so that the cross-domain claims cannot drift into unfalsifiable numerology. The function falsifierClass implements the pairing; its definition lists explicit cases such as .eegDecoder for c1CognitiveTensor and .seismicAtmosphericRatio for c2PlanetStrata.
proof idea
The proof is a one-line reflexivity that matches the .c8MillerSpan case inside the definition of falsifierClass.
why it matters
The assignment feeds the falsifierRegistryCert definition, which certifies that nine combinations, nine test classes, three statuses, nine dataset classes, and nine observables are all accounted for. It directly supports the module's goal of keeping the C1-C9 theorems empirically tethered within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.