firstPassSchedule_mem_protocol

formal source

  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