programSpec
plain-language theorem explainer
The definition assembles a complete program row for any given combination identifier by populating its protocol, priority, analysis action, deliverable, pipeline, and readiness fields from dedicated upstream specifications. Researchers validating the Option A empirical program would cite this constructor when forming the ordered first-pass list. Construction occurs through direct record initialization that delegates each component without further computation.
Claim. For a combination identifier $c$, the assigned program row is the structure whose combination field equals $c$, whose protocol equals the protocol specification of $c$, whose priority equals the empirical priority of $c$, whose action equals the analysis action of $c$, whose deliverable equals the deliverable assigned to $c$, whose pipeline equals the pipeline specification of $c$, and whose readiness equals the all-ready status of $c$.
background
ProgramSpec is the structure for one executable row in the Option A first-pass empirical program; it carries the combination identifier together with its protocol, priority, analysis action, deliverable, pipeline, and readiness status. The module supplies a single certificate for the assembled first-pass empirical program attached to Option A after separate modules have established the queue, schedule, actions, deliverables, pipelines, and readiness pieces. Upstream results include the action map that sends c3OncologyTensor to fitFactorModel and c8MillerSpan to fitDiscreteCollapse, the deliverable map that pairs the same identifiers with oncologyFactorModelNotebook and memoryCollapseNotebook, the pipeline constructor that re-uses those components, the protocol constructor, and the priority map that marks c3OncologyTensor and c8MillerSpan as immediate.
proof idea
The definition is a direct record literal that sets the combination field to the input and fills the remaining six fields by applying protocolSpec, empiricalPriority, analysisAction, deliverableFor, pipelineSpec, and empiricallyReady_all to that same input.
why it matters
The constructor is invoked by firstPassProgram to produce the ordered list of five rows and by the injectivity theorem that shows distinct combinations yield distinct rows. It also supplies the equalities used in scheduled_program_pipeline and scheduled_program_ready. These facts feed EmpiricalProgramCert, which certifies that the first-pass program has length five, contains no duplicates, and satisfies the readiness and completeness conditions required for the metadata-layer verification that the Option A empirical program is collision-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.