hasPipeline_all
plain-language theorem explainer
Every implemented Option A combination possesses a complete empirical pipeline record. Researchers certifying empirical readiness for the Recognition Science protocols cite this result when assembling the C1-C5 validation package. The proof is a direct one-line construction that supplies the pipeline record and closes by reflexivity.
Claim. For every combination identifier $c$, there exists a pipeline specification $p$ such that the pipeline record assigned to $c$ equals $p$.
background
The module assembles a unified empirical pipeline for Option A that links protocol, priority, analysis action, and deliverable across the implemented combinations. HasPipeline holds for a combination precisely when a PipelineSpec record exists for it. The pipelineSpec function builds each record by pulling the protocol specification, empirical priority, analysis action, and deliverable for the given combination. CombinationID enumerates the five implemented cases (cognitive tensor, planet strata, oncology tensor, quantum molecular depth, attention tensor), with C10 noted only as commentary.
proof idea
This is a one-line wrapper proof. It witnesses the existential quantifier in the definition of HasPipeline by supplying the pipeline record returned by pipelineSpec applied to the input combination and discharges the equality with reflexivity.
why it matters
The result is collected inside the empiricalPipelineCert definition that aggregates injectivity, equivalence, and completeness facts. It is invoked directly by the scheduled_has_pipeline theorem for first-pass schedules and by empiricallyReady_all to establish overall readiness. It supplies the missing completeness clause for the unified empirical pipeline record in the Option A framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.