datasetClass_injective
plain-language theorem explainer
The function assigning each of the nine CombinationIDs to a DatasetClass is injective. Empirical protocol designers cite this to guarantee that distinct cross-domain theorems receive distinct test datasets. The proof proceeds by exhaustive case analysis on the finite enumeration of combinations followed by simplification using the explicit mapping.
Claim. The mapping $datasetClass : CombinationID → DatasetClass$ is injective.
background
The Option A Falsifier Registry maintains a finite pairing between each of the nine C1-C9 cross-domain theorems, represented as CombinationID, and an empirical test class in DatasetClass. This registry ensures that falsifiers remain attached to the Lean theorem bundle, preventing drift into unfalsifiable claims. The upstream definition datasetClass explicitly maps each combination, such as .c1CognitiveTensor to .eegMegDecoderCorpus.
proof idea
The proof introduces two arbitrary combinations a and b, assumes their images under datasetClass are equal, then performs exhaustive case analysis on both and simplifies using the definition of datasetClass.
why it matters
This injectivity supports the parent result protocolSpec_injective, which establishes that distinct combinations yield distinct protocol records. It also contributes to the falsifierRegistryCert by confirming nine distinct dataset classes. Within the Recognition framework, it anchors the empirical test classes to the cross-domain theorems, fulfilling the requirement that the Option A registry keeps all claims falsifiable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.