firstPassProgram_length
plain-language theorem explainer
The theorem asserts that the first-pass empirical program has cardinality exactly five. Researchers certifying the Option A empirical program cite it when assembling the metadata completeness check. The proof reduces the claim by unfolding the program definition as the image of the schedule under the specification map and invoking the already-proved schedule length.
Claim. Let $P$ be the list obtained by applying the program-specification map to every element of the first-pass schedule. Then $|P| = 5$.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A. The program is assembled from a queue, schedule, actions, deliverables, pipelines, and readiness checks already established in sibling modules. The definition firstPassProgram is the image of firstPassSchedule under the map programSpec. The upstream theorem firstPassSchedule_length states that the underlying schedule has length five and is proved by decide.
proof idea
The term proof unfolds firstPassProgram to expose the mapped schedule, then rewrites the length using the standard List.length_map lemma together with the upstream result firstPassSchedule_length.
why it matters
The length equality is required by the definition empiricalProgramCert and by the theorem firstPassProgramComplete. It supplies one of the metadata invariants needed for the Option A certificate in the foundation layer, confirming that the assembled program matches the five-step schedule size fixed by the recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.