firstPassProgram_actions_nodup
The theorem proves the list of first-pass actions in the Option A empirical program has no duplicates. Researchers assembling the empirical program certificate cite it to confirm collision-free metadata. The proof is a one-line wrapper that invokes the upstream no-duplicates result for the mapped action list.
claimThe list of first-pass analysis actions obtained by mapping over the first-pass schedule is duplicate-free.
background
The Option A empirical program module assembles a certificate from separately proved pieces: queue, schedule, actions, deliverables, pipelines, and readiness. First-pass actions are the image of the first-pass schedule under the analysis action constructor. The upstream theorem in the action plan module shows this image list satisfies the no-duplicates property by rewriting to an equality and deciding it directly.
proof idea
The proof is a one-line wrapper that applies the upstream theorem firstPassActions_nodup from the action plan module.
why it matters in Recognition Science
This result supplies one of the no-duplicates fields inside the empiricalProgramCert definition, which bundles injectivity, length, readiness, and completeness for the first-pass program. It closes the collision-free metadata requirement stated in the module documentation. In the Recognition Science setting it supports a well-defined first-pass schedule without action collisions, consistent with the need for unique elements in the forcing chain construction.
scope and limits
- Does not prove no-duplicates for the full program list or other components.
- Does not address semantic correctness or execution behavior of the actions.
- Does not establish properties of the schedule or deliverables themselves.
formal statement (Lean)
81theorem firstPassProgram_actions_nodup :
82 firstPassActions.Nodup :=
proof body
One-line wrapper that applies firstPassActions_nodup.
83 firstPassActions_nodup
84