c7_falsifier
plain-language theorem explainer
This declaration records that the c7 universal response combination maps to the cross-field equilibrium response test class inside the Option A registry. Researchers auditing cross-domain theorems cite it to confirm every C1-C9 entry carries a concrete empirical anchor. The equality holds by direct reflexivity on the definition of falsifierClass.
Claim. The falsifier class attached to the C7 universal response combination equals the cross-field equilibrium response: $falsifierClass(C7) = crossFieldEquilibriumResponse$.
background
The Option A Falsifier Registry supplies a finite pairing of each C1-C9 cross-domain theorem with an empirical test class. Its module doc states that the registry keeps falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology. The upstream definition falsifierClass : CombinationID → TestClass supplies the concrete mapping for every combination, with its doc-comment reading 'The empirical test class for each Option A combination.'
proof idea
The proof is a one-line reflexivity that matches the definition of falsifierClass at the c7 case.
why it matters
The entry feeds the falsifierRegistryCert, which certifies that nine combinations, nine test classes, and the remaining counts are all populated. It completes the C7 slot in the registry of empirical anchors for the cross-domain theorems. The module thereby enforces that Recognition Science claims remain testable rather than numerological.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.