c3_pipeline_priority
plain-language theorem explainer
The declaration fixes the priority of the C3 oncology tensor pipeline specification to immediate. Researchers certifying Option A empirical pipelines for oncology tensor analysis would reference this when confirming scheduling order. The proof reduces by direct reflexivity to the pipelineSpec definition.
Claim. Let $c$ be the combination identifier for the C3 oncology tensor. The priority component of the pipeline specification for $c$ equals the immediate level: priority(pipelineSpec($c$)) = immediate.
background
The module supplies a unified empirical pipeline record for combinations C1-C9 that links protocol, priority, analysis action, and deliverable. The upstream definition pipelineSpec builds a PipelineSpec record for any CombinationID by assigning protocol := protocolSpec c, priority := empiricalPriority c, action := analysisAction c, and deliverable := deliverableFor c. This supplies the concrete mapping used throughout the Option A empirical deliverables.
proof idea
The proof is a one-line wrapper that applies reflexivity, reducing the equality directly to the definition of pipelineSpec at the .c3OncologyTensor case.
why it matters
This assignment feeds the empiricalPipelineCert definition, which collects injectivity, equivalence, and scheduling properties for all pipelines. It supplies the concrete priority datum for the C3 oncology tensor combination inside the foundation layer of the Recognition Science empirical pipeline structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.