firstPassSchedule_nodup
plain-language theorem explainer
The theorem proves that the explicit first-pass empirical test list contains no duplicate CombinationIDs. Downstream results on pipelines, programs, and the schedule certificate cite it to guarantee uniqueness in the initial sequence. The proof is a one-line decision procedure that verifies the Nodup property by direct computation on the finite list.
Claim. The list firstPassSchedule is duplicate-free: $Nodup(firstPassSchedule)$.
background
The module defines an ordered schedule for the first five empirical tests attached to Option A. The upstream definition firstPassSchedule supplies the concrete list [.c3OncologyTensor, .c8MillerSpan, .c5AttentionTensor, .c9RegulatoryCeiling, .c2PlanetStrata]. This fixes an execution order for high-value tests while the surrounding proofs establish that every scheduled item is high-or-immediate and protocol-covered.
proof idea
The proof is a one-line wrapper that applies the decide tactic to discharge the Nodup goal by exhaustive decidable checking of the explicit list.
why it matters
It is invoked by firstPassPipelines_nodup and firstPassProgram_nodup via List.Nodup.map with injective specifications, and is packaged inside empiricalScheduleCert. The result closes the no-duplicates requirement for the Option A empirical foundation, supporting certified construction of the initial test sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.