Exact common-activity compatibility of autocatalytic cores: finite cycle acceleration, monotone elimination, and fixed-parameter tractability in the longest path

Autocatalytic cores that are individually realizable under thermodynamically consistent mass action need not be realizable together, because every reaction touching a shared species sees the same activity. We study this compatibility problem for weighted two-reaction cores $X_u\rightleftharpoons X_v$, $X_v+F\rightleftharpoons 2X_u$ placed on the edges of an arbitrary finite oriented graph, with fixed positive rational kinetic factors and an independent rational activity box for every species: is there one activity vector at which both internal species of every core are strictly net produced? At a fixed margin the constraints are monotone two-variable implications whose feasible set has a least element, and we give two exact algorithms that compute it, decide strict compatibility, and return a rational witness. The first accelerates label-correcting propagation by least admissible fixed points of rooted cycle maps: every jump is forced on all feasible states, cycle–root tokens prove termination where plain iteration converges forever, and every value that arises has bounded symbolic ancestry, one box endpoint or one fixed cycle root transported along one simple path. Keeping the roots free during one-block quantifier elimination reduces every comparison to three free variables, the margin is handled as a positive infinitesimal by deciding each comparison for all sufficiently small margins, and the cost is $(J+1)\,n\,(h+2)^{O(h)}\operatorname{poly}(B)$ bit operations, where $n$ is the number of species, $B$ the input bit length, $h$ the number of edges of a longest undirected simple path, and $J$ the number of jumps; always $J\le(n+2)^{O(h)}$, and $J=O(n)\,(h+2)^{O(h)}$ on forests, windmills and every class with linearly many simple cycles. The second algorithm eliminates the species bottom-up along a depth-first forest. Because monotone two-variable implications are closed under exact elimination of a variable, with a next-admissible-value map recording the disconnected projections, all intermediate constraints stay two-variable, their envelopes have near-linearly many pieces by Davenport–Schinzel theory, and strict compatibility is decided in $f(h)\,n^2\operatorname{poly}(B)$ bit operations: the problem is fixed-parameter tractable in $h$, equivalently in the treedepth. Polynomial time in $n$ alone would require deciding the sign of an $n$-fold composition of rational quadratics at a rational point, already on a directed path. We also derive the least-inventory property of the returned state, an exact capacity scale with universal ceiling $(3-2\sqrt2)/8$, a reduction of interval-ratio robustness to the same algorithms with the sharp obstruction $r^+\ge2r^-$, an all-size certified example with tolerance radius $19/301$, and an extension to cores of any fixed order. The order-theoretic core, the forced-root and finite-progress lemmas, the vertex-elimination lemma, the source bridge, the quantitative corollaries and all example arithmetic are compiled in Lean 4 with Mathlib; the real-algebraic execution and the complexity analysis are conventional proofs and are marked as such.