Energy service and peroxide handling in a proteome-constrained red-cell model: exact inventory certificates, a certified turnover plateau, and kinetic limits

Whether stored red cells can sustain an ATP-dependent service while consuming an oxidative challenge is usually approached through a metabolic flux envelope. We ask what such an envelope actually decides. Working with the proteome-constrained S7 instance of RBC-GEM under an explicit finite-horizon relaxation, we prove three exact statements about one concrete model. First, a complete source-matrix inventory certificate: for every cumulative extent vector obeying the declared bounds, balances and terminal floors, the weighted combination of Na/K-ATPase service $M$ and two-route peroxide turnover $Q$ obeys $M+4Q\le w^{\top}(x_0-\ell)+25.439042\,T+4(R_{\textnormal{\textsc{cysglth}}}+ R_{\textnormal{\textsc{lhcystin}}}+R_{\textnormal{\textsc{ssgthrd}}})$, with all $19\,620$ columns and their decimal coefficients retained; the concrete vector inequality is verified in Lean 4. Second, and in a deliberately restricted diagnostic medium, an exact rational primal witness together with two exact dual certificates shows that the optimal turnover is uniformly enclosed, $6.50048030\le F(m)\le 6.50048050$ $\mathrm{mmol}\,\mathrm{gDW}^{-1}$, for every required service $0\le m\le 1.0345238$, while no feasible point at all has service above $1.0345238944791832$. The certified interval therefore covers all but a window of width $9\times10^{-8}$ of the attainable service range, and across it the variation of the optimum is at most $1.93\times10^{-7}$, about $3\times10^{-6}$ percent of the turnover level. Third, the apparent tradeoff reported when four internal reverse sulfur directions are blocked is not reproduced by closing external sulfur supply: a stoichiometric identity shows that the relevant carriers cancel against an independent reductant, so supply accounting cannot bound repeated turnover. We then show what the envelope does not decide. A returned optimum imports $1000$ peroxide units and leaves $993.4995$ of them in the terminal pool; minimising terminal peroxide merely diverts $981.05$ units through uncounted haemoglobin reactions, and only a subsequent parsimony step removes the gratuitous handling. Finite carrier pools supply the missing constraint, and we prove a sharp finite-time recycling bound, $V(T)\le\frac{ab}{a+b}C_{\mathrm{tot}}T+\frac{a}{a+b}(g(0)-\frac{bC_{\mathrm{tot}}}{a+b}) (1-e^{-(a+b)T})$, which is attained, implies the harmonic average-rate ceiling with an $O(1/T)$ correction, and starts quadratically from a fully oxidised pool. A complementary paired-signal recovery identity gives a necessary consistency test for inferring integrated effective reduction from treated and untreated assays. All results are conditional on the stated model instance; a source-supported theorem of stored-cell oxidative tolerance with preserved ATP-dependent function remains open, and we state precisely which measurements would close it.