Certifying complete families of irreducible autocatalytic sets is co-W[P]-complete

An irreducible reflexively autocatalytic and food-generated set (irrRAF) is an inclusion-minimal self-sustaining reaction subsystem of a catalytic reaction system. Steel, Hordijk and Smith (J. Theor. Biol., 2013) gave a criterion for deciding whether a supplied list of $k$ irrRAFs is complete, that is, whether every irrRAF of the system appears on the list. Their procedure runs in polynomial time for each fixed $k$, with an exponent that grows with $k$, and they asked whether the problem is fixed-parameter tractable in $k$. We show that it is not, unless $\mathsf{FPT}=\mathsf{W[P]}$: exact completeness certification is $\mathsf{co\text{-}W[P]}$-complete when parameterized by the number of listed irrRAFs, and $\mathsf{coNP}$-complete without parameterization. Hardness already holds for systems with a single food molecule whose supplied family consists of $k$ pairwise reaction-disjoint simple catalytic cycles. The reduction starts from MINIMUM AXIOM SET. Each listed cycle is a guard whose unique omitted reaction selects one axiom; decoder reactions read the omission, a literal implication network derives the remaining statements, and a single closing reaction supplies the common catalyst that makes everything else self-sustaining. Every unlisted irrRAF is shown to determine a generating axiom set, including when the implication system is cyclic. Membership follows from the deletion criterion together with the bounded-nondeterminism characterization of $\mathsf{W[P]}$. A second, Lean-verified reduction from $k$-CLIQUE shows that no algorithm runs in time $f(k)\,N^{o(k)}$ unless the Exponential Time Hypothesis fails, so the exponent of the known algorithm cannot be made sublinear in $k$; the problem is fixed-parameter tractable in $k$ plus the size of the largest listed irrRAF. Consequences for the problem of finding one more irrRAF and for bounded-delay enumeration are derived. The finite reductions, the validity of the supplied families, the exact parameter, the one-deletion irreducibility test and the deletion criterion are verified in the Lean 4 proof assistant with warnings promoted to errors; the complexity-class transfers are conventional proofs given in full.