theorem
proved
failureMode_injective
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 217.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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