firstPassProgram_length
The first-pass empirical program has length exactly 5. Researchers certifying Option A would cite this to fix the program scale at the metadata layer. The proof is a one-line term reduction that unfolds the map definition and rewrites via the schedule length theorem.
claimLet the first-pass empirical program be the list obtained by applying the program-specification map to each element of the first-pass schedule. Then its length equals 5.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A. The program is assembled by mapping the program-specification function over the first-pass schedule. An upstream theorem already shows that the schedule itself has length 5.
proof idea
The term proof unfolds the definition of the first-pass program (a direct map over the schedule) and rewrites the length using the list-length-of-map identity together with the schedule-length theorem.
why it matters in Recognition Science
The result is invoked inside the empirical-program certificate and inside the first-pass completeness theorem. It supplies the length datum required for the metadata-layer verification that the assembled program is collision-free.
scope and limits
- Does not establish semantic correctness of any program action.
- Does not address later passes or full execution traces.
- Does not prove injectivity or readiness properties.
Lean usage
exact firstPassProgram_lengthformal statement (Lean)
56theorem firstPassProgram_length :
57 firstPassProgram.length = 5 := by
proof body
Term-mode proof.
58 unfold firstPassProgram
59 rw [List.length_map, firstPassSchedule_length]
60