HasPipeline
plain-language theorem explainer
Definition HasPipeline asserts that an Option A combination identifier possesses a complete empirical pipeline precisely when the pipelineSpec function returns a matching record. Researchers building empirical certification layers for C1-C9 combinations cite this predicate to confirm operational completeness. The definition expands directly to an existential statement over the pipeline assignment function.
Claim. For a combination identifier $c$, HasPipeline$(c)$ holds if and only if there exists a pipeline specification $p$ such that the pipeline record assigned to $c$ equals $p$.
background
The module defines a unified empirical pipeline record for the Option A combinations C1-C9. PipelineSpec is the structure that bundles four components: a protocol specification, an empirical priority, an analysis action, and a deliverable. The function pipelineSpec maps each CombinationID to its PipelineSpec by composing the respective specification functions for protocol, priority, action, and deliverable. CombinationID is the inductive type enumerating the implemented combinations, with C10 left as commentary.
proof idea
This is a definition that directly encodes the existence condition via the pipelineSpec assignment. It functions as a one-line wrapper introducing the HasPipeline predicate with no lemmas or tactics applied.
why it matters
HasPipeline serves as a building block for the EmpiricalPipelineCert structure, which asserts injectivity of pipelineSpec together with the universal claim that every CombinationID has a pipeline. It is invoked directly by hasPipeline_all, scheduled_has_pipeline, and the EmpiricallyReady definition. The predicate operationalizes the requirement for complete empirical records in the Option A validation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.