firstPassActions_nodup
plain-language theorem explainer
The theorem shows that the list of first-pass empirical actions has no duplicates. Implementers of the Option A test schedule cite it to confirm the initial sequence is well-formed before running the full program. The proof is a one-line wrapper that rewrites the list via its defining equality and lets the decide tactic confirm uniqueness of the four actions.
Claim. Let $L$ be the list of initial analysis actions obtained by mapping the action constructor over the first-pass schedule. Then $L$ contains no duplicate entries, where $L$ expands explicitly to the sequence consisting of the fit-factor model, the discrete-collapse fit, plateau detection, and the regulatory-state count.
background
The module supplies concrete analysis action classes for the scheduled Option A empirical tests. The schedule fixes execution order while the file records the computation type required by each test. First-pass actions arise by applying the analysis action map to the first-pass schedule, and the equality theorem supplies the explicit four-element list.
proof idea
The proof rewrites the list using the equality theorem that equates first-pass actions to the concrete sequence, then invokes the decide tactic to verify that the four listed actions are pairwise distinct.
why it matters
The result is invoked directly in the empirical action plan certificate and in the completeness theorem for the first-pass program. It supplies a concrete verification step that the initial segment of the Option A schedule is free of redundant actions, closing a small implementation gap before the program proceeds to full deliverables and pipelines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.