Inherited chemical-state selection across serial transfers: a finite stochastic construction with a machine-checked proof

A heritable chemical difference between compartments supports repeated selection only if the selected state survives the operations that separate one competition from the next: growth on a shared resource, transfer of a random subset of intact compartments, a recovery interval without growth, and replenishment. We construct a finite stochastic chemical population in which these operations are specified literally and prove a joint probability guarantee across two complete cycles. The resident chemistry is a four-species count network with thirteen channels, completed to six materially balanced reversible pairs with maintained reservoir activities and a single compatible potential assignment. A shared growth precursor couples all compartments; division is complementary at doubled size; transfer chooses exactly $M$ intact compartments uniformly without replacement, with no dependence on their chemical state; a fixed precursor-free interval returns the very compartments that were selected to a certified ready region; refill supplies fresh precursor in proportion to their actual total size. For a balanced newborn population of $M$ compartments, half in each of two stationary chemical states, we prove that after two cycles both measured chemical types remain present and the high-to-low compartment-count log odds have increased by more than $G_2=\frac75\log2-\frac{19}{250}-2\log\frac{51}{49}=0.814395\ldots$, with certified probability at least $495999/500000$ for the witness $N=6.5536\times10^{22}$ size units and $M=4\times10^{9}$ retained compartments; the high-state fraction consequently exceeds $0.693045\ldots$. The proof combines source-specific exponential barriers for the batch, a second-moment bound for uniform sampling without replacement whose variance is at most its mean, a fixed-time recovery estimate applied to the actual selected compartments, capped service counters that leave the physical law unchanged, and conditional composition of finite stopped laws without any independence assumption. An endpoint identity converts size selection into count selection while charging the division-phase penalty only once at the two endpoints rather than at every cycle. The finite marked laws, all probability inequalities, the source instantiation and the quantitative witnesses are verified in Lean 4. The construction assumes maintained resident activities and effective growth and division; its scale is an existence witness, not a laboratory prediction, and every limitation of scope is stated.