falsifierClass_injective
plain-language theorem explainer
The mapping from each of the nine cross-domain theorem identifiers to its assigned empirical test class is injective. Registry maintainers cite this to guarantee that distinct combinations receive distinct falsification protocols without overlap. The proof is a one-line wrapper performing exhaustive case analysis on the finite constructors of CombinationID followed by simplification using the definition of the assignment map.
Claim. The function assigning an empirical test class to each cross-domain theorem combination is injective.
background
The Option A Falsifier Registry maintains a finite pairing between each C1-C9 cross-domain theorem and its empirical test class. This attaches falsifiers directly to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology, as stated in the module documentation. The upstream definition falsifierClass supplies the concrete mapping: it sends c1CognitiveTensor to eegDecoder, c2PlanetStrata to seismicAtmosphericRatio, c3OncologyTensor to tcgaClinicalResponse, c4QuantumMolecularDepth to quantumCircuitDepth, and c5AttentionTensor to attentionBlinkPlateaus (with the remaining four combinations following the same pattern).
proof idea
The proof introduces two arbitrary CombinationID values a and b and assumes their images under the assignment map are equal. It then performs case analysis on both a and b. Because CombinationID is finite, the cases exhaust all constructors; simplification using the definition of the assignment map then forces a to equal b.
why it matters
This injectivity supports the downstream falsifierRegistryCert by confirming that the nine combinations map to distinct test classes, thereby certifying the registry counts. It fills the module requirement that each theorem carries a unique empirical anchor. Within the Recognition Science framework it keeps the cross-domain theorems tied to concrete test protocols rather than allowing drift into numerology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.