# From an ACR candidate to a conditioned concentration guarantee

Absolute concentration robustness (ACR) means that a species has the same concentration at **every positive steady state**, even across different conserved totals. It does not mean the same concentration at every time, and a list of algebraic candidates is not an ACR decision. This example connects the paper's algebra to reusable full mass-action models and quantitative operating checks.

## Run and edit

Tested with Python 3.11. Install `pip install -r requirements.txt`; run `python example.py` and `python -m unittest -v`. `python example.py --output replay` writes a separate output set. The default run takes seconds. Edit the driver’s top inputs: five reactor rates, dilution, feed, load, required multiplier pool, derivative residual, uncertainty, initial displacement, EnvZ rates/totals and release/leakage rates. Rational strings preserve exact arithmetic. Concentrations are micromolar and time is minutes; bimolecular rate constants have units micromolar⁻¹ minute⁻¹. These are the paper's illustrative scales, not fitted biochemical data.

`Reaction` and `MassActionModel` construct the literal deterministic fluxes, vector field and Jacobian; 2B→empty uses κb² and changes b by −2κb². `LoadedReactor` adds feed, dilution and load to the full three-species chemistry. `EnvZOmpR` supplies all nine reactions and seven species. `PrivateRelease` replaces a reaction's product side with private intermediates. Algebra and certification live separately in `BlockCandidates`, `ResidualCertificate`, exact `Interval`, and `InvariantEllipsoid`. There is no shared framework required by other papers.

## Three sets that must not be confused

The first bimolecular counterexample has positive steady states (2,τ,τ), so a is ACR at 2, but the quotient algebra also sees a boundary branch at a=3. The block candidate list is {2,3}. The second has the positive curve (τ,τ,τ²,τ²), hence no ACR, yet the isolated nonpositive point (1,−1,1,1) supplies the sole zero-divisor candidate 1. The exact source replay checks the identities and quotient arguments' algebraic fixtures. We do not use a numerical positive root search to assert absence of other positive branches.

The monomial-order comparison recomputes the mixed-order basis {u²−v²,ut−v,vt−u}, whose z-leading coefficients return no positive candidate despite ACR t=1. Lexicographic u>v>t is an explicit block order and returns 1. `BlockCandidates` uses the **original** steady-state ideal: no radical, saturation, or conservation equations are silently added. It returns exact algebraic roots, not an automatic ACR verdict. The paper's completeness theorem covers zero-divisor values. A positive steady state with Jacobian rank equal to stoichiometric rank additionally guarantees ACR coverage; this is checked on the full EnvZ field. Neither statement turns a candidate into ACR, and there is no claimed complexity bound or universal ACR solver.

## A loaded reactor that keeps its setpoint while losing its margin

The default reactor has the positive equilibrium (a,b,c)=(2.2,1.7,1.7). Its exact setpoint is α=(k2+k3+D)/k1. Positive operation requires Δ=k5+D−k4α>0 and N=cin−α(1+ell/D)>0. Then b= rN/(1+r), c=N/(1+r), with r=Δ/k3. All three Routh coefficients and their strict stability margin are checked exactly along the load sweep. This establishes local stability, not global attraction.

Load on A leaves α unchanged but consumes the multiplier pool b. The positive branch ends at ell=39/1100 per minute, while the specified b≥1 floor ends earlier at 29/1100. The identity (a−α)k1 b = b' gives |a−2.2|≤0.02 micromolar if b≥1 and |b'|≤0.001 micromolar/min. A concentration measurement error does not supply this derivative bound.

`ResidualCertificate` verifies the polynomial identity exactly, encloses the multiplier and coefficient polynomials with rational intervals, and simplifies the **signed** disturbance q·d before bounding it. An added A-only load cancels in this certificate; a direct b-load does not. The output distinguishes `invalid_identity` from `unresolved_multiplier_floor`: interval dependency or a domain reaching zero may prevent confirmation without refuting the requested floor. Residual and load assumptions remain explicit. A small-residual counterexample holds a−α=1 while b→0, demonstrating why the floor cannot be discarded.

The ±1% parameter-box calculation gives α∈[218/101,74/33] and b*≥15415907/10428000>1.47. It is an exact enclosure, not a corner sample. Setpoint uncertainty must be added to an error around a nominal value. These are equilibrium floors, not floors at arbitrary states having the same parameters.

The nominal ellipsoid provides a stronger, local trajectory statement. Fresh rational checks verify P>0, JᵀP+PJ=−I, the nonlinear cubic remainder, coordinate bounds and V≤1/5. Inside it, b≥1.573 for all future time. The default initial displacement is checked exactly for membership, then Radau and BDF trajectories are compared as illustrations. Changing rates or load invalidates this particular certificate unless its checks pass again; the program reports non-applicability. It proves neither entry from arbitrary initial conditions nor robustness to time-varying loads. The advertised 0.045 ball is separately checked at the requested ellipsoid level.

## EnvZ/OmpR and private release

The seven-species EnvZ model retains both protein-pool conservation laws. Its positive steady state exists for Xtotal>0 and Ytotal>α, and the exact quadratic determines it uniquely. The full raw Jacobian has rank five at the constructed positive state; the source replay also verifies the symbolic minor valid at every positive state. All nine rates in [0.99,1.01], Xtotal∈[1,2], Ytotal∈[4,5] yield the paper's exact x2 floor 9121780899/77264239204>0.118. The two certificate gains differ under independent interval bounds although they coincide when exact equilibrium correlations are retained. The driver demonstrates both on a **separately declared measured-state box**; it never uses equilibrium-only floors to certify the illustrative transient.

The release example uses A+B→3B, B→A, B→empty. Its positive steady states have a=1, b>0. Replacing the first reaction by A+B→Z1, Z1→B+Z2, Z2→2B gives the same original steady-state equations after exact substitution zj=ab/λj for any positive release rates. The transported identity is (a−1)b = new_b'/2 + 3Z1'/2 + Z2'. Old-species residuals alone miss those extra terms. The code compares the block candidates before and after release, computes material storage with unit and cargo weights, and integrates the complete extended model.

Leakage reduces each stage's yield by successive factors λ/(λ+δ). In this particular illustrative network, any nonzero leak actually destroys the positive steady state: the A balance forces a=1 and the B balance then has a strict deficit. The leakage result explicitly reports this; a conditional concentration-defect formula is not an existence proof. Product release does not generally preserve trajectories, stability, conserved totals or thermodynamic properties, nor does it reduce a super-bimolecular reactant complex. Private intermediate names and rate signs are validated.

## Evidence and limits

Outputs contain exact candidates/bases, reactor operating and floor limits, source-check report, accepted/rejected/inconclusive certificates, the rational Lyapunov evidence, parameter boxes, EnvZ states and pool checks, release identities/costs, complete species trajectories, figures and hashes. All assertions in the source checker are freshly executed in symbolic/rational arithmetic. New trajectories are numerical and compared where stated. `source_provenance.json` records the source checker and its execution-wrapper change. Lean is not rerun; the paper distinguishes its compiled algebra from conventional geometry, existence and dynamical arguments. No newly run formal proof is claimed.

MIT is proposed for newly authored example code pending the owner's license decision. This README does not grant a license.