c3_pipeline_deliverable
plain-language theorem explainer
The theorem fixes the deliverable for the C3 oncology tensor combination to the oncology factor model notebook inside the pipeline specification. Researchers tracing Option A empirical deliverables for oncology cases would cite this equality when assembling the full pipeline record. The proof reduces immediately by reflexivity once pipelineSpec is unfolded.
Claim. For the combination identifier $c = $ C3OncologyTensor, the deliverable component of the pipeline specification satisfies deliverable(pipelineSpec($c$)) = OncologyFactorModelNotebook.
background
The module assembles a unified empirical pipeline record for every C1-C9 combination. PipelineSpec packages four fields: protocol from protocolSpec, priority from empiricalPriority, action from analysisAction, and deliverable from deliverableFor. The upstream definition pipelineSpec simply assembles these four components for any given CombinationID.
proof idea
One-line wrapper that applies reflexivity to the definition of pipelineSpec and the deliverableFor clause for the C3 case.
why it matters
The result supplies the concrete deliverable entry required by empiricalPipelineCert. It completes the C3 row in the Option A table, ensuring the certificate can assert that every scheduled pipeline carries a well-defined output artifact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.