firstPassProgram_pipelines_nodup
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish no-duplicates for actions or deliverables components.
- Does not address runtime execution or empirical data validation.
- Does not cover higher-order program semantics beyond metadata.
formal statement (Lean)
89theorem firstPassProgram_pipelines_nodup :
90 firstPassPipelines.Nodup :=
proof body
Term-mode proof.
91 firstPassPipelines_nodup
92
93/-- First-pass completion gate: every scheduled row is ready and every output