IndisputableMonolith.Foundation.OptionAEmpiricalPipeline

   1import Mathlib
   2import IndisputableMonolith.Foundation.OptionAEmpiricalDeliverables
   3
   4/-!
   5# Option A Empirical Pipeline
   6
   7Unified empirical pipeline record for C1-C9. This ties together protocol,
   8priority, analysis action, and deliverable for every implemented Option A
   9combination.
  10
  11Lean status: 0 sorry, 0 axiom.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Foundation
  16namespace OptionAEmpiricalPipeline
  17
  18open OptionAFalsifierRegistry
  19open OptionAEmpiricalProtocol
  20open OptionAEmpiricalQueue
  21open OptionAEmpiricalSchedule
  22open OptionAEmpiricalActionPlan
  23open OptionAEmpiricalDeliverables
  24
  25/-- Full empirical execution record for an Option A combination. -/
  26structure PipelineSpec where
  27  protocol : ProtocolSpec
  28  priority : Priority
  29  action : AnalysisAction
  30  deliverable : Deliverable
  31  deriving DecidableEq, Repr
  32
  33/-- Pipeline record assigned to each C1-C9 combination. -/
  34def pipelineSpec (c : CombinationID) : PipelineSpec where
  35  protocol := protocolSpec c
  36  priority := empiricalPriority c
  37  action := analysisAction c
  38  deliverable := deliverableFor c
  39
  40theorem pipelineSpec_injective : Function.Injective pipelineSpec := by
  41  intro a b h
  42  apply protocolSpec_injective
  43  exact congrArg PipelineSpec.protocol h
  44
  45theorem pipelineSpec_eq_iff (a b : CombinationID) :
  46    pipelineSpec a = pipelineSpec b ↔ a = b := by
  47  constructor
  48  · intro h
  49    exact pipelineSpec_injective h
  50  · intro h
  51    rw [h]
  52
  53/-- A combination has a full empirical pipeline iff a pipeline record exists. -/
  54def HasPipeline (c : CombinationID) : Prop :=
  55  ∃ p : PipelineSpec, pipelineSpec c = p
  56
  57theorem hasPipeline_all (c : CombinationID) : HasPipeline c := by
  58  exact ⟨pipelineSpec c, rfl⟩
  59
  60theorem scheduled_has_pipeline
  61    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  62    HasPipeline c :=
  63  hasPipeline_all c
  64
  65/-- First-pass pipeline records in schedule order. -/
  66def firstPassPipelines : List PipelineSpec :=
  67  firstPassSchedule.map pipelineSpec
  68
  69theorem firstPassPipelines_length :
  70    firstPassPipelines.length = 5 := by
  71  unfold firstPassPipelines
  72  rw [List.length_map, firstPassSchedule_length]
  73
  74theorem firstPassPipelines_nodup :
  75    firstPassPipelines.Nodup := by
  76  unfold firstPassPipelines
  77  exact List.Nodup.map pipelineSpec_injective firstPassSchedule_nodup
  78
  79theorem c3_pipeline_priority :
  80    (pipelineSpec .c3OncologyTensor).priority = .immediate := rfl
  81
  82theorem c3_pipeline_action :
  83    (pipelineSpec .c3OncologyTensor).action = .fitFactorModel := rfl
  84
  85theorem c3_pipeline_deliverable :
  86    (pipelineSpec .c3OncologyTensor).deliverable = .oncologyFactorModelNotebook := rfl
  87
  88theorem c8_pipeline_priority :
  89    (pipelineSpec .c8MillerSpan).priority = .immediate := rfl
  90
  91theorem c8_pipeline_action :
  92    (pipelineSpec .c8MillerSpan).action = .fitDiscreteCollapse := rfl
  93
  94theorem c8_pipeline_deliverable :
  95    (pipelineSpec .c8MillerSpan).deliverable = .memoryCollapseNotebook := rfl
  96
  97structure EmpiricalPipelineCert where
  98  pipeline_injective : Function.Injective pipelineSpec
  99  pipeline_eq_iff : ∀ a b : CombinationID, pipelineSpec a = pipelineSpec b ↔ a = b
 100  all_have_pipeline : ∀ c : CombinationID, HasPipeline c
 101  scheduled_have_pipeline :
 102    ∀ {c : CombinationID}, c ∈ firstPassSchedule → HasPipeline c
 103  first_pass_length : firstPassPipelines.length = 5
 104  first_pass_nodup : firstPassPipelines.Nodup
 105  c3_priority : (pipelineSpec .c3OncologyTensor).priority = .immediate
 106  c3_action : (pipelineSpec .c3OncologyTensor).action = .fitFactorModel
 107  c3_deliverable :
 108    (pipelineSpec .c3OncologyTensor).deliverable = .oncologyFactorModelNotebook
 109  c8_priority : (pipelineSpec .c8MillerSpan).priority = .immediate
 110  c8_action : (pipelineSpec .c8MillerSpan).action = .fitDiscreteCollapse
 111  c8_deliverable :
 112    (pipelineSpec .c8MillerSpan).deliverable = .memoryCollapseNotebook
 113
 114def empiricalPipelineCert : EmpiricalPipelineCert where
 115  pipeline_injective := pipelineSpec_injective
 116  pipeline_eq_iff := pipelineSpec_eq_iff
 117  all_have_pipeline := hasPipeline_all
 118  scheduled_have_pipeline := scheduled_has_pipeline
 119  first_pass_length := firstPassPipelines_length
 120  first_pass_nodup := firstPassPipelines_nodup
 121  c3_priority := c3_pipeline_priority
 122  c3_action := c3_pipeline_action
 123  c3_deliverable := c3_pipeline_deliverable
 124  c8_priority := c8_pipeline_priority
 125  c8_action := c8_pipeline_action
 126  c8_deliverable := c8_pipeline_deliverable
 127
 128end OptionAEmpiricalPipeline
 129end Foundation
 130end IndisputableMonolith
 131