pith. machine review for the scientific record. sign in
structure definition def or abbrev

EmpiricalQueueCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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,
 180    c ∈ deferredTests ↔ empiricalPriority c = .defer
 181

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.