firstPassProgram
plain-language theorem explainer
The first-pass empirical program is the ordered list of executable rows obtained by mapping the program row constructor over the predefined schedule of five combination identifiers. Researchers certifying the Option A empirical pipeline cite this as the concrete execution sequence for the oncology tensor, Miller span, attention tensor, regulatory ceiling, and planet strata tests. The definition is realized as a direct one-line list mapping.
Claim. The first-pass empirical program is the list obtained by applying the program row constructor to each identifier in the first-pass test order list, yielding the sequence of five rows each bundling a combination identifier with its protocol, priority, action, deliverable, and readiness flag.
background
ProgramSpec is the structure for one executable row in the Option A first-pass empirical program, holding the combination identifier, protocol specification, priority, analysis action, deliverable, pipeline specification, and empirical readiness predicate. The first-pass schedule is the ordered list of five CombinationIDs for the oncology tensor, Miller span, attention tensor, regulatory ceiling, and planet strata tests. This definition appears in the module that assembles a single certificate for the Option A first-pass empirical program, proving completeness and collision-freeness at the metadata layer from separately established queue, schedule, actions, deliverables, pipelines, and readiness components.
proof idea
The definition is a one-line wrapper that applies the list map operation to the first-pass schedule using the program row constructor.
why it matters
This definition supplies the concrete program list certified by the EmpiricalProgramCert structure and the FirstPassProgramComplete proposition. It assembles the schedule and program row pieces into the executable sequence whose length, noduplication, and readiness properties are verified in downstream theorems. In the Recognition framework it provides the first-pass test order for Option A, closing the metadata layer before empirical execution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.