When can a negative recovery assay exclude a recoverable subpopulation? Sharp coverage, stage mismatch and allocation bounds for paired observations

A finite recovery experiment that records no qualifying event is compatible both with the absence of recoverable units and with a failure to observe their recovery. We give a sharp conditional separation of the two explanations for a gated two-stage source observed under two alternative conditions, with activation and subsequent progeny probabilities $(x,y)$ and $(a,b)$. If the two conditions cover each stage, $x+a\ge c$ and $y+b\ge c$, and the within-condition stage mismatch obeys $|x-y|\le d$, the equally weighted complete-path response is at least $R_{\mathrm{full}}(c,d)=\bigl(c^2-t^2\bigr)/4$ with $t=\min\{d,\min(c,2-c)\}$, and this is attained. Because $c$ bounds a sum of two probabilities, its range is $[0,2]$; on the restricted range $c\le1$ the bound reduces to $\max\{0,c^2-d^2\}/4$, and for $c>1$ a positive floor of at least $c-1$ holds with no mismatch information at all. We compute the exact worst-case response of every fixed allocation weight $w$, which has three regimes, is maximized at $w=1/2$, and is strictly suboptimal away from $w=1/2$ exactly when the mismatch budget binds. The uniform mismatch bound can be weakened to a mean-square budget $\mathbb{E}[(x-y)^2]\le D^2$ without changing the floor. With conditional recording probability at least $\kappa$ on a covered fraction $1-\eta$ of recoverable types, the usable floor is $g=(1-\eta)\kappa R_{\mathrm{full}}(c,D)$. For an even number $n$ of independent eligible units split equally between the two conditions, and recoverable fraction at least $\theta$, the worst-case all-negative probability is exactly $(1-\theta g)^n$; a conditional calibration-failure allowance $\delta$ gives the sharp total bound $\delta+(1-\delta)(1-\theta g)^n$. A finite balanced design achieves total error $\alpha$ if and only if $\theta g>0$ and $\delta<\alpha$, or $\theta g=1$ and $\delta\le\alpha$; no history-dependent reallocation of the same budget improves the guarantee. The coverage, allocation, mean-square, population and decision inequalities are verified in Lean 4. A synthetic example needs $2{,}300$ units to exclude a recoverable fraction of one per cent at five per cent error under its declared premises, and $750$ units when the coverage assumptions are strengthened beyond the restricted range. The result identifies a joint calibration requirement; it does not validate any particular assay, and non-detection is not evidence of irreversible death.