# Reliable covalent export under driven cleavage

Standalone model and certificate evaluator for *Reliable covalent export from an autocatalytic reactor under driven cleavage: explicit finite-copy operating, output and supply certificates over an exponential horizon* (14 September 2026). Original PDF SHA-256: `b03c9193c19090688e71a36a46ad31bf33dc9bde1d910c5b0cf3615ae803b05e`.

The six-species reactor ligates foods U and W into a covalent template X. Reversible binding produces complexes C1 and C2; templated ligation produces duplex Z; duplex release yields two free templates. A maintained-drive cleavage pair competes with this cycle by returning X to its food components. The paper proves a joint finite-copy event: startup, resource retention, catalytic residence, output in every completed unit window, and gross food/driving budgets, all on the same continuing trajectory.

## Run and change inputs

```sh
python -m pip install -r requirements.txt
python -m unittest -v
python example.py --output outputs
```

Python 3.11 or later is required. Inputs at the top set copy scale V, equilibrium bias K, duplex release r, driven cleavage delta, post-startup duration H, failure target, dimensional scales and the optional simulation budget. The baseline is `V=100000000`, `K=10`, `r=20`, `delta=1/20`, `H=100`. Basal epsilon is fixed at `1/500000000` by the theorem; changing it exits the probability certificate's scope.

Outputs include exact bookkeeping/coefficient checks, outward interval evaluations of the probability expressions, sufficient copy scales, a physical-unit translation, deterministic density trajectories with eight ledgers, per-window exports, CSV sweeps, PNG/SVG figures and hashes. Default results reproduce a joint success lower bound **0.923849223293379...**, the simpler lower bound **0.729329433526774...**, and a disabled upper bound below **10^-21699**.

The default failure target is 0.01, so V=1e8 does not pass that target. The geometric search individually verifies V=194871710 as sufficient using the full expression; the simpler rule gives V=264915869. Neither is claimed to be the minimum.

```python
from example import Parameters, DrivenReactor, ObservationPolicy, ProbabilityBudget

p = Parameters(K=8, release=18, delta='1/100')
model = DrivenReactor(p)
print(model.generator([10**8,10**8,0,0,0,0], 10**8, (0,0,1,0,0,0)))
certificate = ProbabilityBudget(V=200000000, H='48', parameters=p)
print(certificate.interval_pass('0.01'))
print(certificate.evaluate())
```

## Literal count model and reusable components

`Parameters`, `Channel` and `DrivenReactor` separate coefficients, labelled transitions and reactor dynamics. The enabled source has exactly twenty labels. The disabled source removes **only labels 6 and 7**, the templated ligation pair C2 <-> Z; all other labels retain their identities, rates and marks.

`Channel.count_rate` uses falling-factorial counts and the copy-scale factor `V**(1-reactant_order)`. In particular, the association `2X -> Z` has rate `r*x*(x-1)/V`, with no extra factorial divisor. Inputs to the count API must be nonnegative integer counts and positive integer V. `rates(state)` without V instead supplies deterministic concentration monomials; the distinction between a count model and its density-limit ODE is explicit.

Labels 18 and 19 have the same six-species jumps as basal cleavage and ligation, but different coefficients and independent service marks. Reservoirs F and P are externally maintained activities absorbed into those coefficients; they are not additional finite species. The eight ledgers are covalent export, two food inputs, two driving directions, two moiety washouts and total washout mass.

The resource weights are `A=(1,0,1,2,2,2)` and `B=(0,1,1,1,2,2)`. Weighted catalytic count is `Y=X+(9/8)C1+(7/5)C2+(9/5)Z`. Resident mass is `M=2(A+B)`, whereas covalent stock is `S=4X+4C1+4C2+8Z`. A complex can carry unligated food; that food contributes resident mass but is not exported covalent product. Cleavage is not export. Gross driving service is `QF+QP`, never the net difference.

The monitor audits both moiety balances and `M+washed_mass=4V+2*IU+2*IW` after each supported event. Basal and driven channels remain distinct even when their state changes coincide. Opposite driving events can cancel in the chemical state while still adding two service events.

## Observation schedule and endpoint semantics

`ObservationPolicy` fixes the source event: initial food-only state `(V,V,0,0,0,0)`, resource corridor `0.9V<=A,B<=1.1V`, entry into `Y>=V/2500` by time 500, and no subsequent return to `Y<=V/5000` through `500+H`. Every completed window `(500+i,501+i]` must export at least `V/5000`. The final fractional interval has resource, residence and supply requirements but no extra output threshold.

`OperatingMonitor` retains a single chemical state, entry phase, persistent all-window pass bit and cumulative supplies. At window boundaries it resets **only** the export measurement. A failed output window stays failed even if a later window passes; chemistry can continue. Reaching an export cap never suspends residence or resource checks. Entry exactly at time 500 is allowed. A reaction at a window's right endpoint is assigned to that window. A return exactly to the residence floor fails.

Each supply counter is capped at `ceil(2*V*(500+H))+1`, strictly above all relevant thresholds. The implementation keeps natural counters too and checks their agreement with capped counters. Pair-sum budget violations survive saturation. First resource-exit states are retained, not clipped back into the corridor. The disabled monitor requires only the same output schedule and credits every resource exit as a possible success, matching the conservative comparison; it imposes no entry, residence or supply requirement.

Optional direct count simulation uses:

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

The simulation has a fixed event budget. At V=1e8 even food turnover makes a full direct path expensive; an unfinished path returns `event_verdict=None`, not failure. Event holding times and choices use numerical random sampling. The direct sampler requires V<1e12, and the path monitor limits the number of explicit windows. These are computational limits of this example, not physical failure events. The separate probability interface supports far larger durations without enumerating windows.

## Probability expressions and sufficient sizing

`ProbabilityBudget` checks the published domain: integer V>=1e8, K in [8,12], r in [18,22], delta in [1/100,1/20], fixed epsilon and H>=1. It evaluates all nine error components in logarithmic arithmetic: missed entry, startup clock, initial/resource leakage, initial/return leakage, all-window output, two food budgets and gross service. **They are added on one law.** Startup and shared failures are paid once; only the pointwise window error is multiplied by floor(H). Independence between windows is neither assumed nor simulated.

The full finite-duration formula applies to any H>=1 in the model domain. The simplified `1-2*exp(-2e-8*V)` is exposed only after an outward interval check confirms `log(H)<=V/1e6`. The exponential horizon is reported by its logarithm; no astronomical window list is created. The finite-duration disabled bound is reported for integer H, exactly the stated finite-duration theorem; fractional H receives no improvised comparator formula.

The mpmath `iv` calculations enclose logarithms and sums outward at 70 digits. `interval_pass(rho)` compares the upper log-error endpoint with the lower log-target endpoint. The sufficient-size search checks each bounded geometric candidate individually; it does not assume global monotonicity or return an alleged optimum. The simpler closed rule is rounded to an integer and its two logarithmic requirements are rechecked outward. Numerical interval evaluation is a separate layer from the paper's Lean-verified finite-kernel statements.

The saved algebraic certificate recomputes resource drift, catalytic drift, per-label mass and moiety bookkeeping, the disabled stock/export identity and rational low-density coefficient slack. The test suite additionally checks growth/noise estimates at several box-edge parameter choices and integer low-count states. This is useful regression evidence, not a fresh general proof of all generator, kernel-composition or infinite-state identification steps.

## Output, supplies and dimensional interpretation

`ProductionLedger` reports consequences conditional on the joint event. At the default settings each unit window exports at least 20000 model mass units, or 5000 covalent X equivalents; all 100 completed windows export at least 2 million mass units. Each food input is bounded by 120 billion events over the full 600 time units, and gross driving is bounded by 7.5 billion events. Inventory remains between 3.6V and 4.4V, whereas cumulative replenishment scales with duration.

The expected completed-window export is bounded below by the guaranteed output times the event probability lower bound; the program records the ordinary high-precision evaluation of that consequence. For an interval of length L contained in the completed-window span, `aligned_interval(L)` gives `V/5000 * max(0,floor(L)-1)`. In particular, every contained interval of length two gets at least one certified window's output; the original unit-window threshold is not asserted for every sliding unit interval.

At reference concentration 1 micromolar and dilution 1/hour, V=1e8 corresponds to about 166.054 pL, the startup allowance is 500 hours, and the conditional equivalent-product concentration rate is at least 50 pM/hour. These are unit translations, not measured productivities or a calibrated operating protocol. Export includes covalent templates carried in complexes and duplexes; dissociation, purification, recovery losses and activity must be modelled before calling it free active product.

Reservoir consistency requires affinity `log(K/eta)=log(8e9*K)` in units of kBT. The program also translates it to kJ/mol at a chosen temperature. Gross driving times this affinity bounds absolute service work exchange on the successful event, but does not price food work, separation, apparatus power or total entropy production. Finite autonomous reservoirs would require a different model.

## Deterministic illustration and verification

The density-limit ODE carries the same reaction and observation labels with continuous ledgers per V. It compares enabled and disabled trajectories and reports exports separately for every complete window. A second stiff solver checks the numerical solution, and the source balances check its ledgers. Continuous basal production can seed the ODE immediately; finite-copy startup is an immigration event. The ODE curves therefore cannot estimate the stochastic startup probability or replace its certificate.

Seven test groups cover labels and falling factorials, exact identities and low-count estimates, deadline/window/final-fraction semantics, return equality, supply saturation, disabled credit, unfinished paths, interval bounds and sizing scope, independent solver agreement, output geometry and dimensional conversion. The paper's finite-kernel theorem is formally verified upstream; this package does not rerun Lean. Nonexplosion and identification with the literal infinite-state process are conventional arguments in the paper. Exponential finite horizons do not imply perpetual survival at fixed V.

Licensing: MIT is proposed, pending the owner's decision. No new license grant is made by this example.