highPriorityTests_nodup
plain-language theorem explainer
The list of high-priority empirical tests contains no duplicate combination identifiers. A researcher auditing the Option A queue would cite this to confirm the test set is free of repetition before running protocols. The proof is a one-line decision procedure that computes the no-duplicates property directly on the explicit three-element list.
Claim. The list consisting of the combination identifiers for planet strata, attention tensor, and regulatory ceiling satisfies the no-duplicates property.
background
The module constructs a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols to test first and proves formal coverage by the empirical protocol, with zero sorry or axiom in the file. The upstream definition supplies the concrete list of three combination identifiers for the high-priority tier.
proof idea
The proof is a one-line wrapper that applies the decidable check for the no-duplicates predicate to the explicitly given list.
why it matters
This declaration ensures the high-priority segment of the empirical queue is well-formed. It supports the module's overall claim that every queued item is already covered by the formal empirical protocol. In the Recognition framework it contributes to clean data structures for the C-series empirical validation steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.