programSpec_injective
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.