programSpec_injective
The map sending each combination identifier to its executable program row is injective. Researchers assembling the Option A first-pass empirical program certificate cite this to guarantee that distinct inputs produce distinct rows in the schedule. The proof is a one-line term that applies congruence to the combination projection of the ProgramSpec structure.
claimLet $f$ be the map from combination identifiers to program specification rows that sets the combination field of the row directly to the input identifier. Then $f$ is injective: if $f(c_1) = f(c_2)$ then $c_1 = c_2$.
background
The Option A empirical program module assembles a single certificate for the first-pass empirical program from separately proved pieces (queue, schedule, actions, deliverables, pipelines, readiness). ProgramSpec is the structure type for one executable row; it contains fields for the combination identifier, protocol specification, priority, analysis action, and deliverable. The function programSpec constructs such a row for a given combination identifier by setting the combination field to the input and filling the remaining fields from auxiliary specifications.
proof idea
The proof is a term-mode one-liner. It introduces two combination identifiers a and b together with the hypothesis that their images under the map are equal, then applies congruence to the combination projection of the ProgramSpec structure to recover equality of the identifiers.
why it matters in Recognition Science
This result supplies the injectivity component required by the empiricalProgramCert definition that assembles the full first-pass certificate. It is invoked directly in the proof of firstPassProgram_nodup to transfer the no-duplicates property from the underlying schedule via the map. Within the Recognition Science formalization it closes the collision-free metadata layer for the Option A first-pass pipeline.
scope and limits
- Does not establish completeness or readiness of the program rows for execution.
- Does not address the internal content of protocol or action fields.
- Does not prove uniqueness properties for the full empirical program beyond the first-pass schedule.
- Does not cover runtime behavior or empirical validation of the assembled program.
Lean usage
unfold firstPassProgram; exact List.Nodup.map programSpec_injective firstPassSchedule_nodupformal statement (Lean)
48theorem programSpec_injective : Function.Injective programSpec := by
proof body
Term-mode proof.
49 intro a b h
50 exact congrArg ProgramSpec.combination h
51
52/-- First-pass empirical program in execution order. -/