IndisputableMonolith.Foundation.OptionAEmpiricalSchedule

   1import Mathlib
   2import IndisputableMonolith.Foundation.OptionAEmpiricalQueue
   3
   4/-!
   5# Option A Empirical Schedule
   6
   7Ordered schedule for the first five empirical tests attached to Option A.
   8
   9The queue module assigns priorities. This module fixes an explicit execution
  10order for the high-value tests and proves that every scheduled item is
  11high-or-immediate and protocol-covered.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace OptionAEmpiricalSchedule
  19
  20open OptionAFalsifierRegistry
  21open OptionAEmpiricalProtocol
  22open OptionAEmpiricalQueue
  23
  24/-- First-pass empirical test order. -/
  25def firstPassSchedule : List CombinationID :=
  26  [ .c3OncologyTensor
  27  , .c8MillerSpan
  28  , .c5AttentionTensor
  29  , .c9RegulatoryCeiling
  30  , .c2PlanetStrata
  31  ]
  32
  33theorem firstPassSchedule_length :
  34    firstPassSchedule.length = 5 := by
  35  decide
  36
  37theorem firstPassSchedule_head :
  38    firstPassSchedule.head? = some .c3OncologyTensor := by
  39  decide
  40
  41theorem firstPassSchedule_second :
  42    firstPassSchedule[1]? = some .c8MillerSpan := by
  43  decide
  44
  45theorem firstPassSchedule_third :
  46    firstPassSchedule[2]? = some .c5AttentionTensor := by
  47  decide
  48
  49theorem firstPassSchedule_nodup :
  50    firstPassSchedule.Nodup := by
  51  decide
  52
  53theorem firstPassSchedule_mem_high_or_immediate
  54    {c : CombinationID} (h : c ∈ firstPassSchedule) :
  55    isHighOrImmediate c := by
  56  simp [firstPassSchedule] at h
  57  rcases h with h | h | h | h | h
  58  · subst h
  59    simp [isHighOrImmediate, empiricalPriority]
  60  · subst h
  61    simp [isHighOrImmediate, empiricalPriority]
  62  · subst h
  63    simp [isHighOrImmediate, empiricalPriority]
  64  · subst h
  65    simp [isHighOrImmediate, empiricalPriority]
  66  · subst h
  67    simp [isHighOrImmediate, empiricalPriority]
  68
  69/-- The first-pass schedule contains exactly the high-or-immediate tests. -/
  70theorem firstPassSchedule_mem_iff_high_or_immediate (c : CombinationID) :
  71    c ∈ firstPassSchedule ↔ isHighOrImmediate c := by
  72  cases c <;> simp [firstPassSchedule, isHighOrImmediate, empiricalPriority]
  73
  74theorem firstPassSchedule_mem_protocol
  75    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  76    ProtocolFalsifiable c :=
  77  protocolFalsifiable_all c
  78
  79structure EmpiricalScheduleCert where
  80  length_five : firstPassSchedule.length = 5
  81  head_c3 : firstPassSchedule.head? = some .c3OncologyTensor
  82  second_c8 : firstPassSchedule[1]? = some .c8MillerSpan
  83  third_c5 : firstPassSchedule[2]? = some .c5AttentionTensor
  84  no_duplicates : firstPassSchedule.Nodup
  85  scheduled_high_or_immediate :
  86    ∀ {c : CombinationID}, c ∈ firstPassSchedule → isHighOrImmediate c
  87  schedule_exactly_top_priority :
  88    ∀ c : CombinationID, c ∈ firstPassSchedule ↔ isHighOrImmediate c
  89  scheduled_protocol :
  90    ∀ {c : CombinationID}, c ∈ firstPassSchedule → ProtocolFalsifiable c
  91
  92def empiricalScheduleCert : EmpiricalScheduleCert where
  93  length_five := firstPassSchedule_length
  94  head_c3 := firstPassSchedule_head
  95  second_c8 := firstPassSchedule_second
  96  third_c5 := firstPassSchedule_third
  97  no_duplicates := firstPassSchedule_nodup
  98  scheduled_high_or_immediate := firstPassSchedule_mem_high_or_immediate
  99  schedule_exactly_top_priority := firstPassSchedule_mem_iff_high_or_immediate
 100  scheduled_protocol := firstPassSchedule_mem_protocol
 101
 102end OptionAEmpiricalSchedule
 103end Foundation
 104end IndisputableMonolith
 105