firstPassProgramComplete
plain-language theorem explainer
The theorem establishes that the first-pass empirical program meets its completion gate: readiness holds, the program list has length exactly 5 and is duplicate-free, and the same holds for its derived actions, deliverables, and pipelines lists, with schedule membership equivalent to high-or-immediate combinations. Researchers certifying Option A empirical programs cite this result to confirm metadata-layer collision freedom. The proof is a direct term-mode constructor application that assembles the six component lemmas.
Claim. The first-pass program is complete when it is ready, has length exactly 5, the program and its action, deliverable, and pipeline lists are duplicate-free, and a combination belongs to the schedule if and only if it is high or immediate priority.
background
FirstPassProgramComplete is the conjunction of FirstPassReady (every scheduled row is ready), firstPassProgram.length = 5, firstPassProgram.Nodup, firstPassActions.Nodup, firstPassDeliverables.Nodup, firstPassPipelines.Nodup, and the schedule equivalence (∀ c, c ∈ firstPassSchedule ↔ isHighOrImmediate c). The module supplies a single certificate for the first-pass empirical program attached to Option A; earlier modules prove the pieces separately (queue, schedule, actions, deliverables, pipelines, readiness) and this file assembles them to show the program is complete and collision-free at the metadata layer.
proof idea
The proof is a term-mode exact application of the conjunction constructor, directly supplying the six component theorems firstPassReady, firstPassProgram_length, firstPassProgram_nodup, firstPassActions_nodup, firstPassDeliverables_nodup, firstPassPipelines_nodup, and firstPassSchedule_mem_iff_high_or_immediate.
why it matters
This theorem supplies the completeness property bundled into empiricalProgramCert, which collects program injectivity, length, nodup, readiness, and completeness for the Option A empirical track. It closes the first-pass program verification step, ensuring the metadata layer has no collisions before higher-level empirical claims. No open questions or scaffolding are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.