# Specimen reliability and finite-count exclusion

Companion to manuscript 60, SHA-256 `1dc510ae7b7bfe6e68deeb68dd67fbb4c0f39d25d340499b2feab171dc34f530`. Python 3.11+. Inputs are designed mathematical assay parameters, not measurements or an operationally validated assay.

```sh
python -m venv .venv
# Activate the environment using your platform's command.
python -m pip install -r requirements.txt
python -m unittest -v
python example.py --output outputs
```

## The result and its meaning

For an original finite count N, each target is assigned to one of five mutually exclusive paths: unallocated, lost after entering A, detected in A, lost after entering B, detected in B. A latent recovery pair (X,Y) is drawn once per specimen. Conditional on it, target paths are independent, with probabilities `1-a-b, a(1-X), aX, b(1-Y), bY`. Thus the negative probability is **E[(1-aX-bY)^N]**, not a power evaluated at the mean recovery. Two independent Poisson aliquots would be a different model.

Reference pairs contain exactly one native target in each usable input. Their four outcomes have probabilities `1-p1-p2+q, p1-q, p2-q, q`, where p1=E[X], p2=E[Y], q=E[XY]. Keep all four outcomes, including both-success and both-failure. References are independent pairs drawn from the same recovery population and independent of the future specimen. Preparation loss is already in a,b; it is not deducted a second time from reference recovery.

The gate accepts if every pair has at least one recovery. For balanced fractions and N>=K, its complete false-exclusion event has the sharp bound `G_m(H)=max_w w^m(1-(1-H)w)`, with H=(1-a)^K. The exact maximizer is `min(1,m/((m+1)(1-H)))`. A corner-supported recovery population attains this maximum. The conditional future miss probability is unchanged by conditioning on an independent reference gate: the guarantee concerns the joint event, not posterior confidence in N.

Default original/available volumes are 1 mL, with 0.05 mL loss in each preparation. Hence a=b=.45. K=6 and m=9 give **0.04987721425**; eight pairs fail the .05 requirement. K=2 and K=5 are unreachable regardless of the number of pairs because their floors H exceed .05. The reference experiment consumes 18 preparations and 18 exact native targets; at the illustrative external input volume .5 mL per preparation it also consumes 9 mL of external reference material. It does not borrow this volume from the original specimen.

## Reusable pieces

* `model.py`: immutable `SpecimenBudget`, finite-mixture `SourceLaw`, and `ExclusionPolicy`. Source laws supply exact moments, reference outcomes, finite-count negative probabilities and whole-specimen simulation. Policies preserve complete records and refuse incomplete, invalid, failed-gate, positive-target or uncertified designs.
* `certificates.py`: exact single/batch, total-variation and specificity bounds; outward rational exponential enclosures; `PoissonReference`; adaptive exact source-constraint certificates.
* `example.py`: editable inputs first, independent demonstrations, exact source witnesses, seeded finite-target illustrations, output tables and figures. No universal assay base class is required.

Import these classes to sweep allocation or count thresholds, replace the latent population, or attach a different observation layer. For example:

```python
from fractions import Fraction as F
from model import SourceLaw, ExclusionPolicy
law = SourceLaw.corners(F(4,5), F(4,5), F(16,25))
policy = ExclusionPolicy(F(9,20), F(9,20), 6, 9)
print(law.negative(6, policy.a, policy.b))
print(policy.report(['10','01','11','10','11','01','10','11','11'], 0))
```

All probability inputs should use `Fraction`, rational strings or integers. Using a binary float records that float's exact rational value. For unequal aliquots, the unrestricted bound uses `max((1-a)^K,(1-b)^K)` and the adversary puts single-good states on the smaller aliquot. Balanced-only Poisson and equal-mean demonstrations are skipped for unequal fractions. Reference tables with additional assumptions are labeled separately and are freshly checked after edits; a manuscript's original minimal pair count is not assumed to remain optimal.

## What changes the design

**Known moments.** A corner population with the same p1,p2,q simultaneously maximizes the negative probability for all allocations and counts. The example reconstructs the K=2 comparison: the single-preparation risk is .202, versus .1432 for a split with p=.8,q=.64 and .20395 for q=.79. The exact switch is q=106/135. Pairing can help or hurt depending on the joint source law.

**Batch reuse.** For T independent null specimens sharing one reference gate, the sharp familywise error is the maximum of `w^m[1-(1-H)^T w^T]`. Its floor is `1-(1-H)^T`. For default K=6, even T=2 has floor .054595..., so no number of references reaches .05. The example reproduces the largest reachable batch sizes and pair counts for K=8,10,12: (6,96), (20,330), (66,1070). A numerical proposal locates each count; exact integer-power comparisons prove its pass and the preceding count's failure. Expected false-report counts and per-specimen marginal bounds must not be substituted for familywise control. Shared specimen dependence would require another model.

**Poisson reference loading.** With mean loading lambda, pair acceptance conditional on S=X+Y is `1-exp(-lambda*S)`. This differs from the exactly-one-native-target model. The general sharp solution is the upper concave envelope of `(1+(a/lambda)*log(1-z))^K`, followed by maximizing z^m times that envelope. `envelope_numeric` returns the maximizing one/two-state diagonal source as well as the numerical value; it never certifies a reporting decision.

The simpler exact chord result is valid only when `K*a*(1-exp(-2*lambda)) >= lambda*(1-(1-2*a)^K)`. Outward rational exponential intervals classify the condition as certified, invalid or unresolved. `chord_bound` returns no bound outside the certified regime. At lambda=2.5, seven pairs are certified even though the stricter global-convexity condition fails. At lambda=3, a two-point source with S=.23 and 2, weights .2 and .8, exceeds the inapplicable chord expression. At lambda=100, constant X=Y=.05 yields joint error above .75. More loaded references can hide poor recovery. Independent Poisson loading and the declared conditional thinning law are essential; shared uncertain loading is not handled by substituting its mean.

**Observation mismatch.** The configured whole-pair total-variation allowance and independent target-law allowance yield `max_w min(1,w+ec)^m min(1,1-(1-H)w+et)`, evaluated at its exact finite critical set. With m=9, ec=et=.0001, this sharper event bound passes .05 while the generic product-TV bound fails. At .001 the event bound also fails; that means the design is not certified, not that its actual error is proved excessive. These allowances are assumptions, not inferred from assay CVs or simulation.

**Spurious reference positives.** A separately modeled false-positive pair probability kappa changes acceptance to `kappa+(1-kappa)w`. The exact sharp bound passes for kappa=1/300 and fails for 1/250 at the reference design. At least 898 all-clean negative-control pairs are needed to place a one-sided 95% bound below 1/300; 897 fail. This separate confidence procedure has its own failure probability, which must be included before plugging a data-dependent specificity estimate into a final error guarantee. No beneficial target false-positive contribution is assumed.

**Source constraints.** Equal recovery means together with nonnegative covariance lower the adversarial maximum to a one-dimensional polynomial curve. Adaptive exact rational interval bounds certify the reference counts 38,16,11,9,8 for K=2,3,4,5,6, and exact rational witnesses refute the preceding counts. The limiting floor is J=(1-2a)^K. Nonnegative covariance alone does not improve the unrestricted guarantee: the example's Y=0 adversary already has covariance zero. An exhausted interval budget is explicitly unresolved, never a proof of feasibility or impossibility.

## Reporting and evidence boundaries

`ExclusionPolicy.report` implements only the exactly-one-target, independent reference, prespecified single-experiment contract. Poisson, batch, mismatch and constrained-source calculations are separate design tools, not silently combined into that report. To operationalize an extension, construct a policy whose complete assumptions and combined allowance are justified together. Repeating gates until one passes changes the experiment and can drive false exclusion toward one; the single-gate guarantee cannot be reused for such retries. Choosing pairs or a threshold after observing outcomes also needs a different guarantee.

The synthetic independent Bernoulli(.8) population illustrates utility. Its reference gate passes with probability .96^9. For N=0,...,5, the saved joint report probabilities quantify useful low-count exclusions; “fewer than six” does not mean “zero”. Simulation draws complete original specimens and full reference records and is descriptive, not a rare-error certification. The seven test groups check dependency preservation, adversarial attainment, exact minimality, reporting refusal, batch decisions, Poisson counterexamples, error margins and constrained-source certificates. No external measurement or Lean proof is rerun.

Outputs include exact fractions and decimal conveniences, design sweeps, source witnesses, classification records, figures and SHA-256 provenance. Large exact batch powers are recomputed for decisions rather than stored as enormous decimal strings. Numerical concave-envelope curves and seeded simulation are explicitly distinguished from exact rational inequalities.

## License

MIT is proposed for this example, pending the owner's decision. No new license grant is asserted by this package; manuscript and repository terms remain separate.