EmpiricalPipelineCert
plain-language theorem explainer
EmpiricalPipelineCert is a record that certifies the pipelineSpec map from CombinationID is injective with the equality-iff property, that HasPipeline holds for every CombinationID and for all entries in firstPassSchedule, that firstPassPipelines has length 5 and contains no duplicates, and that the c3OncologyTensor and c8MillerSpan records carry immediate priority together with their specific actions and deliverables. Researchers implementing Option A empirical validation cite the certificate to confirm the complete pipeline setup. The entryis
Claim. Let $pi$ map each CombinationID to its PipelineSpec. The structure asserts that $pi$ is injective, $pi(a)=pi(b)leftrightarrow a=b$ for all CombinationIDs $a,b$, every CombinationID $c$ satisfies HasPipeline $c$ (i.e., $exists p$ with $pi(c)=p$), every $c$ in firstPassSchedule satisfies HasPipeline $c$, the list firstPassPipelines has length 5 and is duplicate-free, and the records for c3OncologyTensor and c8MillerSpan have priority immediate, action fitFactorModel or fitDiscreteCollapse, and the matching deliverables oncologyFactorModelNotebook and memoryCollapseNotebook.
background
The module supplies a unified empirical pipeline record for Option A combinations C1-C9 that links protocol, priority, analysis action, and deliverable. HasPipeline $c$ is the proposition that there exists a PipelineSpec $p$ such that pipelineSpec $c = p$. firstPassPipelines is defined as the list obtained by mapping pipelineSpec over firstPassSchedule. Upstream theorems establish by reflexivity that analysisAction .c3OncologyTensor equals fitFactorModel, analysisAction .c8MillerSpan equals fitDiscreteCollapse, deliverableFor .c3OncologyTensor equals oncologyFactorModelNotebook, and deliverableFor .c8MillerSpan equals memoryCollapseNotebook.
proof idea
The declaration is a structure definition that directly packages the listed properties. The individual fields are supplied by sibling results: pipelineSpec_injective and pipelineSpec_eq_iff for the injectivity and equivalence statements, hasPipeline_all and scheduled_has_pipeline for coverage, firstPassPipelines_length and firstPassPipelines_nodup for the list properties, and the rfl theorems c3_action, c3_deliverable, c8_action, c8_deliverable for the concrete c3 and c8 values.
why it matters
The structure is instantiated by the downstream empiricalPipelineCert definition to furnish the complete certificate for the Option A empirical pipeline. It closes the foundation setup that ties every implemented combination to a concrete priority, action, and deliverable, supporting empirical validation steps without engaging the core forcing chain or Recognition Composition Law. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.