 218  intro a b h
 219  cases a <;> cases b <;> simp [failureMode] at h ⊢
 220
 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
 248def falsifierRegistryCert : FalsifierRegistryCert where
 249  nine_combinations := combinationID_count
 250  nine_test_classes := testClass_count
 251  three_statuses := empiricalStatus_count

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.