c8_pipeline_priority
plain-language theorem explainer
The declaration establishes that the C8 Miller-Span combination receives immediate priority in its assigned empirical pipeline record. Analysts confirming scheduling details for Option A Miller-Span validations would cite this to lock in the priority level. The proof is a direct reflexivity reduction against the pipelineSpec definition.
Claim. The priority component of the pipeline specification for the Miller-Span combination equals immediate.
background
The module supplies a unified empirical pipeline record covering combinations C1-C9, each equipped with protocol, priority, analysis action, and deliverable. The upstream pipelineSpec definition constructs a PipelineSpec record for any CombinationID by delegating its priority field to empiricalPriority c. The local setting is the deterministic Option A empirical pipeline with zero axioms or sorrys.
proof idea
The proof is a one-line wrapper that applies reflexivity to match the equality against the priority value supplied by pipelineSpec for .c8MillerSpan.
why it matters
This assignment feeds the empiricalPipelineCert definition, which aggregates all priority and pipeline facts into a single certification record. It fills the C8 slot in the deterministic pipeline structure required by the Option A empirical deliverables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.