highPriorityTests_exact

formal source

 128    c ∈ immediateTests ↔ empiricalPriority c = .immediate := by
 129  cases c <;> simp [immediateTests, empiricalPriority]
 130
 131theorem highPriorityTests_exact (c : CombinationID) :
 132    c ∈ highPriorityTests ↔ empiricalPriority c = .high := by
 133  cases c <;> simp [highPriorityTests, empiricalPriority]
 134
 135theorem mediumPriorityTests_exact (c : CombinationID) :
 136    c ∈ mediumPriorityTests ↔ empiricalPriority c = .medium := by
 137  cases c <;> simp [mediumPriorityTests, empiricalPriority]
 138
 139theorem deferredTests_exact (c : CombinationID) :
 140    c ∈ deferredTests ↔ empiricalPriority c = .defer := by
 141  cases c <;> simp [deferredTests, empiricalPriority]
 142
 143theorem priorityBucketTotal :
 144    immediateTests.length + highPriorityTests.length +
 145      mediumPriorityTests.length + deferredTests.length = 9 := by
 146  rw [immediateTests_length, highPriorityTests_length,
 147    mediumPriorityTests_length, deferredTests_length]
 148
 149structure EmpiricalQueueCert where
 150  four_priorities : Fintype.card Priority = 4
 151  c3_now : isImmediate .c3OncologyTensor
 152  c8_now : isImmediate .c8MillerSpan
 153  c5_next : empiricalPriority .c5AttentionTensor = .high
 154  c2_next : empiricalPriority .c2PlanetStrata = .high
 155  c9_next : empiricalPriority .c9RegulatoryCeiling = .high
 156  all_have_protocol : ∀ c : CombinationID, ProtocolFalsifiable c
 157  immediate_classification :
 158    ∀ c : CombinationID, isImmediate c ↔
 159      c = .c3OncologyTensor ∨ c = .c8MillerSpan
 160  high_or_immediate_classification :
 161    ∀ c : CombinationID, isHighOrImmediate c ↔