module module

`IndisputableMonolith.Foundation.OptionAEmpiricalProgram`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.OptionAEmpiricalReadiness module_import

declarations in this module (17)

structure ProgramSpec L29
def programSpec L39
theorem programSpec_injective L48
def firstPassProgram L53
theorem firstPassProgram_length L56
theorem firstPassProgram_nodup L61
theorem firstPassProgram_exact_top_priority L67
theorem scheduled_program_ready L71
theorem scheduled_program_pipeline L76
theorem firstPassProgram_actions_nodup L81
theorem firstPassProgram_deliverables_nodup L85
theorem firstPassProgram_pipelines_nodup L89
class is L94
def FirstPassProgramComplete L95
theorem firstPassProgramComplete L104
structure EmpiricalProgramCert L109
def empiricalProgramCert L127