datasetClass_injective
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not verify the actual existence or quality of the listed datasets.
- Does not prove that the assigned test classes suffice to falsify the theorems.
- Does not address statistical power of the empirical protocols.
- Does not extend beyond the nine enumerated combinations.
Lean usage
intro a b h; apply datasetClass_injective; exact congrArg ProtocolSpec.dataset hformal statement (Lean)
209theorem datasetClass_injective : Function.Injective datasetClass := by
proof body
Term-mode proof.
210 intro a b h
211 cases a <;> cases b <;> simp [datasetClass] at h ⊢
212