FirstPassProgramComplete
plain-language theorem explainer
FirstPassProgramComplete packages the gate conditions for the initial empirical program in Option A: schedule readiness, length exactly five, duplicate-free lists for program/actions/deliverables/pipelines, and schedule membership restricted to high or immediate priorities. Certification work on the Option A empirical program cites this gate when forming the assembled certificate. The declaration is a direct conjunction of the listed predicates with no additional lemmas.
Claim. FirstPassProgramComplete holds precisely when FirstPassReady is true (every scheduled CombinationID is EmpiricallyReady), the program list obtained by mapping programSpec over the schedule has length 5 and contains no duplicates, the derived action list, deliverable list, and pipeline list each contain no duplicates, and the schedule contains exactly those CombinationID satisfying isHighOrImmediate.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A. Upstream modules establish the schedule, the mapping to ProgramSpec, AnalysisAction, Deliverable, and PipelineSpec, and the readiness predicate separately. FirstPassReady is the predicate that every c in firstPassSchedule satisfies EmpiricallyReady c. isHighOrImmediate holds when empiricalPriority c equals immediate or high. firstPassProgram, firstPassActions, firstPassDeliverables, and firstPassPipelines are each obtained by mapping the corresponding spec function over the same schedule.
proof idea
Definition that directly forms the conjunction of FirstPassReady, the length and Nodup properties of the four mapped lists, and the schedule membership equivalence with isHighOrImmediate. No lemmas are invoked; the body simply assembles the component predicates already established in sibling definitions.
why it matters
Supplies the first_pass_complete field required by the EmpiricalProgramCert structure and is discharged by the sibling theorem firstPassProgramComplete. It completes the metadata-layer verification step for the first-pass program before the full Option A certificate is assembled. The definition supports the Recognition Science empirical program construction by ensuring the initial schedule produces collision-free outputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.