HasPipeline
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not enumerate the internal fields or content of any pipeline record.
- Does not prove totality or injectivity of the pipelineSpec function.
- Does not apply to combinations outside the listed C1-C9 set.
- Does not reference J-cost, defect distance, or the phi-ladder.
Lean usage
example (c : CombinationID) : HasPipeline c := ⟨pipelineSpec c, rfl⟩formal statement (Lean)
54def HasPipeline (c : CombinationID) : Prop :=
proof body
Definition body.
55 ∃ p : PipelineSpec, pipelineSpec c = p
56