Reliable autocatalytic operation with a finite fuel–waste bath: joint mission guarantees, reservoir sizing and a sharpened certificate
Abstract
A reactor that is repeatedly thinned, refed and harvested must recover its catalytic stock, deliver product, and leave a state from which the next operation can succeed. If its fuel is a genuinely finite molecular inventory rather than a chemostatted activity, then every driven event also changes the chemistry of the next operation, and the guarantee has to be proved for that changed stochastic law. We prove a joint finite-horizon operating theorem for an explicitly specified six-species count reactor coupled to a conserved two-species fuel/waste bath of total inventory and reference capacity , in which the driven channel moves one molecule between the two bath species at every event and its two directed propensities are proportional to the current bath fractions and . One event on the full normalized history law requires, in every one of externally clocked cycles, return of the actual endpoint to an explicit restart set, two overlapping collected-output thresholds, two food allowances and a gross driven-service allowance, together with an all-prefix bound on the bath composition and a pathwise net-synthesis statement for every physical realization. For every admitted bath state, every parameter in the class , , and every controller acting on the returned history, the probability that all cycles succeed is at least .
We then sharpen the certificate in two independent ways and propagate both through the entire chain. First, the published phase-transport exponent discards a factor: the unrounded rate is rather than , and a new absorption estimate makes valid from instead of . Second, on the pure-fuel bath at the two directed service intensities are controlled by correlated bath fractions summing to one, which halves the certified per-cycle gross allowance from to inside the same error budget, and therefore halves the sufficient reservoir at fixed copy scale. Together they give the design rule , . The hundred-cycle instance certified at , with confidence is matched at , ; at the original copy scale the same mission now has failure probability at most with half the fuel. We also give exact finite-bath endpoint free energies, a finite metered-food corollary and deterministic diagnostics separating productive output from fuel turnover. The whole chain, including nonexplosion, the identification of the stopped device with the physical process, the repetition argument and both refinements, is verified in Lean 4 with Mathlib; an exact replay script re-derives every printed constant. The reactor is a schematic benchmark with established catalyst and externally implemented feeds and interventions; reliable production does not imply positive net fuel consumption.