Finite-copy productive operation in a reversible autocatalytic binding network: an explicit probability guarantee with a machine-checked proof

Structural criteria for autocatalysis, such as reflexively autocatalytic food-generated (RAF) sets or stoichiometric autocatalytic cores, certify that a reaction network can in principle amplify its own catalysts. They do not decide whether a reactor that starts with food alone will actually establish catalytic material, keep enough of it in the face of washout and reversible sequestration, and export a specified amount of product within a specified time. We prove such a finite-time operating guarantee for one explicit six-species open stochastic reaction network with exact integer-count propensities: basal and template-catalysed ligation of two food species into a product $X$, reversible binding of $X$ to its substrates, duplex formation and release, continuous food supply and washout. At copy scale $V=10^8$ and from the food-only initial state, the event that a weighted catalytic count enters a prescribed band by time $500$, stays above a lower threshold thereafter, resources remain in a corridor, and at least $10^7$ covalent mass units are exported during $(500,1000]$ has probability at least $9/10$, for every equilibrium-bias parameter $K\in[8,12]$ and release parameter $r\in[18,22]$. Removing only the two catalytic ligation channels leaves a network in which a conservative version of the same export event has probability below $1/5000$. The proof is a chain of generator estimates on finite stopped uniformized kernels: conserved resource units control free food, a weighted catalytic count turns free and bound catalyst into a single drift inequality, a changing exponential test yields entry by a fixed deadline, a return potential pays for residence from the random entry state, and a marked-export tilt yields the lower tail of exported mass. All failures are charged to one union bound under one law; no independence between stages, deterministic approximation, or restart at entry is used. The combined theorem is formally verified in Lean 4 with Mathlib. The result concerns the specified mechanism and parameter box; it is not a claim about generic random reaction networks or experimentally calibrated rates.