def
definition
falsifierRegistryCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 248.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
c1_falsifier -
c2_falsifier -
c3_falsifier -
c3_observable -
c4_falsifier -
c5_failure -
c5_falsifier -
c6_falsifier -
c7_falsifier -
c8_dataset -
c8_falsifier -
c9_falsifier -
combinationID_count -
datasetClass_count -
datasetClass_injective -
empiricalStatus_count -
failureMode_count -
failureMode_injective -
falsifierClass_injective -
FalsifierRegistryCert -
predictedObservable_count -
predictedObservable_injective -
testClass_count
formal source
245 observable_injective : Function.Injective predictedObservable
246 failure_mode_injective : Function.Injective failureMode
247
248def falsifierRegistryCert : FalsifierRegistryCert where
249 nine_combinations := combinationID_count
250 nine_test_classes := testClass_count
251 three_statuses := empiricalStatus_count
252 nine_dataset_classes := datasetClass_count
253 nine_observables := predictedObservable_count
254 nine_failure_modes := failureMode_count
255 c1_test := c1_falsifier
256 c2_test := c2_falsifier
257 c3_test := c3_falsifier
258 c4_test := c4_falsifier
259 c5_test := c5_falsifier
260 c6_test := c6_falsifier
261 c7_test := c7_falsifier
262 c8_test := c8_falsifier
263 c9_test := c9_falsifier
264 c3_predicted_observable := c3_observable
265 c5_failure_mode := c5_failure
266 c8_dataset_class := c8_dataset
267 test_class_injective := falsifierClass_injective
268 dataset_class_injective := datasetClass_injective
269 observable_injective := predictedObservable_injective
270 failure_mode_injective := failureMode_injective
271
272end OptionAFalsifierRegistry
273end Foundation
274end IndisputableMonolith