c9_falsifier
plain-language theorem explainer
The declaration states that the falsifier class for the C9 regulatory ceiling combination equals the encoded TCGA regulatory module. Researchers anchoring cross-domain theorems to empirical tests cite this to maintain falsifiability in the Option A registry. The proof reduces immediately to reflexivity on the case definition of falsifierClass.
Claim. The empirical test class assigned to the regulatory ceiling combination equals the encoded TCGA regulatory module.
background
Option A Falsifier Registry pairs each of the C1-C9 cross-domain theorems with a specific empirical test class. The module documentation states that this registry keeps falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology, with zero sorrys and zero axioms in the file.
proof idea
The proof is a one-line wrapper applying reflexivity to the definition of falsifierClass at the regulatory ceiling case.
why it matters
This theorem populates the falsifierRegistryCert by supplying one of the nine required mappings. It anchors the C9 regulatory ceiling claim to its TCGA test class, enforcing the module's rule that all cross-domain results stay tied to concrete datasets rather than floating as numerology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.