EmpiricalProgramCert
plain-language theorem explainer
EmpiricalProgramCert packages injectivity of programSpec together with length-five nodup on firstPassProgram, FirstPassReady, FirstPassProgramComplete, schedule-to-priority equivalence, and nodup on the action-deliverable-pipeline lists. Researchers certifying the Option A empirical pipeline would cite the resulting record when they need a single metadata-complete object. The declaration is a structure definition that simply aggregates the component lemmas already established in sibling modules.
Claim. The record type whose inhabitants witness that programSpec is injective, that firstPassProgram has length 5 and contains no duplicates, that FirstPassReady holds, that FirstPassProgramComplete holds, that every scheduled combination satisfies the empirical readiness and pipeline equations, that firstPassActions, firstPassDeliverables and firstPassPipelines are duplicate-free, and that membership in firstPassSchedule is exactly the set of high-or-immediate CombinationIDs.
background
The module assembles a single certificate for the first-pass empirical program of Option A. FirstPassProgramComplete is the proposition that FirstPassReady holds, firstPassProgram has length 5 and is nodup, and the three output lists (actions, deliverables, pipelines) are likewise nodup, together with the exact schedule equivalence to isHighOrImmediate. firstPassProgram is obtained by mapping programSpec over firstPassSchedule; the three output lists are obtained analogously by mapping the respective action, deliverable and pipeline constructors.
proof idea
Structure definition that collects the listed properties into a single record type; no proof term is required.
why it matters
The structure is instantiated by the downstream definition empiricalProgramCert, which supplies the single certificate object used by any later verification that the Option A first-pass program is metadata-complete. It closes the assembly step described in the module doc-comment, confirming that the queue, schedule, actions, deliverables and pipelines fit together without collision at the specification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.