firstPassProgram_actions_nodup
plain-language theorem explainer
The theorem states that the list of analysis actions for the first-pass empirical program contains no duplicate entries. Researchers certifying the Option A empirical program would cite this when confirming metadata integrity of the action sequence. The proof is a direct one-line wrapper invoking the corresponding no-duplicates result on the underlying action list.
Claim. Let $A$ be the list of actions obtained by mapping the analysis action constructor over the first-pass schedule. Then $A$ contains no duplicate entries.
background
The Option A Empirical Program module assembles a single certificate showing the first-pass program is complete and collision-free at the metadata layer, building on separate proofs for queue, schedule, actions, deliverables, pipelines, and readiness. The definition firstPassActions produces the list by applying the analysisAction map to firstPassSchedule. The upstream theorem firstPassActions_nodup establishes the no-duplicates property for this list via rewriting to an equality followed by a decision procedure.
proof idea
This is a one-line wrapper that applies the theorem firstPassActions_nodup.
why it matters
This result feeds the empiricalProgramCert definition, which collects program injectivity, first-pass length, nodup, readiness, and completeness. It supports the module claim that the assembled first-pass program is collision-free at the metadata layer. The property ensures distinct action sequences within the Recognition Science empirical program structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.