c4_falsifier
plain-language theorem explainer
The declaration records that the quantum-molecular-depth combination receives the quantum-circuit-depth empirical test class. Cross-domain researchers in Recognition Science cite this registry entry to keep the c4 theorem tied to an observable prediction. The proof reduces to a single reflexivity step that matches the explicit case in the assignment function.
Claim. The empirical test class assigned to the quantum-molecular-depth combination equals the quantum-circuit-depth class.
background
The Option A Falsifier Registry supplies a finite mapping from each of the nine C1-C9 cross-domain theorems to a concrete empirical test class. Its purpose is to attach falsifiers directly to the Lean theorem bundle so that theoretical claims cannot drift into unfalsifiable numerology. The upstream definition falsifierClass implements the mapping by cases, sending the quantum-molecular-depth entry to the quantum-circuit-depth test class.
proof idea
The proof is a one-line reflexivity wrapper that directly matches the corresponding case inside the definition of falsifierClass.
why it matters
This entry feeds the falsifierRegistryCert, which aggregates counts of combinations, test classes, and empirical statuses to certify registry completeness. It implements the module's requirement that cross-domain theorems remain empirically testable, consistent with the Recognition Science emphasis on attaching falsifiers to prevent numerology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.