immediateTests_nodup
plain-language theorem explainer
The declaration proves the immediate empirical tests list contains no duplicate CombinationIDs. Researchers building the priority queue for C1-C9 cross-domain theorems cite it to confirm the top items are distinct before protocol execution. The proof is a one-line wrapper that applies the decide tactic to resolve the nodup predicate via decidable equality on the list elements.
Claim. The list consisting of the oncology tensor combination and the Miller span combination contains no duplicate elements.
background
The module constructs a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. immediateTests is defined as the list of highest-priority items: the oncology tensor and Miller span combinations. The nodup property asserts that every queued item appears at most once, which supports the claim that the queue records distinct protocols to test first.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the nodup predicate for the immediateTests list, relying on decidable equality for CombinationID.
why it matters
This result ensures the immediate test queue is well-formed and feeds into downstream coverage statements for the empirical protocol. It aligns with the framework's requirement that every queued item is already covered by the formal empirical protocol, closing a basic integrity check with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.