falsifierRegistryCert
plain-language theorem explainer
The declaration constructs a single certificate structure that registers empirical falsifiers for each of the nine cross-domain theorems C1-C9. A Recognition Science researcher would cite it to confirm that theoretical claims remain tethered to concrete observables such as EEG decoding or TCGA clinical response. The definition proceeds by direct field assignment of cardinality constants and reflexivity lemmas for each mapping.
Claim. Let $F$ be the structure requiring $|CombinationID|=9$, $|TestClass|=9$, $|EmpiricalStatus|=3$, $|DatasetClass|=9$, $|PredictedObservable|=9$, $|FailureMode|=9$, together with the assignments falsifierClass(c1CognitiveTensor) = eegDecoder, falsifierClass(c2PlanetStrata) = seismicAtmosphericRatio, falsifierClass(c3OncologyTensor) = tcgaClinicalResponse, and the remaining six mappings, plus the four injectivity conditions on classes, datasets, observables, and failure modes. The term falsifierRegistryCert denotes the instance of $F$ satisfying all these equalities.
background
The Option A Falsifier Registry maintains a finite collection of empirical test classes attached to the C1-C9 theorems. The module documentation states that this registry keeps the falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology. Each individual mapping is supplied by an upstream reflexivity theorem, for example c1_falsifier asserts falsifierClass .c1CognitiveTensor = .eegDecoder and c3_observable asserts predictedObservable .c3OncologyTensor = .multiplicativeTherapyResponse.
proof idea
The definition constructs the structure instance by assigning the cardinality constants combinationID_count, testClass_count, empiricalStatus_count, datasetClass_count, predictedObservable_count, and failureMode_count to the respective fields. It then supplies the reflexivity theorems c1_falsifier through c9_falsifier for the test mappings, c3_observable for the predicted observable, c5_failure for the failure mode, c8_dataset for the dataset class, and the four injectivity lemmas falsifierClass_injective, datasetClass_injective, predictedObservable_injective, and failureMode_injective.
why it matters
This definition supplies the central registry that anchors the cross-domain theorems to empirical observables, preventing drift into unfalsifiable territory as stated in the module documentation. It completes the Option A falsifier attachment for the foundation layer, ensuring each C1-C9 claim carries its test class and observable. No downstream uses are recorded, indicating it serves as a standalone certification point within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.