When does a negative assay exclude a finite target count? Sharp false-exclusion bounds for native-reference reporting rules

A negative readout need not exclude targets in the original specimen when extraction failures are shared across targets and splitting consumes material. We study a finite, well-mixed specimen with conditionally independent target paths and arbitrary dependence between two preparation recoveries. A sharp moment bound reduces the all-negative probability to four recovery states. An explicit reporting rule accepts each of $m$ independent native-reference pairs whenever at least one reference is recovered, and issues a count-exclusion certificate only if the future assay is also negative. For balanced effective fractions $a$, the exact worst-case probability of a false certificate is $G_m((1-a)^K)$, where $G_m(H)=\max_{0\le z\le1}z^m[1-(1-H)z]$ has a closed two-branch formula; no equality of marginal recovery means is needed, and an explicit source attains the value. We then quantify four things that a reporting rule must survive. Reusing one calibration across $T$ independent specimens has an exact familywise value with an irreducible floor $1-(1-H)^T$, so a five percent familywise level is unreachable for two specimens in the worked design however many references are bought. Replacing the exactly-one reference input by Poisson loading of mean $\lambda$ leaves the guarantee intact for $\lambda\le1$, has a closed sharp value $d_\lambda^{\,m}G_m((1-2a)^K)$ under an explicit rational criterion, and in general reduces to a one-dimensional concave-envelope problem; heavy loading destroys the guarantee outright. An event-specific allowance for observation-law mismatch replaces a product-coupling bound that was an order of magnitude looser. Spurious control positives admit an exact reduction to the same scalar problem, and the resulting specificity budget — a pair false-positive rate below about $1/300$ — is the binding practical constraint. Finally, imposing equal means and nonnegative covariance moves the feasibility threshold from $(1-a)^K$ to $(1-2a)^K$, which makes an otherwise impossible exclusion attainable. The central chain and the new batch, false positive and Poisson results are mechanized in Lean 4; biological transport remains an experimental premise.