FalsifierRegistryCert
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
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove any of the empirical claims attached to the combinations.
- Does not include the C10 combination left as commentary.
- Does not specify the actual data or results from the listed datasets.
- Does not derive the mappings from the J-cost equation or the forcing chain.
- Does not address the status of the underlying theorems beyond recording their empirical attachments.
formal statement (Lean)
221structure FalsifierRegistryCert where
222 nine_combinations : Fintype.card CombinationID = 9
223 nine_test_classes : Fintype.card TestClass = 9
224 three_statuses : Fintype.card EmpiricalStatus = 3
225 nine_dataset_classes : Fintype.card DatasetClass = 9
226 nine_observables : Fintype.card PredictedObservable = 9
227 nine_failure_modes : Fintype.card FailureMode = 9
228 c1_test : falsifierClass .c1CognitiveTensor = .eegDecoder
229 c2_test : falsifierClass .c2PlanetStrata = .seismicAtmosphericRatio
230 c3_test : falsifierClass .c3OncologyTensor = .tcgaClinicalResponse
231 c4_test : falsifierClass .c4QuantumMolecularDepth = .quantumCircuitDepth
232 c5_test : falsifierClass .c5AttentionTensor = .attentionBlinkPlateaus
233 c6_test : falsifierClass .c6EriksonReverse = .adniDementiaProgression
234 c7_test : falsifierClass .c7UniversalResponse = .crossFieldEquilibriumResponse
235 c8_test : falsifierClass .c8MillerSpan = .workingMemorySpanReduction
236 c9_test : falsifierClass .c9RegulatoryCeiling = .encodeTcgaRegulatoryModule
237 c3_predicted_observable :
238 predictedObservable .c3OncologyTensor = .multiplicativeTherapyResponse
239 c5_failure_mode :
240 failureMode .c5AttentionTensor = .nonFortyPlateauSpectrum
241 c8_dataset_class :
242 datasetClass .c8MillerSpan = .workingMemoryPerturbation
243 test_class_injective : Function.Injective falsifierClass
244 dataset_class_injective : Function.Injective datasetClass
245 observable_injective : Function.Injective predictedObservable
246 failure_mode_injective : Function.Injective failureMode
247