module module

`IndisputableMonolith.Foundation.OptionAEmpiricalReadiness`

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.OptionAEmpiricalProgram module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.OptionAEmpiricalPipeline module_import

declarations in this module (12)

def EmpiricallyReady L30
theorem empiricallyReady_all L36
theorem scheduled_empiricallyReady L41
theorem c3_ready L46
theorem c8_ready L49
theorem c5_ready L52
def FirstPassReady L56
theorem firstPassReady L59
def AllImplementedReady L64
theorem allImplementedReady L67
structure EmpiricalReadinessCert L70
def empiricalReadinessCert L77