mediumPriorityTests_length
plain-language theorem explainer
The theorem establishes that the medium-priority empirical tests list contains exactly two entries. Researchers certifying the overall empirical queue coverage in Recognition Science cite this length when summing bucket sizes to confirm nine total tests. The proof evaluates the explicit list definition by direct decidable computation.
Claim. Let $M$ be the list of medium-priority empirical tests consisting of the cognitive tensor and universal response combinations. Then $|M| = 2$.
background
The module maintains a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols should be tested first and proves that every queued item is already covered by the formal empirical protocol. The upstream definition mediumPriorityTests constructs the list as [.c1CognitiveTensor, .c7UniversalResponse].
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the length of the explicitly constructed list.
why it matters
This length fact is invoked by priorityBucketTotal to obtain the total of nine tests across all priority buckets and by empiricalQueueCert to certify the queue structure. It fills the empirical validation layer for the C1-C9 theorems in the Recognition framework without supplying actual empirical data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.