 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 ↔
 162      c = .c2PlanetStrata ∨
 163      c = .c3OncologyTensor ∨
 164      c = .c5AttentionTensor ∨
 165      c = .c8MillerSpan ∨
 166      c = .c9RegulatoryCeiling
 167  immediate_count : immediateTests.length = 2
 168  high_count : highPriorityTests.length = 3
 169  medium_count : mediumPriorityTests.length = 2
 170  defer_count : deferredTests.length = 2
 171  bucket_total : immediateTests.length + highPriorityTests.length +
 172    mediumPriorityTests.length + deferredTests.length = 9
 173  immediate_exact : ∀ c : CombinationID,
 174    c ∈ immediateTests ↔ empiricalPriority c = .immediate
 175  high_exact : ∀ c : CombinationID,
 176    c ∈ highPriorityTests ↔ empiricalPriority c = .high
 177  medium_exact : ∀ c : CombinationID,
 178    c ∈ mediumPriorityTests ↔ empiricalPriority c = .medium
 179  defer_exact : ∀ c : CombinationID,

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.