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