Productive recovery and repeated harvesting in a reversible autocatalytic reactor: a uniform operating theorem with a machine-checked proof

Autocatalytic reaction structure does not by itself establish that a reactor can be harvested repeatedly. Withdrawal changes the chemical state, catalyst can be lost unequally across its bound and free forms, and replenishing food does not replace catalyst. We prove a uniform operating theorem for a specified, materially balanced, reversible mass-action source with fixed compatible thermochemistry: six reversible pairs on the species $U,W,X,C_1,C_2,Z$ with maintained fuel and waste, continuous food supply and washout, over a two-parameter rectangle of release and cleavage speeds. Each intervention withdraws $25$–$75\%$ of the well-mixed contents, permits up to $2\%$ additional species-dependent loss, and adds only food with a bounded refill error. A one-time conditioning period of twelve normalized time units carries any admitted preparation into an operating region; thereafter three units of recovery and one unit of collection return the actual chemical state to that region, for every admissible intervention and for interventions that depend on the current state. Every routine cycle exports at least $1/28$ template equivalents and at least $1/540$ of the free template species, while using at most $951/200$ of each food and at most $9/50$ gross fuel–waste service; the cumulative bounds for conditioning followed by $m$ cycles are explicit and linear in $m$. An inventory identity proves that the net covalent synthesis exceeds $m/28-11/10$, so production beyond any admitted initial stock is certified from the thirty-first cycle onward. The argument combines exact material relaxation, a growth inequality that holds only below a catalytic threshold, a strict exponential fence that replaces first-hitting-time constructions, and integrating-factor transfer inequalities between the catalytic phases. The trajectory, output, resource, arbitrary-finite-repetition and net-synthesis statements are verified in Lean 4 as one theorem; a conventional fixed-point argument adds a productive periodic hybrid trajectory for each fixed intervention. Targeted numerical experiments measure the conservatism of the certified constants. The result concerns a maintained schematic reactor; finite-copy reliability and molecular implementation are outside its scope and are delimited precisely.