# Finite-copy productive operation in a binding reactor

Companion to paper 18, *Finite-copy productive operation in a reversible
autocatalytic binding network: an explicit probability guarantee with a
machine-checked proof*. Manuscript SHA-256:
`5f10655592fdba876cc0e8fbf37bbd3862c4a8506a4f365128ef6756c48950a2`.

The example supplies the six-species reactor, literal integer-count
propensities, a reusable entry/residence/export monitor, deterministic
parameter sweeps, symbolic bookkeeping and exact rational error budgets.
The model begins with food only. Bound catalyst remains part of the catalytic
population; it is not assumed that free templates stay abundant.

## Run

Python 3.11 or newer:

```sh
python -m venv .venv
# PowerShell: .venv\Scripts\Activate.ps1
# macOS/Linux: source .venv/bin/activate
python -m pip install -r requirements.txt
python example.py --output outputs
python -m unittest -v
```

The default calculation uses LSODA and an independent Radau replay, SymPy
algebra, rational probability envelopes, and Matplotlib figures. It does not
attempt to simulate the enormous number of jumps at the certified copy scale.
An optional budget-limited exact count path is available separately:

```sh
python example.py --ssa --output exploratory_outputs
```

At the default V=10^8 and 20000-event computation budget this path will
normally be unfinished far before the deadline. `event_verdict=None` means
no conclusion. The SSA is a usable reference implementation, not an efficient
large-volume approximation; it never silently substitutes tau-leaping.
Use a separate output folder for optional runs so saved default results
remain easy to compare.

## Objects and units

The species are food U and W, covalent template X=UW, substrate complexes
C1=X:U and C2=X:(U,W), and duplex Z=X:X. Five reversible internal pairs
provide basal ligation, two substrate-binding steps, templated ligation and
duplex release. Two food feeds and six washouts bring the total to 18 directed
events. `Reaction` records input multiplicities, output multiplicities,
coefficient, and covalent export mark. `BindingReactor` composes them.

Editable inputs are at the top. V is both the divisor in bimolecular count
propensities and the feed rate of each food species; initially U=W=V.
Washout has unit rate per molecule, so time is measured in inverse-washout
units. K sets the common ligation equilibrium bias, r the duplex-release
rate, and epsilon=1/500000000 the basal coefficient. The rate table is
illustrative chemistry, not experimentally calibrated kinetics. Interpreting
V as a physical volume requires a concentration and time reference.

`count_rate` returns an exact fraction for integer states. Re-association
2X -> Z has rate r*x*(x-1)/V, with no factorial divisor. The vectorized count
kernel uses the same falling factorial. The deterministic kernel uses the
concentration monomial r*x^2 instead. The disabled model deletes exactly
C2 -> Z and Z -> C2; basal chemistry, binding, release, feeds and washout
remain unchanged.

Two conserved internal resource units are

```
A = U + X + 2*C1 + 2*C2 + 2*Z
B = W + X +   C1 + 2*C2 + 2*Z
```

Their count drifts are V-A and V-B. Physical mass is 2(A+B). The weighted
catalytic count is Y=X+(9/8)C1+(7/5)C2+(9/5)Z. These weights measure progress
through the catalytic route and produce the useful low-density drift; Y is
neither a literal count of free templates nor covalent mass. Covalent stock
is S=4X+4C1+4C2+8Z, and the corresponding washout marks are 4,4,4,8.

## The operating event

`OperatingPolicy` separates model parameters from the requested operation.
Its manuscript defaults are:

- V=10^8 and resource corridor 0.9V <= A,B <= 1.1V throughout [0,1000].
- Reach Y>=40000 by time 500.
- After the first entry, never fall below Y=20000 through time 1000.
- Export at least 10^7 covalent units during (500,1000].

`OperatingMonitor` carries the integer state, phase and saturated export
counter. It uses integer 40Y comparisons to avoid threshold roundoff. A
resource exit, return failure or missed entry deadline is absorbing. The
full state passes through time 500; no chemistry or residence state restarts.
Counter saturation does not stop the reactor because later residence or
resource failure still invalidates success. The SSA handles deterministic
time boundaries by exponential memorylessness while retaining the state.

The disabled monitor has no entry or residence condition and no deadline
freeze. Its deliberately conservative event is **export target reached OR
resource exit**. Thus its probability bound also bounds the export event
under weaker conditions than the enabled operating event. This distinction
is preserved in `event_verdict` and should not be replaced by a comparison
of two identical phase tests.

The computational event limit is separate from these scientific stops.
An unfinished run is not a failed operating trial. Each jump is monitored
even though saved count traces are decimated. The direct SSA has a volume
guard below 10^12 and uses 64-bit integer counts.

## What is reproduced

For (K,r)=(8,18),(10,20),(12,22), numerical entry occurs at about 10.0899,
9.5793 and 9.2125 time units. Deterministic export/V over (500,1000] is
726.175, 748.421 and 764.032. The disabled K=10,r=20 trajectory exports about
4e-6 per V. Cumulative output greatly exceeds instantaneous inventory because
food is continuously supplied. CSVs retain all six concentrations and total
cumulative export. Entry times come from solver root events, not a sampled
grid; they remain numerical illustrations.

`symbolic_bookkeeping` independently derives resource drifts and quadratic
rates, the full weighted-Y drift identity, its uniform coefficient bounds,
and the disabled covalent-stock balance from the literal channels. It checks
the parameter-box corners used in the manuscript's inequalities analytically,
not by a random parameter grid. The independent resource vectors also check
the numerical trajectories.

`ProbabilityBudget.evaluate` evaluates rational upper envelopes for resource
exit, missed entry, return failure and insufficient export, and **adds** them.
It uses e^(-a)<=m!/a^m and a rational upper bound for e^(1/50), so there is no
floating-point underflow disguised as zero probability. The resulting lower
bound exceeds 0.9166606; the conservative disabled upper bound is below
9.7271e-5. The paper reports the simpler 0.9 and 1/5000 guarantees. These
are evaluations of its generator argument, not probabilities estimated from
trajectories. The kernel/semigroup proof itself is not rerun in Lean here.

The budget is tied to the fixed manuscript scale, thresholds, window and
epsilon, with K in [8,12] and r in [18,22]. `applies(parameters,policy)` checks
that scope. Modified inputs are useful for exploration but do not inherit
the probability guarantee automatically. The function always returns the
fixed theorem's budget, separately from each run's applicability flag.

## Reuse and sweeps

```python
from fractions import Fraction as Q
from example import BindingReactor, ReactorParameters, OperatingPolicy, ProbabilityBudget

policy = OperatingPolicy()
for release in (18, 19, 20, 21, 22):
    parameters = ReactorParameters(K=Q(10), release=Q(release))
    reactor = BindingReactor(parameters)
    solution = reactor.deterministic(policy)
    export_per_V = solution.sol(policy.end)[6] - solution.sol(policy.deadline)[6]
    print(release, export_per_V, ProbabilityBudget.applies(parameters, policy))

# A different finite-copy exploration; the original theorem does not apply.
small = OperatingPolicy(volume=100, entry=4, floor=2,
                        deadline=5, end=10, export=8)
run = BindingReactor().stochastic(small, seed=123, limit=100000)
print(run['status'], run['event_verdict'])
```

`generator(counts,V,weights)` returns exact drift and quadratic-variation
rate for any linear observable, so new weights can be explored without
rewriting reaction bookkeeping. Add or replace a mechanism deliberately:
the current proof inequalities are specific to these channels and weights.

Seven test groups check channel removal and equilibrium consistency, exact
count support, falling factorials, symbolic identities and rational bounds,
entry/residence/deadline transitions, export boundaries and saturation,
disabled-event semantics, unfinished SSA handling, and the deterministic
enabled/disabled reproduction. No test or plot claims indefinite residence;
the paper's statement is finite-horizon and specific to this mechanism.

License: MIT is proposed, pending the owner's choice. No license grant is
asserted by this package.