The complexity of complete irreducible autocatalytic families: output-polynomial enumeration of irreducible RAFs if and only if P = NP

An irreducible reflexively autocatalytic and food-generated set (irreducible RAF, or irrRAF) is an inclusion-minimal nonempty RAF of a finite catalytic reaction system. Detecting whether a system contains a RAF is polynomial, and Steel, Hordijk and Smith (J. Theor. Biol., 2013) gave a deletion-based criterion for certifying that a supplied list of irreducible RAFs is complete, whose cost grows exponentially in the list length. We settle the complexity of listing the complete family. For finite catalytic reaction systems with an explicit incidence encoding, a fixed deterministic multitape Turing machine that writes every irreducible RAF exactly once in time polynomial in the input length plus the output length exists if and only if $\mathsf P=\mathsf{NP}$. The lower bound is a polynomial-size SAT source whose entire RAF family has a prescribed normal form: a mandatory catalytic cycle forces all auxiliary reactions into every RAF, and a reset reaction cannot enable itself, so the irreducible RAFs are exactly $n$ conflict pairs together with the satisfying assignments of the formula. Unsatisfiable formulas therefore have a known polynomial-size complete family, and an output-sensitive time bound becomes a polynomial deadline that decides satisfiability. The converse builds, under $\mathsf P=\mathsf{NP}$, a uniform enumerator from a polynomial-size supported-trace SAT encoding of the query “is there a RAF avoiding every known output?” and a filtered deletion minimizer. The same source gives an exact count identity $|\mathcal I(Q_\varphi)|=n+\#\textup{\textsc{Sat}}(\varphi)$, coNP-completeness of exact certification, $\#\mathsf P$-hardness of counting, and an equivalence between polynomial-delay streaming enumeration and $\mathsf P=\mathsf{NP}$. The classification is machine-checked in Lean 4 for concrete multitape machines, including original-input initialization, arbitrary finite identifiers, and a count-prefixed fixed-width output, with no hypotheses beyond the standard axioms.