Positive reference controls can check assay recovery, but targets in a specimen may still be lost during preparation or missed in its aliquots. This example designs a complete procedure: allocate a finite specimen, observe every reference pair, and issue a count exclusion only when the prespecified reference-control acceptance rule and error bound allow it.

With a 1 mL specimen and a 0.05 mL loss per preparation, the balanced usable fractions are 0.45 and 0.45. Nine independent pairs containing exactly one native target per reference input support the statement “fewer than six original targets” at a sharp joint false-exclusion bound of 4.9877%. An explicit adversarial recovery distribution attains that bound. This is a guarantee about the complete experiment, not a posterior probability or a claim of zero targets.

Sharp exclusion bounds decline to count-dependent floors as reference pairs increase; batch reuse raises the familywise error floor.
Exact finite-count design formulas. The horizontal dotted line is the configured error allowance. Reference success cannot remove the specimen-allocation floor.
Poisson reference loading changes the sharp error, and small observation-law errors consume the narrow default design margin.
Left: numerical concave-envelope exploration, separate from certified Poisson chord bounds. Right: exact event-specific total-variation allowances evaluated over the displayed input grid.

The reusable model keeps one shared recovery state per specimen and sends each original target into at most one aliquot. Editable inputs control specimen volume, preparation loss, allocation, count threshold, reference count and error allowances. Exact arithmetic checks design decisions; simulations illustrate the model without authorizing the report.

The extensions matter operationally. Reusing the same reference-control result for two specimens has a familywise error floor above 5%. Poisson-loaded references need a different certificate, and the code refuses the simple chord formula when its condition fails. Observation mismatch, control false positives, and additional source constraints are evaluated separately with their assumptions visible.

Download the package for composable source, specimen, policy and certificate classes, exact witnesses, numerical concave-envelope exploration, parameter sweeps and seven scientific test groups. The values are designed mathematical inputs; no measured assay validation or Lean rerun is implied.

Python source

"""A reusable finite-count exclusion design, with sharp adversarial witnesses."""
from fractions import Fraction as F
from pathlib import Path
import argparse,csv,hashlib,json,platform
import numpy as np
from model import SpecimenBudget,SourceLaw,ExclusionPolicy,gate_bound,minimum_pairs,moment_bound
from certificates import batch_certificate,observation_bound,specificity_bound,PoissonReference,constrained_certificate,constrained_value,exp_negative

# EDITABLE INPUTS: designed mathematical example, not measured assay performance.
ORIGINAL_ML='1'
AVAILABLE_ML='1'
LOSS_PER_PREPARATION_ML='0.05'
SPLIT='0.5'
COUNT_THRESHOLD=6
REFERENCE_PAIRS=9
FALSE_EXCLUSION_ALLOWANCE='0.05'
RECOVERY_MEAN='0.8'             # illustrative independent Bernoulli source only
CONTROL_LAW_TV='0.0001'        # whole pair-law error, assumed, not estimated here
TARGET_LAW_TV='0.0001'
REFERENCE_LOADING='2.5'         # mean native targets per Poisson reference input
INTERVAL_BUDGET=100000
PAIR_SEARCH_BUDGET=4000
SIMULATION_REPLICATES=2000
SEED=60092026
MANUSCRIPT_SHA256='1dc510ae7b7bfe6e68deeb68dd67fbb4c0f39d25d340499b2feab171dc34f530'


def main():
    parser=argparse.ArgumentParser(description=__doc__);parser.add_argument('--output',type=Path,default=Path('outputs'))
    out=parser.parse_args().output;out.mkdir(parents=True,exist_ok=True)
    budget=SpecimenBudget(F(ORIGINAL_ML),F(AVAILABLE_ML),F(LOSS_PER_PREPARATION_ML));a,b=budget.fractions(F(SPLIT))
    alpha=F(FALSE_EXCLUSION_ALLOWANCE);policy=ExclusionPolicy(a,b,COUNT_THRESHOLD,REFERENCE_PAIRS,alpha)
    H=max((1-a)**COUNT_THRESHOLD,(1-b)**COUNT_THRESHOLD);g,z=gate_bound(H,REFERENCE_PAIRS)
    # Least-favourable law concentrates single-good specimens on smaller aliquot.
    witness=SourceLaw.corners(z if a<=b else 0,z if b<a else 0,0)
    assert witness.joint_error(COUNT_THRESHOLD,a,b,REFERENCE_PAIRS)==g
    p=F(RECOVERY_MEAN);synthetic=SourceLaw.corners(p,p,p*p)
    def dump(name,data):
        (out/name).write_text(json.dumps(data,indent=2,default=lambda x:{'exact':str(x),'decimal':float(x)} if isinstance(x,F) else str(x))+'\n',encoding='utf-8')
    def table(name,header,rows):
        with (out/name).open('w',newline='',encoding='utf-8') as f:w=csv.writer(f);w.writerow(header);w.writerows(rows)
    thresholds=[]
    for K in [2,5,6,8,10]:thresholds.append(dict(K=K,H=max((1-a)**K,(1-b)**K),**minimum_pairs(max((1-a)**K,(1-b)**K),alpha,PAIR_SEARCH_BUDGET)))
    batch=[dict(T=T,**batch_certificate(H,REFERENCE_PAIRS,T,alpha)) for T in [1,2,5,10,24]]
    # The exact rational power can be very large; JSON retains it for audit.
    reach=[]
    for K in [6,8,10,12]:
        h=max((1-a)**K,(1-b)**K);T=1
        while T<1000 and 1-(1-h)**(T+1)<=alpha:T+=1
        if 1-(1-h)**T>alpha:reach.append(dict(K=K,status='infeasible'));continue
        import math
        c=float((1-h)**T)
        def approx(m):
            return 1-c if c<=m/(m+T) else math.exp(math.log(T/(m+T))+m/T*(math.log(m/(m+T))-math.log(c)))
        proposal=next((m for m in range(1,PAIR_SEARCH_BUDGET+1) if approx(m)<=float(alpha)),None)
        m=proposal if proposal and batch_certificate(h,proposal,T,alpha)['certified'] else None
        reach.append(dict(K=K,largest_batch=T if T<1000 else None,pairs=m,status='certified' if m and T<1000 else 'budget-exhausted',
                          previous_fails=m==1 or (m is not None and not batch_certificate(h,m-1,T,alpha)['certified'])))
    observation=[]
    for m,e in [(9,F(0)),(9,F(1,100000)),(9,F(1,10000)),(9,F(1,1000)),(10,F(1,1000)),(10,F(3,1000)),(12,F(3,1000))]:
        ideal=gate_bound(H,m)[0];event=observation_bound(H,m,e,e)
        observation.append(dict(m=m,epsilon=e,ideal=ideal,product=min(F(1),ideal+1-(1-e)**(m+1)),event=event,certified=event<=alpha))
    specificity=[dict(kappa=k,bound=specificity_bound(H,REFERENCE_PAIRS,k),certified=specificity_bound(H,REFERENCE_PAIRS,k)<=alpha)
                 for k in [F(0),F(1,1000),F(1,300),F(1,250),F(1,100),F(1,30)]]
    clean=next(n for n in range(1,10000) if F(299,300)**n<=F(1,20))
    poisson=[];constrained=[];poisson_counterexample=None;configured_loading=None
    if a==b and a>0:
        ref=PoissonReference(F(REFERENCE_LOADING),a,COUNT_THRESHOLD)
        configured_loading=dict(loading=F(REFERENCE_LOADING),chord_status=ref.chord_status(),bound=ref.chord_bound(REFERENCE_PAIRS),numerical=ref.envelope_numeric(REFERENCE_PAIRS))
        for loading in [F(1,2),F(1),F(2),F(9,4),F(5,2),F(3)]:
            ref=PoissonReference(loading,a,COUNT_THRESHOLD);m=None
            if ref.chord_status()=='certified':
                m=next((n for n in range(1,100) if ref.chord_bound(n)[1]<=alpha),None)
            poisson.append(dict(loading=loading,chord_status=ref.chord_status(),pairs=m,
                                bound=ref.chord_bound(m) if m else None,
                                previous_fails=(m==1 or ref.chord_bound(m-1)[0]>alpha) if m else None,
                                numerical_envelope=ref.envelope_numeric(REFERENCE_PAIRS)))
        ref=PoissonReference(3,a,COUNT_THRESHOLD);J=(1-2*a)**COUNT_THRESHOLD
        poisson_counterexample=dict(two_point_source=ref.source_error([(F(1,5),F(23,100)),(F(4,5),F(2))],REFERENCE_PAIRS),
             invalid_chord_upper=(1-exp_negative(6)[0])**REFERENCE_PAIRS*gate_bound(J,REFERENCE_PAIRS)[0],
             heavy_loading=PoissonReference(100,a,COUNT_THRESHOLD).source_error([(F(1),F(1,10))],REFERENCE_PAIRS))
        for K,guess in [(2,38),(3,16),(4,11),(5,9),(6,8)]:
            h,j=(1-a)**K,(1-2*a)**K
            # These are manuscript reference pair counts, freshly checked, not
            # assumed to remain minimal after editing the specimen fractions.
            good=constrained_certificate(h,j,guess,alpha,INTERVAL_BUDGET)
            bad=constrained_certificate(h,j,guess-1,alpha,INTERVAL_BUDGET)
            constrained.append(dict(K=K,pairs=guess,upper_certificate=good,previous=bad,
                minimal_certified=good['status']=='certified' and bad['status']=='refuted'))
    rng=np.random.default_rng(SEED);simulation=[]
    for label,law in [('synthetic',synthetic),('sharp-adversary',witness)]:
        outcomes=law.pair_outcomes();labels=list(outcomes);probs=[float(outcomes[k]) for k in labels]
        issued=0;gate_passes=0;misses=0
        for _ in range(SIMULATION_REPLICATES):
            references=rng.choice(labels,size=REFERENCE_PAIRS,p=probs).tolist()
            target=law.sample_specimen(COUNT_THRESHOLD,a,b,rng)
            gate_passes+=int('00' not in references);misses+=int(target['detected']==0)
            issued+=int(policy.report(references,target['detected'])['issued'])
        simulation.append(dict(source=label,replicates=SIMULATION_REPLICATES,gate_passes=gate_passes,negative_targets=misses,
            exclusions=issued,analytic_joint=law.joint_error(COUNT_THRESHOLD,a,b,REFERENCE_PAIRS),
            evidence='Seeded illustration only; exact theorem bound, not Monte Carlo frequency, authorizes reporting.'))
    nonblank=[dict(N=n,report_probability=synthetic.joint_error(n,a,b,REFERENCE_PAIRS)) for n in range(COUNT_THRESHOLD)]
    moment_demo=dict(single=1-F(4,5)+F(4,5)*F(1,20)**2,
        split_low_q=moment_bound(2,F(9,20),F(9,20),F(4,5),F(4,5),F(16,25)),
        split_high_q=moment_bound(2,F(9,20),F(9,20),F(4,5),F(4,5),F(79,100)),switch_q=F(106,135))
    report=policy.report(['10']*REFERENCE_PAIRS,0)
    summary=dict(specimen=dict(original_ml=budget.original_ml,available_ml=budget.available_ml,a=a,b=b,single=budget.single()),
        policy=dict(K=COUNT_THRESHOLD,m=REFERENCE_PAIRS,alpha=alpha,H=H,bound=g,maximizer=z,adversary=witness.atoms),
        illustrative_complete_record=report,missing_record=policy.report(['10']*(REFERENCE_PAIRS-1),0),
        reference_budget=dict(preparations=2*REFERENCE_PAIRS,exact_native_targets=2*REFERENCE_PAIRS,external_input_ml=F(1,2)*2*REFERENCE_PAIRS),
        synthetic_moments=synthetic.moments(),synthetic_reference_outcomes=synthetic.pair_outcomes(),
        configured_observation_bound=observation_bound(H,REFERENCE_PAIRS,F(CONTROL_LAW_TV),F(TARGET_LAW_TV)),
        clean_negative_controls=dict(pairs=clean,previous_fails=F(299,300)**(clean-1)>F(1,20),coverage_failure=F(1,20),
        note='A 95% bound for kappa is a separate confidence statement. Its failure probability must be budgeted before using it in a reporting guarantee.'),
        moment_comparison_reference=moment_demo,simulation=simulation,
        assumptions=['One shared latent state per specimen; targets independent conditional on that state.',
        'Reference pairs independent of one another and the future specimen, with the same source law.',
        'Exactly one native target per usable reference input unless explicitly using the Poisson model.',
        'One prespecified gate and report; no retry-until-pass or postselection of pairs.',
        'Batch results require independent future specimens; marginal error is not familywise error.',
        'Designed model values; no measured assay, clinical validation or rerun of Lean.'])
    dump('summary.json',summary);dump('thresholds.json',thresholds);dump('batch.json',dict(reuse=batch,reach=reach))
    dump('observation.json',dict(total_variation=observation,specificity=specificity));dump('poisson.json',dict(configured=configured_loading,rows=poisson,counterexample=poisson_counterexample))
    dump('constrained.json',constrained);dump('nonblank.json',nonblank)
    table('design_sweep.csv',['K','pairs','sharp_bound','floor'],((K,m,float(gate_bound(max((1-a)**K,(1-b)**K),m)[0]),float(max((1-a)**K,(1-b)**K))) for K in [2,5,6,8,10] for m in range(1,81)))
    plot(out,a,b,alpha,batch,poisson)
    print(f'Sharp joint false-exclusion bound: {float(g):.11f}; design certified: {g<=alpha}')
    print('Reference gate does not change the independent future specimen miss probability. Retain the complete event.',flush=True)
    digest=lambda p:hashlib.sha256(p.read_bytes()).hexdigest();here=Path(__file__).parent
    dump('run_metadata.json',dict(manuscript_sha256=MANUSCRIPT_SHA256,source_sha256=digest(Path(__file__)),python=platform.python_version(),
        module_sha256={n:digest(here/n) for n in ['model.py','certificates.py']},output_sha256={p.name:digest(p) for p in sorted(out.iterdir()) if p.is_file() and p.name!='run_metadata.json'}))


def plot(out,a,b,alpha,batch,poisson):
    import matplotlib
    matplotlib.use('Agg')
    import matplotlib.pyplot as plt
    fig,axs=plt.subplots(1,2,figsize=(10,4),layout='constrained')
    for K in [2,5,6,8,10]:
        h=max((1-a)**K,(1-b)**K);axs[0].plot(range(1,81),[float(gate_bound(h,m)[0]) for m in range(1,81)],label=f'K = {K}')
    axs[0].axhline(float(alpha),color='black',ls=':');axs[0].set(xlabel='Independent reference pairs',ylabel='Sharp joint false-exclusion bound',ylim=(0,.33),title='False-exclusion bounds by target count and\nreference number');axs[0].legend(fontsize=8)
    axs[1].plot([r['T'] for r in batch],[r['bound_numeric'] for r in batch],'o-',label='Sharp bound with configured gate')
    axs[1].plot([r['T'] for r in batch],[float(r['floor']) for r in batch],'s--',label='Floor even with more references')
    axs[1].axhline(float(alpha),color='black',ls=':');axs[1].set(xlabel='Independent null specimens sharing the gate',ylabel='Familywise false-exclusion probability',title='Error from sharing reference controls\nacross specimens');axs[1].legend(fontsize=8)
    for ax in axs:ax.grid(alpha=.2)
    fig.savefig(out/'design.png',dpi=180);fig.savefig(out/'design.svg');plt.close(fig)
    if a==b and a>0:
        fig,axs=plt.subplots(1,2,figsize=(10,4),layout='constrained');load=np.linspace(.2,3.5,70)
        vals=[PoissonReference(str(l),a,COUNT_THRESHOLD).envelope_numeric(REFERENCE_PAIRS)['bound'] for l in load]
        axs[0].plot(load,vals,label='Numerical concave-envelope maximum');axs[0].axhline(float(alpha),color='black',ls=':');axs[0].set(xlabel='Mean native targets per reference input',ylabel='Joint false-exclusion probability',title='False-exclusion probability versus\nreference loading');axs[0].legend(fontsize=8)
        eps=np.linspace(0,.003,80);h=(1-a)**COUNT_THRESHOLD
        for m in [9,10,12]:axs[1].plot(eps,[float(observation_bound(h,m,F(str(e)),F(str(e)))) for e in eps],label=f'{m} pairs')
        axs[1].axhline(float(alpha),color='black',ls=':');axs[1].set(xlabel='Assumed TV error per experiment',ylabel='Event-specific upper bound',title='False-exclusion bound with observation-law\nerror');axs[1].legend(fontsize=8)
        for ax in axs:ax.grid(alpha=.2)
        fig.savefig(out/'observation.png',dpi=180);fig.savefig(out/'observation.svg');plt.close(fig)


if __name__=='__main__':main()
Run output
Sharp joint false-exclusion bound: 0.04987721425; design certified: True
Reference gate does not change the independent future specimen miss probability. Retain the complete event.