c1_falsifier
plain-language theorem explainer
The theorem asserts that the falsifier class for the cognitive tensor combination C1 is the EEG decoder. Researchers anchoring cross-domain Recognition Science claims to empirical tests would cite this mapping. The equality follows by direct reflexivity from the case definition of the falsifier class function.
Claim. The empirical test class assigned to the C1 cognitive tensor combination equals the EEG decoder: $falsifierClass(c1CognitiveTensor) = eegDecoder$.
background
The Option A Falsifier Registry is a finite mapping that pairs each of the nine C1-C9 cross-domain theorems with a concrete empirical test class. As stated in the module documentation, this structure keeps the falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology. The upstream definition of the falsifier class function explicitly records the case for the cognitive tensor combination as the EEG decoder.
proof idea
The proof is a one-line reflexivity equality that matches the explicit case in the definition of the falsifier class function for the C1 cognitive tensor combination.
why it matters
This declaration supplies one of the nine mappings required by the falsifier registry certificate. It directly supports the module goal of preventing drift into unfalsifiable numerology. Within the Recognition Science framework it anchors the foundational cross-domain theorems to observable test classes, consistent with the requirement that all claims remain empirically tethered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.