pipelineSpec_injective
plain-language theorem explainer
The map sending each C1-C9 combination identifier to its full empirical pipeline record is injective. Researchers certifying Option A deliverables cite this to guarantee that distinct combinations produce distinct execution records. The proof reduces the claim to the already-established injectivity of the protocol component by projecting onto the protocol field.
Claim. The function mapping each combination identifier to its empirical execution record (protocol specification, priority, analysis action, and deliverable) is injective.
background
The module assembles a single empirical pipeline record for every C1-C9 combination under Option A. PipelineSpec is the structure that packages a protocol record, a priority value, an analysis action, and a deliverable. The function pipelineSpec builds each such record by delegating the protocol field to protocolSpec while filling the remaining fields from empiricalPriority, analysisAction, and deliverableFor. This construction sits on top of the prior theorem that protocolSpec itself is injective, which is proved by reducing to datasetClass_injective via the dataset field.
proof idea
The proof is a one-line wrapper. It assumes two combinations a and b whose pipeline records are equal, extracts equality of their protocol components by congrArg on the protocol field of PipelineSpec, and feeds that equality directly into protocolSpec_injective.
why it matters
The result supplies the injectivity clause required by empiricalPipelineCert and is invoked by firstPassPipelines_nodup to obtain a duplicate-free list via List.Nodup.map. It therefore closes the uniqueness step for the Option A empirical pipeline inside the Recognition Science foundation, ensuring that the C1-C9 combinations remain distinguishable at the level of executable records.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.