mediumPriorityTests_nodup
plain-language theorem explainer
The declaration proves that the list of medium-priority empirical tests contains no duplicate CombinationIDs. Maintainers of the empirical protocol queue cite this to confirm the test list is well-formed. The proof is a one-line application of the decide tactic that evaluates the decidable no-duplicates predicate on the two-element list.
Claim. Let $L$ be the list consisting of the cognitive tensor test and the universal response test. Then $L$ contains no duplicate elements.
background
The Option A Empirical Queue module defines a priority system for empirical tests tied to the C1-C9 cross-domain theorems. It records which protocols should be tested first and includes formal proofs that every queued item is already covered by the empirical protocol, with zero sorry or axiom in the module. The upstream definition specifies the medium-priority tests as the list containing the cognitive tensor combination and the universal response combination.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic succeeds because the no-duplicates property for a finite list of CombinationIDs is decidable and evaluates to true for the two distinct elements present.
why it matters
This theorem ensures the medium-priority queue remains free of repetition, supporting the module's overall claim that queued items are covered by the formal protocol. It sits in the foundation layer for empirical testing order but does not engage the main forcing chain, the Recognition Composition Law, or constants such as phi and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.