Conservative exchange preserves repeated production in autocatalytic reactor networks: a uniform composition theorem with a machine-checked proof

An isolated reactor’s guarantee of repeated productive operation does not automatically survive connection to other reactors: exchange changes the state during recovery, and the exchanged material includes the catalyst in all of its chemical forms. We prove that it does survive for a specified family. Any finite number of equal-volume, maintained, reversible six-species autocatalytic reactors, each with its own release and cleavage speeds in a fixed rectangle, is connected by an arbitrary finite symmetric nonnegative exchange graph in which every edge transports all six internal species with one common coefficient. Synchronized harvesting interventions withdraw a quarter to three quarters of each reactor, allow up to two percent additional species-dependent loss, refill only food with a bounded error, and may depend on the completed history of the whole assembly. From any admitted preparation, one pulse and twelve normalized time units carry the assembly into an operating region; thereafter every pulse followed by four units of flow returns the actual coupled state to that region, and the last unit of every cycle collects at every node at least $1/28$ template equivalents and at least $1/160$ of the free template species, with explicit food and driven-service allowances that are linear in the number of cycles. The constants do not depend on the number of reactors, the graph, or the exchange strength. The proof rests on three properties of common transport (it commutes with fixed linear observables, is nonnegative at a node that minimizes such an observable, and cancels from summed accounts), a finite simultaneous comparison principle that never differentiates a moving minimum, guarded catalytic growth at the least-stock node, and a backward-evolving phase observable that converts complexed stock into a free-product guarantee; a degree-four truncation of the backward weight improves an earlier floor of $1/209$ to $1/160$. An inventory telescope proves net synthesis beyond the initial template stock. An exact two-node witness shows that species-selective exchange breaks the minimum-drift argument. The trajectory, return, output, resource, arbitrary-repetition and net-synthesis statements are verified in Lean 4 as one declaration, together with closed path and ring instances; conventional corollaries give mission sizing, endpoint rates and architecture-dependent handling bounds, and a dimensioned four-reactor array with numerical diagnostics illustrates the constants without asserting a molecular realization.