deferredTests_length
plain-language theorem explainer
The theorem establishes that the deferred empirical tests list has length exactly two. Researchers verifying the total coverage of the Option A priority queue for C1-C9 cross-domain theorems would cite this fact when summing bucket lengths. The proof is a one-line decision procedure that computes the length directly from the explicit two-element list definition.
Claim. The length of the deferred empirical tests list equals 2, where the list consists of the quantum molecular depth test and the Erikson reverse test.
background
The Option A Empirical Queue module defines a priority queue that records which protocols should be tested first for the C1-C9 cross-domain theorems while proving formal coverage by the empirical protocol. The upstream deferredTests definition supplies the explicit list [.c4QuantumMolecularDepth, .c6EriksonReverse] of CombinationID values. This length theorem sits inside the same module and is invoked by sibling results that aggregate bucket sizes.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the length of the explicitly defined two-element list by decidable computation.
why it matters
This length fact is used in the priorityBucketTotal theorem to rewrite the sum of immediate, high, medium, and deferred bucket lengths to 9. It also supports the empiricalQueueCert structure that certifies the overall queue organization. Within the Recognition Science framework it closes a bookkeeping step for the empirical validation layer attached to the C1-C9 theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.