Certifying fresh microbial conversion from finite challenge records: a sharp two-pool material bound

A finite record of product collected from a microbial preparation is compatible both with fresh conversion and with release of material that was already present. We study this ambiguity in a two-window material model with a mobile product pool, a convertible reserve pool, release, uptake, losses, and an intervening recovery step with pool-specific retention. Given calibrated upper bounds on initial stock $B$, on the pre-wash reserve $J$, on credited recovery input $H$, and retention factors $0\le e\le s\le1$, we prove that the fresh credited inventory $F_1+F_2$ generated during the two windows is at least $L$, the maximum of five affine expressions in the two observed collections, and that $L$ is exactly the minimum of $F_1+F_2$ over the declared class: an explicit finite material schedule attains it from every admissible initial split of the stock. The lower bound, an equivalent remaining-stock form, the attaining schedule and the resulting exactness statement are verified in Lean 4 against Mathlib. An exact counterexample shows that an initial reserve ceiling cannot be substituted for the pre-wash ceiling, because uptake during the first window moves mobile product into the better retained pool; we also verify a zero-fresh history lying inside the reported output envelopes of our worked record. We then prove that a bound on the initial reserve together with a cumulative uptake cap is a valid alternative premise: the same five expressions, evaluated at $J_0=\overline R+\overline T$, remain sound and remain exactly attained, so destructive pre-wash measurement is sufficient but not necessary. Finally we quantify what a wash buys. At a matched material source the mobile retention factor cancels from the certificate, so removing known product is not itself an improvement; the entire benefit is attenuation of first-window measurement uncertainty, worth $(s-e)\bigl(\epsilon_1-(J-r)\bigr)$ in the regime where the reserve-sensitive expression is active. In a synthetic $10\,$mL example the washed certificate is $1.69$ $\mu\mathrm{mol}$ against $1.52$ $\mu\mathrm{mol}$ for a matched unwashed protocol, and that $0.17$ $\mu\mathrm{mol}$ margin is erased by reserve slack $\delta$ or by lost productive activity: strict improvement holds exactly when the retained activity exceeds $\tfrac{193}{210}+\tfrac{17}{42}\delta$. All numerical inputs are synthetic. The results are an assay-design theory with a proposed biological application; they are not biologically calibrated, and the certificate does not assert substrate-specific atom attribution, viability, or future function.