pith. machine review for the scientific record. sign in
def definition def or abbrev high

falsifierRegistryCert

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 248def falsifierRegistryCert : FalsifierRegistryCert where
 249  nine_combinations := combinationID_count

proof body

Definition body.

 250  nine_test_classes := testClass_count
 251  three_statuses := empiricalStatus_count
 252  nine_dataset_classes := datasetClass_count
 253  nine_observables := predictedObservable_count
 254  nine_failure_modes := failureMode_count
 255  c1_test := c1_falsifier
 256  c2_test := c2_falsifier
 257  c3_test := c3_falsifier
 258  c4_test := c4_falsifier
 259  c5_test := c5_falsifier
 260  c6_test := c6_falsifier
 261  c7_test := c7_falsifier
 262  c8_test := c8_falsifier
 263  c9_test := c9_falsifier
 264  c3_predicted_observable := c3_observable
 265  c5_failure_mode := c5_failure
 266  c8_dataset_class := c8_dataset
 267  test_class_injective := falsifierClass_injective
 268  dataset_class_injective := datasetClass_injective
 269  observable_injective := predictedObservable_injective
 270  failure_mode_injective := failureMode_injective
 271
 272end OptionAFalsifierRegistry
 273end Foundation
 274end IndisputableMonolith

depends on (23)

Lean names referenced from this declaration's body.