programSpec_injective
plain-language theorem explainer
The assignment from CombinationIDs to executable program rows is shown to be one-to-one. Workers certifying the Option A empirical program invoke it to guarantee distinct rows in the assembled first-pass list. The argument reduces equality of two rows to equality of their embedded CombinationIDs by direct projection.
Claim. The map sending each CombinationID $c$ to the ProgramSpec record with combination $c$, protocol given by protocolSpec $c$, priority given by empiricalPriority $c$, action given by analysisAction $c$, and deliverable given by deliverableFor $c$ is injective.
background
The module assembles a single certificate for the first-pass empirical program attached to Option A. ProgramSpec is the structure type for each row, containing a CombinationID, ProtocolSpec, Priority, AnalysisAction, and Deliverable. The function programSpec populates such a row for a given CombinationID by delegating to the four component specifications on that identifier.
proof idea
The term proof is a one-line wrapper. It introduces two CombinationIDs a and b together with an equality hypothesis h between their program rows, then recovers a = b by applying congrArg to the combination field of the ProgramSpec structure.
why it matters
It supplies the program_injective component of the EmpiricalProgramCert definition and is applied inside the nodup theorem for the first-pass program list via List.Nodup.map. The result closes the metadata uniqueness step required for the collision-free certificate described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.