firstPassProgram_pipelines_nodup
plain-language theorem explainer
The theorem states that the list of first-pass pipeline specifications contains no duplicates. It is cited when constructing the empirical program certificate to confirm metadata collision-freeness for Option A. The proof is a one-line wrapper that directly applies the upstream nodup result on the mapped schedule.
Claim. The list of pipeline specifications obtained by mapping the pipeline specification function over the first-pass schedule is duplicate-free: firstPassPipelines.Nodup.
background
The module assembles prior results on queue, schedule, actions, deliverables, pipelines, and readiness into a single certificate showing the first-pass empirical program is complete and collision-free at the metadata layer. firstPassPipelines is defined as firstPassSchedule.map pipelineSpec, the list of PipelineSpec records in schedule order. The upstream theorem firstPassPipelines_nodup establishes the nodup property via List.Nodup.map applied to pipelineSpec_injective and firstPassSchedule_nodup.
proof idea
The proof is a one-line wrapper that invokes firstPassPipelines_nodup.
why it matters
This supplies the pipelines nodup component to empiricalProgramCert, completing the collision-free metadata claim for the assembled first-pass program. It fills the metadata uniqueness slot in the Option A certificate construction described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.