firstPassPipelines
plain-language theorem explainer
firstPassPipelines constructs the ordered list of five PipelineSpec records by mapping the pipeline constructor over the predefined first-pass schedule of CombinationIDs. Analysts certifying empirical completeness for Option A would cite this list when establishing length, nodup, and readiness properties. The definition is a one-line wrapper applying the map operation from the measurement core to the schedule list.
Claim. The ordered list of pipeline records is the image of the first-pass schedule list under the map sending each combination identifier $c$ to the record containing protocol specification, priority, analysis action, and deliverable for $c$.
background
PipelineSpec is the structure that records the full empirical execution details for an Option A combination, consisting of protocol, priority, analysis action, and deliverable fields. The module supplies unified records for C1-C9 combinations in the Option A empirical pipeline with zero sorry or axiom. Upstream, firstPassSchedule supplies the ordered list of five CombinationIDs, while pipelineSpec constructs the full record for any given combination by assigning the corresponding protocolSpec, empiricalPriority, analysisAction, and deliverableFor values.
proof idea
This definition is a one-line wrapper that applies the map function to firstPassSchedule using the pipelineSpec constructor.
why it matters
This definition supplies the concrete list of pipeline records that populates EmpiricalPipelineCert and enables the length and nodup theorems. It feeds directly into FirstPassProgramComplete and the program-level nodup result. In the Recognition Science framework it implements the first-pass empirical validation step for Option A, linking schedule order to deliverables without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.