module module

`IndisputableMonolith.Foundation.OptionAEmpiricalQueue`

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

used by (1)

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

IndisputableMonolith.Foundation.OptionAEmpiricalSchedule module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.OptionAEmpiricalProtocol module_import

declarations in this module (34)

inductive Priority L22
theorem priority_count L29
def empiricalPriority L33
def isImmediate L44
def isHighOrImmediate L47
theorem c3_immediate L50
theorem c8_immediate L52
theorem c5_high L54
theorem c2_high L56
theorem c9_high L58
theorem c3_protocol_covered L60
theorem c8_protocol_covered L64
theorem every_priority_has_protocol L68
theorem immediate_iff L73
theorem high_or_immediate_iff L78
def immediateTests L88
def highPriorityTests L92
def mediumPriorityTests L96
def deferredTests L100
theorem immediateTests_length L103
theorem highPriorityTests_length L106
theorem mediumPriorityTests_length L109
theorem deferredTests_length L112
theorem immediateTests_nodup L115
theorem highPriorityTests_nodup L118
theorem mediumPriorityTests_nodup L121
theorem deferredTests_nodup L124
theorem immediateTests_exact L127
theorem highPriorityTests_exact L131
theorem mediumPriorityTests_exact L135
theorem deferredTests_exact L139
theorem priorityBucketTotal L143
structure EmpiricalQueueCert L149
def empiricalQueueCert L182