IndisputableMonolith.Foundation.OptionAEmpiricalProgram

   1import Mathlib
   2import IndisputableMonolith.Foundation.OptionAEmpiricalReadiness
   3
   4/-!
   5# Option A Empirical Program
   6
   7Single certificate for the first-pass empirical program attached to Option A.
   8The earlier modules prove the pieces separately: queue, schedule, actions,
   9deliverables, pipelines, and readiness. This file proves that the assembled
  10first-pass program is complete and collision-free at the metadata layer.
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Foundation
  17namespace OptionAEmpiricalProgram
  18
  19open OptionAFalsifierRegistry
  20open OptionAEmpiricalProtocol
  21open OptionAEmpiricalQueue
  22open OptionAEmpiricalSchedule
  23open OptionAEmpiricalActionPlan
  24open OptionAEmpiricalDeliverables
  25open OptionAEmpiricalPipeline
  26open OptionAEmpiricalReadiness
  27
  28/-- One executable row in the Option A first-pass empirical program. -/
  29structure ProgramSpec where
  30  combination : CombinationID
  31  protocol : ProtocolSpec
  32  priority : Priority
  33  action : AnalysisAction
  34  deliverable : Deliverable
  35  pipeline : PipelineSpec
  36  ready : EmpiricallyReady combination
  37
  38/-- Program row assigned to an implemented Option A combination. -/
  39def programSpec (c : CombinationID) : ProgramSpec where
  40  combination := c
  41  protocol := protocolSpec c
  42  priority := empiricalPriority c
  43  action := analysisAction c
  44  deliverable := deliverableFor c
  45  pipeline := pipelineSpec c
  46  ready := empiricallyReady_all c
  47
  48theorem programSpec_injective : Function.Injective programSpec := by
  49  intro a b h
  50  exact congrArg ProgramSpec.combination h
  51
  52/-- First-pass empirical program in execution order. -/
  53def firstPassProgram : List ProgramSpec :=
  54  firstPassSchedule.map programSpec
  55
  56theorem firstPassProgram_length :
  57    firstPassProgram.length = 5 := by
  58  unfold firstPassProgram
  59  rw [List.length_map, firstPassSchedule_length]
  60
  61theorem firstPassProgram_nodup :
  62    firstPassProgram.Nodup := by
  63  unfold firstPassProgram
  64  exact List.Nodup.map programSpec_injective firstPassSchedule_nodup
  65
  66/-- The first-pass program contains exactly the high-or-immediate tests. -/
  67theorem firstPassProgram_exact_top_priority (c : CombinationID) :
  68    c ∈ firstPassSchedule ↔ isHighOrImmediate c :=
  69  firstPassSchedule_mem_iff_high_or_immediate c
  70
  71theorem scheduled_program_ready
  72    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  73    (programSpec c).ready = empiricallyReady_all c :=
  74  rfl
  75
  76theorem scheduled_program_pipeline
  77    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  78    (programSpec c).pipeline = pipelineSpec c :=
  79  rfl
  80
  81theorem firstPassProgram_actions_nodup :
  82    firstPassActions.Nodup :=
  83  firstPassActions_nodup
  84
  85theorem firstPassProgram_deliverables_nodup :
  86    firstPassDeliverables.Nodup :=
  87  firstPassDeliverables_nodup
  88
  89theorem firstPassProgram_pipelines_nodup :
  90    firstPassPipelines.Nodup :=
  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 :
 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
 143