Abstract

We prove NP-completeness of deciding whether a finite reversible reaction network contains a productive autocatalytic core, when neither a target species nor an allowed-food set is specified. The input is a binary encoding of the two literal nonnegative integer complex matrices, and each reaction identity carries a signed real flow. The proof first characterizes existence of a core by a nonsingular square restriction with literal two-sided participation. A weighted incidence construction then reduces prescribed two-path directed linkage to this unrestricted search: incidence saturation controls every possible selected support, and a boundary determinant distinguishes the desired pairing from the crossed pairing. An explicit constant-size switch construction reduces SAT to the required linkage instances. Polynomial certificates and a total polynomial-time binary transducer complete the classification. The terminal theorem, including actual machine-level membership and reduction bounds, is verified in Lean.