Reliable covalent export from an autocatalytic reactor under driven cleavage: explicit finite-copy operating, output and supply certificates over an exponential horizon
Abstract
We prove an explicit reliability theorem for a six-species continuous-flow autocatalytic reactor with reversible substrate binding, templated ligation, duplex release, and an additional maintained-drive cleavage pathway that returns free covalent product to its two food components. The model is the literal integer-count Markov jump process with mass-action propensities, twenty labelled channels, and a copy scale . Starting from food alone, the reactor establishes a catalytic population by a fixed deadline and then exports a prescribed amount of covalent product in every completed unit observation window. Uniformly over a fixed positive cleavage interval and the kinetic box , , the joint operating event through time has probability at least for every integer . The event includes resource retention, post-entry residence, output in each of windows, and separate gross budgets for food input and for the driving service. A directly proved finite-duration version lets a reader choose any post-startup duration and obtain a certificate whose supply allowances are proportional to ; a sufficient copy scale follows from and a target failure probability. Removing only the templated ligation pair makes the same output schedule exponentially unlikely under a comparison that credits every resource exit as a possible success. Deterministic consequences give output on arbitrarily aligned intervals, expected export, resident inventory of order against replenishment of order , and explicit service and recovery ratios. The proof is a chain of generator inequalities on finite stopped uniformized kernels: startup is paid once, one-window output is bounded pointwise in the chemical state and propagated through the actual continuing distribution, and shared failures are charged once outside the window sum, so no independence between windows is assumed. The finite-kernel probability statements are verified in Lean 4 with Mathlib; nonexplosion of the infinite-state process and its identification with the finite construction are proved conventionally. A worked dimensional example illustrates the bounds without asserting experimental calibration.