firstPassProgram_length
The first-pass empirical program has length exactly five. Researchers assembling the Option A empirical certificate cite this result to confirm the program size matches its underlying schedule. The proof reduces directly by unfolding the map definition and applying the schedule length theorem with the length-of-map identity.
claimThe first-pass empirical program, obtained by mapping the program specification over the first-pass schedule, has length five.
background
The Option A empirical program module supplies a single certificate confirming that the assembled first-pass program is complete and collision-free at the metadata layer. The program itself is constructed by applying the programSpec map to the first-pass schedule. An upstream theorem already shows that the schedule contains exactly five entries.
proof idea
The proof unfolds the definition of the first-pass program as the image of the schedule under the programSpec map. It then rewrites via the standard length-of-map lemma and substitutes the known result that the schedule has length five.
why it matters in Recognition Science
This length assertion is required by the empiricalProgramCert definition and by the firstPassProgramComplete theorem. It supplies one metadata property needed to certify the Option A program as ready. The result sits in the foundation layer that precedes any connection to the Recognition Science forcing chain or constants.
scope and limits
- Does not specify the content of any individual program step.
- Does not prove absence of duplicates or injectivity.
- Does not address readiness or pipeline properties.
- Does not connect to physical derivations or constants.
formal 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