priorityBucketTotal
plain-language theorem explainer
The four priority buckets for empirical tests sum in length to nine. Developers of the Option A queue certification cite this to confirm the partition is exhaustive. The proof is a one-line rewrite substituting the four bucket-length theorems.
Claim. Let $I$, $H$, $M$, $D$ be the lists of immediate, high-priority, medium-priority, and deferred empirical tests respectively. Then $|I| + |H| + |M| + |D| = 9$.
background
The module defines a priority queue that records testing order for empirical protocols attached to C1-C9 theorems. It states explicitly that the queue supplies no evidence for the claims and only proves formal coverage by the empirical protocol. Immediate tests contain two CombinationIDs, high-priority tests contain three, deferred tests contain two; the medium-priority list completes the partition to nine items total. Upstream length theorems establish each bucket size via decide tactics.
proof idea
Term-mode proof applies rw to the four length theorems immediateTests_length, highPriorityTests_length, mediumPriorityTests_length, and deferredTests_length.
why it matters
The result feeds empiricalQueueCert, which records the four-priority structure and immediate/high assignments. It closes the queue-size accounting step inside the Option A empirical protocol module, ensuring the formal test list is fully partitioned before certification proceeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.