c3_pipeline_action
plain-language theorem explainer
The theorem states that the analysis action assigned to the C3 oncology tensor combination equals the fit factor model. Researchers verifying pipeline configurations in empirical tests of Recognition Science models would reference this equality when confirming deterministic actions for oncology-related cases. The proof reduces immediately to reflexivity on the definition of pipelineSpec.
Claim. For the combination identifier $C_3$ (oncology tensor), the action field of the pipeline specification equals the fit factor model.
background
The module supplies a unified empirical pipeline record for the nine Option A combinations C1-C9. Each record bundles a protocol, priority, analysis action, and deliverable. The function pipelineSpec maps every CombinationID to such a record by setting its action component to the value returned by analysisAction for that identifier.
proof idea
The proof is a one-line wrapper that applies reflexivity (rfl). This holds directly because pipelineSpec .c3OncologyTensor is constructed with action := analysisAction .c3OncologyTensor and the latter is defined to be .fitFactorModel.
why it matters
The result supplies the concrete action entry for C3 inside empiricalPipelineCert, which assembles injectivity, scheduling, and coverage properties across all pipelines. It completes the deterministic configuration table required by the Option A empirical pipeline framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.