`empiricalProgramCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalProgram
domain: Foundation
line: 127 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalProgram on GitHub at line 127.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 124  exact_top_priority :
 125    ∀ c : CombinationID, c ∈ firstPassSchedule ↔ isHighOrImmediate c
 126
 127def empiricalProgramCert : EmpiricalProgramCert where
 128  program_injective := programSpec_injective
 129  first_pass_length := firstPassProgram_length
 130  first_pass_nodup := firstPassProgram_nodup
 131  first_pass_ready := firstPassReady
 132  first_pass_complete := firstPassProgramComplete
 133  scheduled_ready := scheduled_program_ready
 134  scheduled_pipeline := scheduled_program_pipeline
 135  action_classes_nodup := firstPassProgram_actions_nodup
 136  deliverable_classes_nodup := firstPassProgram_deliverables_nodup
 137  pipeline_records_nodup := firstPassProgram_pipelines_nodup
 138  exact_top_priority := firstPassProgram_exact_top_priority
 139
 140end OptionAEmpiricalProgram
 141end Foundation
 142end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.