c8_pipeline_action
plain-language theorem explainer
The declaration asserts that the pipeline specification for the Miller-Span combination C8 sets its analysis action to fitDiscreteCollapse. Researchers validating empirical pipelines in Recognition Science cite this to confirm the fixed action mapping for that case. The proof proceeds by direct reflexivity on the pipeline specification definition.
Claim. For the Miller-Span combination identifier, the pipeline specification satisfies action = fitDiscreteCollapse.
background
The module supplies a unified empirical pipeline record for combinations C1-C9. Each record bundles protocol, priority, analysis action, and deliverable. The upstream definition pipelineSpec constructs the record for any combination identifier by delegating to separate specifications for protocol, priority, action, and deliverable.
proof idea
The proof is a one-line wrapper applying reflexivity to the definition of pipelineSpec at the C8 Miller-Span case.
why it matters
This result supplies the concrete action assignment used by empiricalPipelineCert, which aggregates injectivity, equivalence, and scheduling facts across all pipelines. It fills a slot in the Option A empirical pipeline setup for the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.