Exact common-activity compatibility for autocatalytic junction–path assemblies: boundary reduction, a rational decision algorithm, and operating certificates

Autocatalytic cores that are each realizable in isolation need not be realizable together: under thermodynamically consistent mass action, every reaction that involves a species sees the same activity of that species, and the stoichiometric powers of the activities constrain both the direction and the magnitude of every current. Kosc, Kuperberg, Rajon and Charlat (Proc. Natl. Acad. Sci. USA, 2025) proved that every isolated potential autocatalytic core admits a productive realization and exhibited two cores with no common one. We study a class of assemblies in which the number of species is unbounded and compatibility is nevertheless decided exactly. An assembly consists of weighted two-reaction cores $X_u\rightleftharpoons X_v$, $X_v+F\rightleftharpoons 2X_u$ with arbitrary positive kinetic factors, arranged in directed paths whose interiors are private and whose endpoints belong to a set of $k$ shared junction species, each species carrying a closed activity box. We prove that a common activity vector making every selected core strictly productive exists if and only if the junction activities alone satisfy, for each path, a strict inequality between two explicitly composed quadratic responses, together with the junction boxes. The interior of every path is eliminated without relaxing a single current law, and a one-parameter interpolation reconstructs it. For rational data this yields a complete decision procedure that also outputs a rational common state; its total bit cost and output length are at most $\mathcal{A}^{O(k+1)}$ with $\mathcal{A}=(n+M+k+2)(2^h+1)(B+h+1)$, where $n$ is the input size, $M$ the number of paths, $h$ their maximum length and $B$ the rational height of the data. The precision analysis, which combines a reciprocal root bound for a one-block quantifier-elimination output with Lipschitz control of the composed responses, replaces algebraic sample points by dyadic bisection and handles singleton junction boxes. We further give a linear-programming sufficient certificate that produces explicit compatible assemblies without any integer grading, a sharp fixed-state tolerance radius for independent relative factor uncertainty, an eight-corner certificate for joint activity, factor and food uncertainty, exact food-activity windows, and instantaneous loss budgets. The source-level equivalence, the path reconstruction, the merge across shared species, the rational certificate checker and every local certificate lemma are verified in Lean 4 against Mathlib with warnings promoted to errors and no admitted statements; the quantifier-elimination instantiation, the bit-size accounting and the linear-programming complexity are conventional proofs and are marked as such.