FirstPassProgramComplete
plain-language theorem explainer
The FirstPassProgramComplete predicate requires that the first-pass schedule for Option A is ready, the derived program list has length exactly 5 with no duplicates, and the mapped action, deliverable, and pipeline lists are likewise duplicate-free, while schedule membership holds precisely for combinations of high or immediate priority. Researchers assembling the empirical certificate for Option A in Recognition Science cite this gate to confirm metadata integrity before full certification. The definition is formed by direct conjunction of the
Claim. Let $S$ be the first-pass schedule. The program is complete when every $c$ in $S$ is empirically ready, the list obtained by mapping $S$ to program specifications has length 5 and no duplicates, the lists obtained by mapping $S$ to analysis actions, deliverables, and pipeline specifications each have no duplicates, and $c$ belongs to $S$ if and only if its empirical priority is high or immediate.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A. Earlier modules establish the queue, schedule, actions, deliverables, pipelines, and readiness separately; this file assembles them at the metadata layer. FirstPassReady asserts that every combination in the first-pass schedule satisfies empirical readiness. The first-pass program is the list of ProgramSpec values produced by applying programSpec to each entry of the schedule. Parallel mappings produce the action list via analysisAction, the deliverable list via deliverableFor, and the pipeline list via pipelineSpec. The predicate isHighOrImmediate holds when empiricalPriority equals immediate or high.
proof idea
The declaration is a direct definition that conjoins FirstPassReady with the length and Nodup properties of the four mapped lists plus the schedule-membership equivalence expressed via isHighOrImmediate. It draws the component definitions from the upstream modules on actions, deliverables, pipelines, program, queue, readiness, and schedule without additional derivation steps.
why it matters
This definition supplies the completeness field inside the EmpiricalProgramCert structure, which packages injectivity of programSpec, length 5, absence of duplicates, readiness, and completeness into one certificate. It thereby closes the assembly of the Option A empirical program after the separate proofs of its constituent pieces. In the Recognition Science framework the gate supports the empirical-validation step that follows the forcing chain (T0-T8) by confirming metadata integrity of the first-pass program before higher-level certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.