firstPassProgram_deliverables_nodup
plain-language theorem explainer
The theorem establishes that the deliverables list derived from the first-pass schedule contains no duplicate entries. Researchers certifying the Option A empirical program in Recognition Science cite it to confirm metadata collision-freeness. The proof is a direct one-line wrapper that invokes the upstream nodup result on the deliverables list.
Claim. The list of deliverables generated by mapping the deliverable construction over the first-pass schedule contains no duplicate entries.
background
The Option A Empirical Program module supplies a single certificate for the assembled first-pass empirical program. It combines previously established components for the schedule, actions, deliverables, and pipelines into a collision-free metadata structure. The deliverables list is defined by applying the deliverableFor mapping to the first-pass schedule. An upstream theorem proves this list satisfies the nodup property via rewriting to an equality followed by a decision procedure.
proof idea
The proof is a one-line wrapper that directly applies the theorem establishing the nodup property for the first-pass deliverables list.
why it matters
This result feeds the empirical program certificate by confirming the deliverables component is duplicate-free, thereby supporting the overall claim that the first-pass program is complete and collision-free at the metadata layer. It fills the deliverables-specific integrity step within the Option A certificate construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.