pipelineSpec
plain-language theorem explainer
pipelineSpec constructs the complete empirical pipeline record for each implemented Option A combination by assigning its protocol, priority, analysis action, and deliverable fields. Researchers checking concrete C1-C9 cases cite the definition when verifying that every combination carries a full executable pipeline. The definition is a direct record constructor that delegates each field to a dedicated upstream mapping from CombinationID.
Claim. For each combination identifier $c$, the pipeline specification is the record whose protocol field equals the protocol specification of $c$, whose priority equals the empirical priority of $c$, whose action equals the analysis action of $c$, and whose deliverable equals the deliverable assigned to $c$.
background
PipelineSpec is the structure holding the four components of an empirical pipeline: ProtocolSpec, Priority, AnalysisAction, and Deliverable. The module defines a unified record for C1-C9 combinations with zero sorry or axiom. Upstream, CombinationID enumerates the implemented cases (c1CognitiveTensor through c5AttentionTensor and beyond), while protocolSpec maps $c$ to its dataset, observable, and failure mode; empiricalPriority, analysisAction, and deliverableFor each supply the remaining fields.
proof idea
The definition is a direct record constructor. It applies the PipelineSpec constructor and populates each field by calling the corresponding component function (protocolSpec, empiricalPriority, analysisAction, deliverableFor) on the input combination identifier.
why it matters
This definition supplies the concrete pipeline for every Option A combination and is used by the family of rfl theorems that verify the action, deliverable, and priority for specific cases such as c3OncologyTensor and c8MillerSpan. It completes the empirical pipeline construction step in the Option A falsifier registry, allowing downstream certification of the full pipeline via EmpiricalPipelineCert. No open questions attach to the construction itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.