theorem
proved
c8_dataset
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 202.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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