firstPassPipelines_nodup
plain-language theorem explainer
The theorem shows that the list of first-pass pipeline records, formed by mapping the first-pass schedule through the pipeline specification function, contains no duplicate entries. Researchers certifying the Option A empirical pipeline for C1-C9 combinations would cite this to confirm uniqueness of scheduled records. The proof is a one-line wrapper that applies the preservation of the no-duplicates property under an injective map to the already-established nodup property of the schedule.
Claim. Let $S$ be the first-pass schedule and let $f$ be the injective pipeline specification map. The list $P = f(S)$ has all distinct elements.
background
The Option A Empirical Pipeline module constructs unified records for C1-C9 that combine protocol, priority, analysis action, and deliverable. The first-pass pipelines list is obtained directly by applying the pipeline specification map to the first-pass schedule. Pipeline specification is injective because it reduces to the injectivity of the underlying protocol specification. The schedule list itself is duplicate-free by direct verification. The map operation here acts on the schedule list while preserving the no-duplicates property when the function is injective.
proof idea
The proof first unfolds the definition of the first-pass pipelines list to expose it as the image of the schedule under the specification map. It then applies the general fact that mapping a list by an injective function preserves the no-duplicates property, citing the injectivity of the specification map and the no-duplicates property of the schedule.
why it matters
This result supplies the pipelines no-duplicates property required by the firstPassProgramComplete theorem and by the empiricalPipelineCert record. It closes one uniqueness gate in the first-pass program, supporting the overall certification that every scheduled row is ready and every output is distinct. In the Recognition Science setting this uniqueness is a prerequisite for consistent protocol application across the forcing chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.