FalsifierRegistryCert
plain-language theorem explainer
The FalsifierRegistryCert structure records the exact cardinalities of nine cross-domain combinations, nine test classes, three empirical statuses, nine dataset classes, nine observables, and nine failure modes, together with explicit mappings from each combination to its test class, predicted observable, and failure mode, plus injectivity of the assignment functions. A physicist or mathematician auditing the empirical grounding of Recognition Science claims would cite this registry to confirm that each C1-C9 theorem carries a concrete falsifer
Claim. A structure certifying that there are exactly nine combinations, nine test classes, three empirical statuses, nine dataset classes, nine predicted observables, and nine failure modes, with assignments such as falsifierClass(cognitiveTensor) = eegDecoder, falsifierClass(planetStrata) = seismicAtmosphericRatio, and similarly for the remaining seven combinations, plus the conditions that the maps from combinations to test classes, dataset classes, observables, and failure modes are injective.
background
The module maintains a finite registry that pairs each implemented cross-domain theorem (C1 through C9) with an empirical test class. CombinationID enumerates the nine combinations c1CognitiveTensor through c9RegulatoryCeiling. TestClass lists the corresponding empirical tests such as eegDecoder and seismicAtmosphericRatio. EmpiricalStatus tracks whether a claim is theoremOnly, theoremPlusHypothesis, or scaffoldPlusHypothesis. DatasetClass, PredictedObservable, and FailureMode supply the expected data source, observable, and failure pattern for each combination.
proof idea
The declaration is a structure definition whose fields are populated by the downstream falsifierRegistryCert. It assembles the cardinality lemmas (combinationID_count, testClass_count, empiricalStatus_count, datasetClass_count, predictedObservable_count, failureMode_count) together with the explicit mapping equations (c1_test through c9_test, c3_predicted_observable, c5_failure_mode, c8_dataset_class) and the four injectivity statements. No tactics are required; the structure simply records these facts as a single certificate.
why it matters
This certificate supplies the concrete falsifiability attachment required by the Option A registry so that the nine cross-domain theorems cannot drift into unfalsifiable numerology. It is consumed by falsifierRegistryCert, which constructs the actual instance. In the Recognition Science framework it closes the loop between the structural theorems (derived from the J-cost and phi-ladder) and empirical testability, ensuring each prediction carries a named dataset class and failure mode. The module documentation states that this keeps the falsifiers attached to the Lean theorem bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.