# Certifying fresh microbial conversion from finite records

Companion to manuscript 62, SHA-256 `e6e69d291896c7e93c96d47920557c1a1eb16bd3f6c15c83c5697207f75f45df`. Python 3.11+. The material and certificate modules use only the standard library; pinned plotting dependencies generate the supplied figures.

```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
```

## What is being certified

All amounts refer to one **original aliquot**, not its retained volume or surviving cells. Mobile product P is physically available for collection. Convertible reserve R includes every other old material capable of contributing to the credited output, at conservative product-equivalent yields: intracellular intermediates, mobilisable biomass, sorbed material and alternative nutrients cannot be omitted just because they are difficult to measure.

Fresh F means entry into this declared credited inventory during the two windows. It can enter intermediates rather than immediately becoming collected product. The result does not attribute atoms to a particular substrate, establish viability or growth, give a per-cell rate, or predict future function. A zero lower bound means unresolved, not inactive or dead.

For one window, fresh addition is followed by reserve release U, mobile uptake T, collection Q and losses DP,DR. `Window` validates the three availability constraints before construction. Its event replay checks both pools and exact conservation after every operation. `Recovery` declares separate upper retention maps e<=s and explicit material inputs. `History` checks that the second window's initial pools fit those maps; any unretained material is excluded from the two credited collections.

The certificate uses lower collection bounds q1,q2 and upper bounds on initial total B, pre-wash reserve J and recovery input H. It is the maximum of

`0, q1-B, q1+q2-B-H, e*q1+q2-e*B-(s-e)*J-H, s*q1+q2-s*B-H`.

These five expressions come from fixed nonnegative combinations of material inequalities; the code is not a general verified linear-programming solver. The equivalent remaining-stock form is

`[q1-B]+ + [q2-H-e*x-(s-e)*min(J,x)]+`, with `x=[B-q1]+`.

This shows the adversary's strategy: satisfy the unavoidable first deficit, store as much remaining stock as allowed in the better-retained reserve pool, then add fresh material only for the remaining second deficit.

## Reusable components

* `material.py`: immutable `Window`, `Recovery`, `History`; exact event replay; an explicit attaining construction for any admissible initial split; bounded volume-times-concentration error propagation.
* `certificate.py`: separate `DirectReserve`, `UptakeBound` and `UnboundedReserve` premise types; `MaterialCertificate` with all active expressions, remaining stock, sensitivity and an attaining history; `Observation` and a reporting wrapper retaining unresolved/incompatible outcomes.
* `example.py`: editable inputs first, configured reports, exact histories, fixed manuscript counterexamples, matched design comparisons, sweeps and reproducibility metadata.

```python
from fractions import Fraction as F
from certificate import MaterialCertificate, UptakeBound, Observation, report
model = MaterialCertificate(F(10), F(1,20), F(9,10), F(1,5),
                            UptakeBound(F(2), F(1,10)))
record = Observation(F(6), F(4), F(1,5), F(1,5))
print(report(record, [model], F(8,5)))
history = model.witness(*record.lower_collections())
for step in history.ledger():
    print(step)
```

Use `Fraction`, integers or exact decimal/rational strings for material inputs. No rates are fabricated: this is a finite material model, and its attaining histories need not be kinetically achievable by a chosen organism in a chosen duration. Adding validated kinetic or joint measurement restrictions narrows the feasible history class and may strengthen the lower bound. The existing exact minimum remains sound but need not remain attainable in that narrower class.

## Distinct reserve premises

`DirectReserve(J)` means an actual upper bound on R immediately before recovery. Initial reserve is not interchangeable with it: mobile product can be taken up during window one and become better retained. The explicit counterexample starts at P=8,R=2, takes up 2 and collects 6, ending at P=0,R=4. After e=.05,s=.9, it collects 3.6 with **zero fresh input**. Incorrectly inserting J=2 returns a false lower bound 1.7; inserting J=4 returns zero. `valid_for` rejects the wrong direct premise for this history.

`UptakeBound(Rbar,Tbar)` records a bound on initial reserve plus **gross cumulative first-window uptake**. It evaluates the same expressions with J0=Rbar+Tbar, but its proof uses `prewash reserve <= J0+F1`, not `prewash reserve <= J0`. The unknown first-window fresh term is harmless because s<=1. The interface preserves that distinction, including a test where actual pre-wash reserve exceeds J0 while the uptake premise remains valid. An attaining history chooses initial reserve min(Rbar,B) and satisfies the uptake cap exactly as required.

A calibrated maximum uptake rate times a valid biomass/time bound can supply a cumulative cap. Net extracellular disappearance cannot: simultaneous release can conceal gross uptake. The target chemical inventory and all unit conversions must match. With initial reserve bound 2 on the worked record, an uptake cap <=9/85 certifies 1.6; a cap <1/5 strictly beats the unwashed bound.

`UnboundedReserve` retains only the information available without a reserve restriction. It sets the effective parameter at the remaining-stock saturation point, yielding the reserve-free maximum. Both direct and uptake premises may be supplied to `report`, which takes the maximum of sound lower bounds. Individual classes have explicit witnesses; this does not assert joint feasibility under arbitrary combined premises or correlated calibration bounds. That compatibility problem must be checked separately.

## Exactness and observation behavior

`attaining_history` accepts any initial reserve in [0,B] for the direct class. It constructs first-window fresh amount `[q1-B]+`, final reserve `min(J,[B-q1]+)` and the necessary release or uptake. Recovery uses the full allowed input H in reserve. The second window adds only its unavoidable deficit and accounts for any leftover material as losses. All availability inequalities, both terminal pools and every ledger step are verified with exact rational arithmetic.

The default run replays 3,316 degenerate-grid and seeded rational histories, including e=0, e=s, s=0, unit retention, zero stock and collections above initial stock. This is a computational audit of the formulas and constructor, not a replacement for the general theorem. The seven scientific test groups additionally check event ordering, the storage counterexample, uptake semantics, strict/inclusive decision boundaries, wash cancellation and amount errors. Lean is not rerun.

Observation errors are deterministic simultaneous bounds. Lower collections are max(0,y-epsilon). Negative reported values remain compatible if their intervals include zero; an interval entirely below zero is incompatible. A report is:

* **at or above** when the lower bound reaches the target, including equality;
* **below** only with an independently justified fresh upper bound strictly below the target;
* **incompatible** if lower exceeds that upper bound or an output interval is entirely negative;
* **unresolved** otherwise.

Low output does not supply a fresh upper bound: `extra_unobserved_formation` adds arbitrarily much fresh material and matching reserve loss without changing collections or the direct premise. The saved example adds 100 equivalents to the same record.

For a measured export V*c, the allowance is `abs(Vhat)*eps_c + abs(chat)*eps_V + eps_V*eps_c`. The example 2 mL times 3 micromol/mL, with .05 mL and .1 micromol/mL errors, gives .355 micromol. Sum allowances for distinct exports and separately account for dilution, recovery, subtraction and normalization. Shared bias does not average away. No confidence level is attached here. If an external simultaneous calibration event has coverage 1-alpha, an erroneous issued claim is contained in its failure event; this does not automatically bound error conditional on issuing a claim.

## What washing buys in the worked source

The fixed manuscript reference starts at (8,2), selectively collects 6 and leaves (2,2), with no first-window fresh input. Washed recovery gives (.1,1.8); fresh input 2.1 and reserve release 3.9 permit collection 4. The matched unwashed arm retains (1.8,1.8), receives the same fresh input and collects 5.7. This first collection is a selective product separation, **not** a homogeneous 75% withdrawal that somehow leaves all reserves and cells behind.

Both protocols use B=10,J=2,H=.2 and two amount errors .2. At the manuscript's principal target **1.6**, the washed result is 1.69 and at-or-above; the unwashed result is 1.52 and unresolved. The unwashed **two retention expressions** tie at 1.52; the total-inventory expression is 1.1. This explicitly follows the arithmetic rather than the inconsistent “total / retention” label in the paper's comparison table. The older companion calculator's default 1.5 is not used for this comparison.

At a matched source, changing e changes Q2 too. The exact zero-error certificate remains 1.90 as e varies; holding Q2 fixed while lowering e would manufacture a benefit. With first-window uncertainty, the gain in the reserve-sensitive regime is `(s-e)*(epsilon1-(J-r))`. For a tight reserve ceiling it is .85*.2=.17. Reserve slack consumes the same margin. Active-expression advice depends on the inputs: when e=s or J stays above remaining stock, tightening J locally buys nothing.

The fixed reference family with additional activity a in [0,1] and reserve slack delta>=0 has `L=max(0,2.1*a-.41-.85*delta)`. Activity is relative to the already-sampled unwashed comparator, not inferred from material retention or charged a second time. Strict improvement over 1.52 requires `a>193/210+17*delta/42`; meeting 1.6 requires `a>=67/70+17*delta/42`. At delta=.2 no admissible activity strictly improves the comparator. At a=.9,delta=0 the washed certificate is 1.48 and loses. These are requirements of a declared constant-capacity response family, not measured wash performance.

Three reserve goals are distinct: positive certification needs J<339/85; meeting 1.6 needs J<=179/85; beating 1.52 needs J<11/5. The figures and saved sweeps retain the strict/equality distinctions.

## Accounting scope and outputs

Declare every carbon-bearing input once: old stock, fresh entry, recovery input or another bounded source. An unreacted challenge outside the credited pool may become fresh entry; it cannot also be charged as old stock for the same event. A homogeneous sample obeys `V*c=(V-v)*c+v*c`; the removed amount is collected once, and the retained amount remains in the state. Wash waste is separate. The stoichiometric C/H/O check for the paper's lactate/acetate witness is only a balanced material possibility, not an organism-specific pathway, thermodynamic feasibility or atom mapping.

The two illustrative durations produce a lower bound on average credited-inventory generation across their combined elapsed window time. No steady-state interpretation or per-cell normalization is added. The record says nothing about future conversion, and the positive reference has F1=0, so it cannot demonstrate recovery relative to a proven positive first-window function.

JSON outputs preserve exact fractions, expressions, witnesses, provenance and interpretation. CSVs expose the reserve/activity sweeps; figures compare the same-source histories and design budgets. All default quantities are synthetic and no biological calibration or clinical use is asserted.

## 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.
