highPriorityTests_length
plain-language theorem explainer
The theorem asserts that the high-priority empirical tests list contains exactly three entries: the planet-strata, attention-tensor, and regulatory-ceiling combinations. Researchers verifying the empirical queue for the C1-C9 cross-domain theorems cite this length when confirming total test coverage. The proof is a one-line decision procedure that evaluates the concrete list definition directly.
Claim. Let $L$ be the list of high-priority empirical tests consisting of the planet-strata, attention-tensor, and regulatory-ceiling combinations. Then $|L| = 3$.
background
The module implements a priority queue that records which empirical protocols attached to the C1-C9 theorems should be tested first and proves each queued item is already covered by the formal empirical protocol. The highPriorityTests definition supplies the three medium-priority items that follow the immediate pair. This list is constructed explicitly as the planet-strata, attention-tensor, and regulatory-ceiling combinations.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable equality on list lengths, evaluating the concrete definition of highPriorityTests directly.
why it matters
The length fact is invoked inside priorityBucketTotal to establish that the four priority buckets sum to nine and inside empiricalQueueCert to populate the certified queue structure. It supplies a concrete accounting step that ensures the empirical test queue aligns with the nine cross-domain theorems in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.