theorem
proved
c5_falsifier
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 181.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
178theorem c4_falsifier :
179 falsifierClass .c4QuantumMolecularDepth = .quantumCircuitDepth := rfl
180
181theorem c5_falsifier :
182 falsifierClass .c5AttentionTensor = .attentionBlinkPlateaus := rfl
183
184theorem c6_falsifier :
185 falsifierClass .c6EriksonReverse = .adniDementiaProgression := rfl
186
187theorem c7_falsifier :
188 falsifierClass .c7UniversalResponse = .crossFieldEquilibriumResponse := rfl
189
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 ⊢