theorem
proved
mediumPriorityTests_nodup
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalQueue on GitHub at line 121.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
118theorem highPriorityTests_nodup : highPriorityTests.Nodup := by
119 decide
120
121theorem mediumPriorityTests_nodup : mediumPriorityTests.Nodup := by
122 decide
123
124theorem deferredTests_nodup : deferredTests.Nodup := by
125 decide
126
127theorem immediateTests_exact (c : CombinationID) :
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