Feedback-induced bistability and global state selection in coupled autocatalytic cores

We study a driven four-species mass-action assembly in which two minimal gain-two autocatalytic cores, an $AB$ core and a $ZH$ core, are joined by a shared fork reaction $A\rightleftharpoons B+z$ and a small reverse channel $B+G\rightleftharpoons 2A$. Each module, obtained by clamping the concentrations of the other while keeping every reservoir and load, has exactly one positive equilibrium, and the fully coupled system is unistationary whenever the output loss rate is at least the reference rate. Two questions are answered on two explicitly separated parameter families. In the routed family the fork current is split between a dynamic channel that feeds the $ZH$ module and a buffered channel of the same stoichiometry, with the total forward and reverse fork capacity held fixed at one. Re-routing the fork from buffered to dynamic changes a unique stationary response (isolated and weak feedback) into two locally exponentially attracting positive equilibria (strong feedback), and an exact rational certificate isolates an intervening nondegenerate saddle-node at feedback fraction $g_*\approx0.970187992295$. In the flagship family ($g=1$, reverse-channel rate $e\in[1/200000,1/50000]$) every positive solution exists globally and converges to one of exactly three equilibria; an explicit response potential decreases strictly along every trajectory in an absorbing region, the middle equilibrium is a saddle whose stable set is an embedded real-analytic hypersurface forming the common basin boundary of the two sinks, this separator has Lebesgue measure zero, and a strict energy-and-side test eventually recognizes every trajectory outside it. Finally, along every positive trajectory the $AB$ core is eventually inactive and the $ZH$ core eventually strictly productive, with the same eventual activity signature at both sinks although their compositions differ. The flagship global theorems and the routed coexistence theorem are machine-checked in Lean 4; the fold certificate, the measure, decision and residence consequences, and the local persistence results are conventional proofs given here.