Reaction-network assurance: the effective equation comes first

9 October 2026. Opportunity 013 now has a bounded, runnable model-review module with exact finite evidence. It remains a low-confidence integration for teams maintaining simulation models. The Facility Plan Auditor stays first in the commercial queue. No chemical process, customer study, source proof or profitability claim has been validated.

Source finding and its limits

A reaction network has nonnegative integer complex vectors y and reactions y->y'. Under constant positive rates, the deterministic mass-action ODE is x'=sum kx^y(y'-y). Weak reversibility means every reaction has a directed return path on the complex graph, not merely an undirected connection or a cycle in a species-interaction graph. It does not require a paired reverse arrow for every individual reaction.

The September manuscript claims a compact positive invariant polytope containing each prescribed strictly positive initial state. It gives all-time upper and positive lower bounds that can depend on that state. The October companion claims a nonempty compact convex forward-invariant set K_P in each positive stoichiometric class P=(c+S) intersect positive orthant. Every positive trajectory in that same class eventually enters this same K_P. Rates and class are fixed; entry time can depend on the initial state. The class need not be bounded. Neither general weak reversibility nor permanence asserts convergence to an equilibrium.

The selected formal scope covers the older initial-state-dependent bounds, not the newer classwise absorption conclusion. Its challenge interface excludes self-loops, uses a finite reaction set and quantifies over global solutions from one initial state. The newer paper allows self-loops, which contribute zero to the vector field. No challenge placeholder, scope link or reading record is treated as a successful proof/kernel check.

The source construction chooses a discontinuous positive tolerance, then a finite affine family, then a positive separation H, and only then a sufficiently small class scale h_P. One rate condition is h^H*sum(k)<min(k), together with a logarithmic condition on a representative c and a uniform active-label threshold. All minimizing labels must be controlled at ties. The affine proof uses compactness and a finite subcover, and the uniform activity corollary is obtained by a compactness contradiction. The reviewed construction does not provide this prototype with an explicit numerical family, usable h_P or entry-time bound.

The final permanence argument passes through successively larger scales h_next=min(sqrt(h),h_P). It uses containment of a trapping set in the next box; it does not assume the trapping sets themselves are nested. Reading these selected arguments is not a full proof review: parts of the affine induction/gluing were not reviewed, and no source construction or kernel ran. The ledger preserves precise extents. Four PDF pages were visually inspected.

What the software actually establishes

reaction_network_audit.py accepts a strict JSON definition of a small deterministic polynomial mass-action ODE. It supports eight species, sixty-four distinct complexes, 128 reactions, total complex degree eight, one MiB of input and exact rational components of at most 32 bits. Intermediate arithmetic has an 8,192-bit limit. The CLI returns unknown on that arithmetic limit and refuses an existing output directory. Original bytes and the checker hash are retained.

The input states its rate convention. For monomial coefficients, a reaction has rate k*x^y. For the factorial-scaled ODE convention, the effective coefficient is k/product(y_i!). Rates must be nonnegative constants. Exact normalization removes zero-rate reactions and self-loops, and adds coefficients of parallel reactions. It reports both the drawn graph and the effective graph. The normalized field is mathematically identical to the supplied field; omitted reactions and individual normalized coefficients remain visible. A zero initial coordinate declines the source's strictly positive initial-state scope.

Reachability, strong components, linkage classes, stoichiometric rank, deficiency, a rational conservation basis and initial derivatives are computed. A reported match to the source's effective model is conditional on the source theorem; it supplies no numerical epsilon or entry time. It does not certify a simulator, units, physical chemistry, a stochastic model, a variable-volume interpretation, external forcing, event rules or arbitrary kinetic expressions. Such extra schema fields are refused. SBML import and a live Catalyst bridge are not implemented. Julia and libSBML were unavailable in the inspected environments; no packages were installed for this batch.

Two independent conventional evidence paths provide useful finite bounds without the new theorem:

1. A supplied nonnegative conservation vector w is accepted only if it is nonzero and w dot (y'-y)=0 for every effective reaction. Then w dot x is constant. In the nonnegative orthant, every coordinate with w_i>0 obeys x_i <= (w dot x0)/w_i. Several accepted vectors can cover different coordinates. A signed basis vector alone is not an upper-bound certificate, and conservation gives no positive lower bound. This uses the standard nonnegative invariance of a mass-action field with nonnegative rates; it does not establish a physical mass interpretation for w.
2. A supplied positive rectangle is checked by exact rational polynomial enclosures on each face. The relevant coordinate derivative must be nonnegative at every lower face and nonpositive at every upper face. Substitution and aggregation happen before interval bounding, preserving cancellations on the face. These sufficient inequalities and local Lipschitz continuity imply forward invariance; compactness gives global continuation. The reported all-time bound applies to the supplied initial state only when it lies in the rectangle. It proves neither eventual entry from outside nor general classwise absorption. Failed interval checks are inconclusive, and a rectangle need not capture a source polytope.

These finite checks are ordinary graph, linear-algebra and interval methods. No implementation of the source's affine-family construction, new solver speed or independent source-proof acceptance is claimed.

Model edits that change the answer

For A<->2A with both nominal rates one, the monomial convention gives A'=A-A^2 and positive equilibrium one. Factorial scaling gives A'=A-A^2/2 and equilibrium two. In the first model, [1/2,3/2] is an invariant interval. In the second, the derivative at 3/2 is +3/8, pointing outward. Both graphs meet weak reversibility; their numerical equations differ. The Catalyst model documentation explains the factorial scaling and the option to disable it.

Setting the reverse rate to zero keeps two arrows in the supplied diagram but removes one from the effective equation: A'=A. The effective network fails weak reversibility and the positive trajectory is unbounded. Starting the logistic model at zero instead gives a zero trajectory, outside the theorem's positive initial-state hypothesis. A valid invariant interval with an initial state outside it also supplies no immediate bound or certified entry time. All these distinctions appear in separate saved fixtures.

For the source's simple 2A<->B example at rates one and state (2,8), the derivative is (8,-4). Thus the unweighted total A+B increases, while A+2B=18 is conserved. The accepted conservation vector gives A<=18 and B<=9. Independently, [1,4] by [1,16] is an invariant rectangle containing this state. The interval and conservation bounds answer different questions; their intersection can narrow the admissible state. A proposed weight (1,1) is rejected. This reproduces the paper's criticism of an earlier monomial-dominance implication without treating that gap as a refutation of the older conclusion.

The public Catalyst CRN tutorial already exposes linkage, reversibility, rank and deficiency tools. We transcribed its first eight-species, seven-complex graph, choosing nominal rates and initial coordinates one for this experiment. With explicit factorial scaling, it has two linkage classes, rank five and deficiency zero; it is not weakly reversible. Nevertheless, w=(2,3,5,4,1,5,1,4) is an exact positive conservation vector with total 25, giving finite upper bounds on every coordinate. These are a documented teaching graph and chosen parameters, not a customer process. Input, report.

An eventual import bridge must preserve equation semantics. In SBML, boundary or constant species can change which reaction-derived equations exist; changing compartment size can change concentrations even when amounts stay fixed. Official species semantics. Checking only arrows and nominal rate values would miss those differences. The current JSON checker does not pretend to have validated such an import.

Finite validation and conventional comparison

702 passing controls cover all 64 directed edge subsets on three complexes, sixty saved generated models, eleven named fixtures, invalid inputs, exact face enclosures and CLI preservation. NetworkX 3.4.2 independently supplies strong/weak components and directed reachability. SymPy 1.13.1 checks rank, nullspace span and polynomial expressions assembled from the original reaction lists. Sampled exact face values cross-check the enclosures; the enclosing arithmetic, rather than sampling, supports accepted face signs. Generated models and reports, fixture summary.

Another eleven controls compare ordinary SciPy 1.18.1 DOP853 trajectories with analytic logistic solutions across two conventions and four initial values, plus a dimer trajectory and a deliberately coarse Euler step. The largest observed logistic absolute error is below 6.29e-11. The dimer's sampled conserved-total drift is below 3.56e-15. These are floating diagnostics, not validated numerical enclosures or rigorous continuous-time simulation error bounds. The exact invariant/conservation checks remain separate.

At A0=3, one explicit Euler step of size one on A'=A-A^2 gives A1=-3, despite a separately verified positive invariant interval containing A0. That deliberately coarse method failure is not a theorem counterexample or a critique of a properly configured production solver. Full inputs, budgets, analytic comparisons and trajectories.

The shaded dimer rectangle is independently invariant, the dashed line is its particular conservation class, and the curve is a floating trajectory. The curve does not establish invariance. All 713 new controls pass; archived tools and original fixtures are preserved in the artifact manifest. No source proof, actual simulator import, physical validation or industrial regression study was executed.

Commercial decision

Potential buyer: a modeling team whose reviewed models repeatedly move between parameter conventions, simulator versions and external file formats. A useful integration would retain exact normalized equations, source scope, accepted finite witnesses and edit-by-edit differences alongside existing simulation reports. Existing libraries already provide the basic graph analysis, symbolic algebra and integration; those capabilities alone do not justify a separate product.

The earlier AUD 3,000-12,000 integration hypothesis remains unvalidated. An illustrative AUD 7,500 engagement with thirty hours at AUD 180/hour leaves AUD 2,100 before support and overhead; fifty hours cost AUD 9,000 in labor alone. Actual demand, avoided-error value and delivery time are unknown. Before a standalone plugin, implement and verify one useful real import path, establish a permissioned recurring model-review problem, and measure how many material errors this catches beyond the team's current stack. Defer broad numerical permanence construction and process-safety claims. Keep this as a specialist evidence-platform module below facility planning.