deferredTests_exact
plain-language theorem explainer
The theorem equates membership of a CombinationID in the deferredTests list with assignment of defer priority by the empiricalPriority map. Researchers maintaining the Option A empirical queue cite it to lock the testing order for cross-domain protocols. The proof is a one-line wrapper that performs exhaustive case analysis on the identifier and simplifies using the explicit list and priority definitions.
Claim. For any combination identifier $c$, $c$ belongs to the list of deferred empirical tests if and only if the empirical priority of $c$ equals defer.
background
The module implements 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 deferredTests definition enumerates the specific combinations [.c4QuantumMolecularDepth, .c6EriksonReverse]. The empiricalPriority function maps c3OncologyTensor and c8MillerSpan to immediate, c5AttentionTensor and c2PlanetStrata to high, and c1CognitiveTensor to medium, with the remaining identifiers receiving defer.
proof idea
The proof performs case analysis on the CombinationID c. It then simplifies the membership statement against the concrete list in deferredTests and the pattern match in empiricalPriority.
why it matters
This result feeds the empiricalQueueCert definition, which assembles the four priority counts and immediate/high flags. It supplies a verification step inside the Option A empirical queue, confirming that the deferred list exactly matches the defer category without touching the underlying physical claims or the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.