firstPassProgram_nodup
plain-language theorem explainer
The theorem establishes that the first-pass empirical program list, formed by mapping programSpec over the first-pass schedule, contains no duplicate ProgramSpec entries. Researchers building the Option A empirical certification cite it to guarantee metadata uniqueness before assembling the full certificate. The proof is a one-line term that unfolds the program definition and applies List.Nodup.map with the injectivity of programSpec and the nodup property of the schedule.
Claim. The list obtained by applying the program specification function to the first-pass schedule is duplicate-free: if $P = S.map(f)$ where $f$ is injective and $S$ is duplicate-free, then $P$ is duplicate-free.
background
The module provides a single certificate for the first-pass empirical program attached to Option A. It assembles prior results on the queue, schedule, actions, deliverables, pipelines, and readiness to establish that the assembled program is complete and collision-free at the metadata layer. Local conventions treat firstPassProgram as the concrete list firstPassSchedule.map programSpec, with ProgramSpec carrying combination metadata.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of firstPassProgram to expose the mapped list, then invokes List.Nodup.map. The required hypotheses are supplied directly by the sibling theorem programSpec_injective (which shows Function.Injective programSpec via congrArg on combinations) and the upstream theorem firstPassSchedule_nodup (which is decided by computation).
why it matters
This result is referenced by empiricalProgramCert to populate the first_pass_nodup field and by firstPassProgramComplete to bundle uniqueness with readiness and length. It closes the metadata-collision-free requirement for the Option A certificate in the foundation layer, ensuring the schedule-derived program list satisfies the no-duplicate condition needed for downstream empirical certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.