module module

`IndisputableMonolith.Foundation.OptionAFalsifierRegistry`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.OptionAEmpiricalProtocol module_import

declarations in this module (35)

inductive CombinationID L19
theorem combinationID_count L31
inductive TestClass L35
theorem testClass_count L47
inductive EmpiricalStatus L51
theorem empiricalStatus_count L57
inductive DatasetClass L61
theorem datasetClass_count L73
inductive PredictedObservable L77
theorem predictedObservable_count L89
inductive FailureMode L93
theorem failureMode_count L105
def falsifierClass L109
def empiricalStatus L122
def datasetClass L134
def predictedObservable L146
def failureMode L158
theorem c1_falsifier L169
theorem c2_falsifier L172
theorem c3_falsifier L175
theorem c4_falsifier L178
theorem c5_falsifier L181
theorem c6_falsifier L184
theorem c7_falsifier L187
theorem c8_falsifier L190
theorem c9_falsifier L193
theorem c3_observable L196
theorem c5_failure L199
theorem c8_dataset L202
theorem falsifierClass_injective L205
theorem datasetClass_injective L209
theorem predictedObservable_injective L213
theorem failureMode_injective L217
structure FalsifierRegistryCert L221
def falsifierRegistryCert L248