mediumPriorityTests_nodup
plain-language theorem explainer
The theorem asserts that the medium-priority empirical tests list contains no duplicate entries. Researchers maintaining the formal empirical validation queue for C1-C9 cross-domain theorems would cite it to confirm queue integrity before protocol execution. The proof reduces immediately to a decidable check on the explicit two-element list definition.
Claim. The list consisting of the cognitive tensor combination identifier and the universal response combination identifier satisfies the no-duplicates property.
background
The module establishes a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols to test first and proves each queued item is already covered by the formal empirical protocol, with zero sorry or axiom in the file. The upstream definition supplies the concrete list mediumPriorityTests as the two-element sequence containing the cognitive tensor and universal response identifiers.
proof idea
This is a one-line wrapper that applies the decide tactic to the decidable Nodup predicate on the list.
why it matters
The result guarantees well-formedness of the medium-priority segment of the empirical queue. It supports the module's guarantee that every queued protocol is formally covered, feeding the overall Option A empirical protocol structure without introducing duplicates that could corrupt test ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.