c8_pipeline_deliverable
plain-language theorem explainer
The declaration confirms that the pipeline specification for the C8 Miller-Span combination yields the memory-collapse notebook as its deliverable. Researchers validating empirical outputs in the Option A framework would cite this equality to fix the artifact type for that case. The proof is an immediate reflexivity reduction against the definition of pipelineSpec.
Claim. The deliverable field of the pipeline record for the C8 Miller-Span combination equals the memory-collapse notebook.
background
The module assembles a single PipelineSpec record for each of the nine C1-C9 combinations. Each record bundles a protocol, an empirical priority, an analysis action, and a deliverable. The upstream definition pipelineSpec builds the complete record by selecting the appropriate component for the supplied combination identifier.
proof idea
The proof is a one-line reflexivity that matches the deliverable field directly from the definition of pipelineSpec applied to the C8 case.
why it matters
This equality supplies the deliverable slot required by the downstream empiricalPipelineCert, which aggregates injectivity, scheduling, and coverage properties across all pipelines. It completes the concrete mapping for the C8 Miller-Span entry inside the unified Option A empirical pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.