firstPassProgram_pipelines_nodup
plain-language theorem explainer
The list of first-pass pipeline specifications contains no duplicate entries. Researchers assembling the Option A empirical program certificate cite this to confirm metadata collision-freeness for the pipeline component. The proof is a direct term reduction to the no-duplicates result on the mapped schedule.
Claim. The sequence of pipeline specifications obtained by mapping the specification function over the first-pass schedule contains no repeated entries.
background
The Option A empirical program module assembles a single certificate for the first-pass program, confirming completeness and collision-freeness at the metadata layer after separate proofs for queue, schedule, actions, deliverables, pipelines, and readiness. First-pass pipelines are the list of pipeline records produced in schedule order. The upstream no-duplicates theorem for these pipelines follows from unfolding the map definition and applying the injectivity of the pipeline specification map to the already-proven no-duplicates property of the schedule.
proof idea
The proof is a one-line term wrapper that applies the no-duplicates theorem for first-pass pipelines.
why it matters
This result supplies the pipelines no-duplicates condition required by the empirical program certificate. It closes one piece of the metadata collision-free property for the assembled first-pass program. The certificate definition collects length, readiness, completeness, and injectivity facts to certify the Option A program as ready without internal conflicts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.