`is`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalProgram
domain: Foundation
line: 94 · 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 94.

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

used by

formal source

  91  firstPassPipelines_nodup
  92
  93/-- First-pass completion gate: every scheduled row is ready and every output
  94class is collision-free. -/
  95def FirstPassProgramComplete : Prop :=
  96  FirstPassReady ∧
  97    firstPassProgram.length = 5 ∧
  98    firstPassProgram.Nodup ∧
  99    firstPassActions.Nodup ∧
 100    firstPassDeliverables.Nodup ∧
 101    firstPassPipelines.Nodup ∧
 102    (∀ c : CombinationID, c ∈ firstPassSchedule ↔ isHighOrImmediate c)
 103
 104theorem firstPassProgramComplete : FirstPassProgramComplete := by
 105  exact ⟨firstPassReady, firstPassProgram_length, firstPassProgram_nodup,
 106    firstPassActions_nodup, firstPassDeliverables_nodup,
 107    firstPassPipelines_nodup, firstPassSchedule_mem_iff_high_or_immediate⟩
 108
 109structure EmpiricalProgramCert where
 110  program_injective : Function.Injective programSpec
 111  first_pass_length : firstPassProgram.length = 5
 112  first_pass_nodup : firstPassProgram.Nodup
 113  first_pass_ready : FirstPassReady
 114  first_pass_complete : FirstPassProgramComplete
 115  scheduled_ready :
 116    ∀ {c : CombinationID}, c ∈ firstPassSchedule →
 117      (programSpec c).ready = empiricallyReady_all c
 118  scheduled_pipeline :
 119    ∀ {c : CombinationID}, c ∈ firstPassSchedule →
 120      (programSpec c).pipeline = pipelineSpec c
 121  action_classes_nodup : firstPassActions.Nodup
 122  deliverable_classes_nodup : firstPassDeliverables.Nodup
 123  pipeline_records_nodup : firstPassPipelines.Nodup
 124  exact_top_priority :

papers checked against this theorem

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