firstPassProgramComplete
The theorem certifies that the first-pass empirical program for Option A satisfies the completion gate: readiness holds, the program has length exactly 5, the program and its actions, deliverables, and pipelines are all duplicate-free, and the schedule contains precisely the high-or-immediate combinations. Researchers assembling empirical validation structures in the Recognition framework cite it to confirm the initial program is collision-free at the metadata layer. The proof is a direct term construction that supplies the seven conjuncts from
claimThe first-pass empirical program is complete when readiness holds, the program list has length exactly 5, the program is duplicate-free, the actions list is duplicate-free, the deliverables list is duplicate-free, the pipelines list is duplicate-free, and every combination belongs to the schedule if and only if it is high or immediate.
background
The module establishes a single certificate for the first-pass empirical program attached to Option A. Separate modules prove the queue, schedule, actions, deliverables, pipelines, and readiness; this file assembles them into one completion gate that is collision-free at the metadata layer. FirstPassProgramComplete is the proposition FirstPassReady ∧ firstPassProgram.length = 5 ∧ firstPassProgram.Nodup ∧ firstPassActions.Nodup ∧ firstPassDeliverables.Nodup ∧ firstPassPipelines.Nodup ∧ (∀ c : CombinationID, c ∈ firstPassSchedule ↔ isHighOrImmediate c). Upstream lemmas include firstPassProgram_length (length equals 5 by unfolding the map over the schedule), firstPassProgram_nodup (Nodup follows from mapping with the injective programSpec), and the corresponding nodup results for actions, deliverables, and pipelines obtained by rewriting to their defining equations and deciding or using List.Nodup.map.
proof idea
The proof is a term-mode exact construction of the required seven-tuple. It supplies firstPassReady for the readiness conjunct, firstPassProgram_length for the length conjunct, firstPassProgram_nodup for the program nodup conjunct, firstPassActions_nodup for the actions nodup conjunct, firstPassDeliverables_nodup for the deliverables nodup conjunct, firstPassPipelines_nodup for the pipelines nodup conjunct, and firstPassSchedule_mem_iff_high_or_immediate for the schedule-membership conjunct.
why it matters in Recognition Science
This declaration closes the assembly step for the first-pass empirical program in the Option A track. It is referenced directly by the definition empiricalProgramCert, which packages program injectivity, length, nodup, readiness, and completeness into a single certificate object. In the Recognition framework it supplies the metadata-level verification that the initial program is complete and collision-free before any higher-pass or semantic analysis proceeds.
scope and limits
- Does not establish semantic correctness or empirical validity of the scheduled tests.
- Does not address programs beyond the first pass.
- Does not cover runtime execution or actual measurement outcomes.
- Does not prove uniqueness properties beyond the listed noduplication conditions.
formal statement (Lean)
104theorem firstPassProgramComplete : FirstPassProgramComplete := by
proof body
Term-mode proof.
105 exact ⟨firstPassReady, firstPassProgram_length, firstPassProgram_nodup,
106 firstPassActions_nodup, firstPassDeliverables_nodup,
107 firstPassPipelines_nodup, firstPassSchedule_mem_iff_high_or_immediate⟩
108