 190theorem c8_falsifier :
 191    falsifierClass .c8MillerSpan = .workingMemorySpanReduction := rfl
 192
 193theorem c9_falsifier :
 194    falsifierClass .c9RegulatoryCeiling = .encodeTcgaRegulatoryModule := rfl
 195
 196theorem c3_observable :
 197    predictedObservable .c3OncologyTensor = .multiplicativeTherapyResponse := rfl
 198
 199theorem c5_failure :
 200    failureMode .c5AttentionTensor = .nonFortyPlateauSpectrum := rfl
 201
 202theorem c8_dataset :
 203    datasetClass .c8MillerSpan = .workingMemoryPerturbation := rfl
 204
 205theorem falsifierClass_injective : Function.Injective falsifierClass := by
 206  intro a b h
 207  cases a <;> cases b <;> simp [falsifierClass] at h ⊢
 208
 209theorem datasetClass_injective : Function.Injective datasetClass := by
 210  intro a b h
 211  cases a <;> cases b <;> simp [datasetClass] at h ⊢
 212
 213theorem predictedObservable_injective : Function.Injective predictedObservable := by
 214  intro a b h
 215  cases a <;> cases b <;> simp [predictedObservable] at h ⊢
 216
 217theorem failureMode_injective : Function.Injective failureMode := by
 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

papers checked against this theorem

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