def
definition
predictedObservable
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 146.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
143 | .c9RegulatoryCeiling => .encodeTcgaRegulatory
144
145/-- Predicted observable assigned to each implemented combination. -/
146def predictedObservable : CombinationID → PredictedObservable
147 | .c1CognitiveTensor => .tensorRank125
148 | .c2PlanetStrata => .strataRatioPhiPower
149 | .c3OncologyTensor => .multiplicativeTherapyResponse
150 | .c4QuantumMolecularDepth => .fiveBitAddressBound
151 | .c5AttentionTensor => .fortyStableFiveTransient
152 | .c6EriksonReverse => .reverseEriksonOrder
153 | .c7UniversalResponse => .unitResponseCoefficient
154 | .c8MillerSpan => .qSpaceSpanSequence
155 | .c9RegulatoryCeiling => .regulatoryCeiling70
156
157/-- Failure mode assigned to each implemented combination. -/
158def failureMode : CombinationID → FailureMode
159 | .c1CognitiveTensor => .singleAxisDecoderSuffices
160 | .c2PlanetStrata => .noSmallPhiPowerRatio
161 | .c3OncologyTensor => .additiveTherapyResponse
162 | .c4QuantumMolecularDepth => .depthExceedsFiveBits
163 | .c5AttentionTensor => .nonFortyPlateauSpectrum
164 | .c6EriksonReverse => .nonReverseDementiaOrder
165 | .c7UniversalResponse => .nonUnitSharedCoefficient
166 | .c8MillerSpan => .nonQSpaceSpanCollapse
167 | .c9RegulatoryCeiling => .moduleExceedsCeiling70
168
169theorem c1_falsifier :
170 falsifierClass .c1CognitiveTensor = .eegDecoder := rfl
171
172theorem c2_falsifier :
173 falsifierClass .c2PlanetStrata = .seismicAtmosphericRatio := rfl
174
175theorem c3_falsifier :
176 falsifierClass .c3OncologyTensor = .tcgaClinicalResponse := rfl