scheduled_program_pipeline
plain-language theorem explainer
The theorem states that for any combination identifier in the first-pass schedule, the pipeline field inside its program specification equals the dedicated pipeline specification. Researchers assembling the Option A empirical certificate would cite it to confirm that program rows and pipeline records stay synchronized at the metadata level. The proof reduces immediately to reflexivity because the two records are built from identical component functions.
Claim. For any combination identifier $c$ belonging to the first-pass schedule, the pipeline field of the program specification for $c$ equals the pipeline specification for $c$.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A, after separate modules have established the queue, schedule, actions, deliverables, pipelines, and readiness. Upstream, pipelineSpec constructs a PipelineSpec record for each CombinationID by setting protocol, priority, action, and deliverable. programSpec constructs the corresponding ProgramSpec row that includes the combination identifier together with the same protocol, priority, action, and deliverable fields plus an explicit pipeline component. firstPassSchedule is the concrete list of initial test combinations, and CombinationID is the inductive type of implemented Option A combinations.
proof idea
The proof is a one-line wrapper that applies reflexivity. The pipeline field of programSpec c is defined to be exactly pipelineSpec c, so the required equality holds definitionally.
why it matters
The result is used inside the construction of empiricalProgramCert, the top-level certificate that records program injectivity, length, absence of duplicates, readiness, and completeness. It closes the metadata-consistency check between program rows and pipeline records for every scheduled combination, completing one layer of the single certificate for the first-pass empirical program of Option A.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.