immediateTests_length
plain-language theorem explainer
The length of the immediate empirical tests list equals two. Researchers formalizing the priority queue for C1-C9 cross-domain theorem validation cite this to fix the size of the first bucket. The proof is a one-line decision procedure that evaluates the constant list definition directly.
Claim. The length of the list of immediate empirical tests equals 2.
background
The Option A Empirical Queue module defines a priority queue that records which protocols attached to the C1-C9 cross-domain theorems should be tested first. It proves every queued item is already covered by the formal empirical protocol but supplies no empirical evidence itself. The immediate tests are the two combination identifiers for the oncology tensor and Miller span cases.
proof idea
The proof is a one-line decision procedure that evaluates the explicit list definition and confirms its length equals two.
why it matters
This result is invoked by priorityBucketTotal to establish that the four priority buckets sum to nine items and by empiricalQueueCert to certify the queue structure. It contributes to the formal bookkeeping layer that tracks empirical protocols for the cross-domain theorems in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.