Reliable repeated harvesting in a finite-molecule autocatalytic reactor: a source-level finite-horizon operating theorem with a machine-checked proof

Repeated harvesting asks a reactor that has just been thinned to make product and to restore its own catalytic stock before the next withdrawal. At finite molecule number this is a probabilistic question: the withdrawal is a random thinning of individual molecules, the catalyst is regrown by a Markov jump process, and the state from which the next cycle starts is the actual random endpoint of the previous one. We prove a joint finite-horizon operating theorem for one explicitly specified six-species stochastic mass-action reactor with maintained fuel and waste, continuous food supply and washout, and a copy scale $V$. Each cycle independently retains, withdraws or loses every molecule according to a history-dependent intervention, adds only food, and runs the literal twenty-channel count process for four time units, collecting effluent during the last unit. One event on the full normalized history law requires, in every cycle, return of the actual endpoint to an explicit restart set, two overlapping output thresholds ($\lceil V/56\rceil$ template equivalents and $\lceil V/1080\rceil$ free template molecules), two food allowances and a gross driven-service allowance, together with pathwise net-synthesis accounting for every physical realization. For every integer $V\ge2\times10^{11}$, every admitted restart state, every parameter pair in the rectangle $r\in[19,21]$, $d\in[1/50,1/25]$ and every controller acting on the complete returned history, the probability that $m$ consecutive cycles all succeed is at least $(1-e(V))^m\ge1-m\,e(V)$ with $e(V)\le101e^{-V/10^{10}}$. Hence a copy scale logarithmic in $m/\delta$ achieves failure tolerance $\delta$: at $V=2\times10^{11}$, $48{,}000$ cycles succeed jointly with probability at least $99\%$ and $100$ cycles with probability at least $99.9979\%$. Net internal synthesis is positive after $55$ successful cycles from every admitted start. The proof combines exponential tests for a molecular pulse, a backward tilt schedule for seeded catalytic recovery, a positive short-window phase-transport estimate from bound catalyst to free product, marked counters on one reaction law, an identification of the stopped uniformized device with the physical chronological process by a renewal identity and material-height exhaustion, and conditioning on actual returns instead of independence between cycles. The entire chain, including nonexplosion and the identification, 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 maintained reservoirs; no molecular implementation is asserted.