# Exact common-activity compatibility and finite cycle acceleration

Example for manuscript 73, SHA-256 `cdd3d14f5f78c6d309b35c7702b8379750fe5df5b5b08ec8e76bf80d3b9336ab`.

The object is an oriented graph of two-reaction cores. Every graph vertex has one activity, shared by all incident cores. A feasible state makes **both endpoint productions positive in every core separately**. The example teaches the paper's forced-root mechanism and supplies exact reusable feasibility tools, while explicitly distinguishing the implemented backend from the paper's complexity-guaranteed algorithms.

## Run and configure

Python 3.11 is tested. Create an environment and install the pinned dependencies:

```sh
python -m venv .venv
# Activate .venv for your shell.
python -m pip install -r requirements.txt
python example.py
python -m unittest -v
python example.py --output replay
```

Edit the inputs at the top of `example.py`: module count, kinetic factors, independent boxes, fixed margin, factor/activity uncertainty, finite-grid resolution and computational budgets. Rational strings avoid binary-float ambiguity. Defaults give a three-triangle windmill with one shared hub. The canonical source examples are always replayed separately from the edited assembly.

For a new graph, construct `ActivityProblem(boxes, cores)`. Every endpoint must have an `ActivityBox`, and the underlying graph must be simple with one orientation per edge. Loops and duplicate/reversed parallel edges are rejected. Boxes satisfy `0 < lower <= upper <= 1`, including singleton boxes. Factors and demand weights are strictly positive.

```python
from fractions import Fraction as F
from activity import ActivityBox, Core, ActivityProblem
from solver import CycleAccelerator, strict_decision, round_down

problem = ActivityProblem(
    {'A': ActivityBox(F(1,10), F(9,10)),
     'B': ActivityBox(F(1,100), F(9,10))},
    (Core('A', 'B', F(2), F(1)),))
print(strict_decision(problem))
solver = CycleAccelerator(problem, F(1,100))
result = solver.solve()
if result['status'] == 'feasible':
    solver.audit_least(result['state'])
    print(round_down(problem, result['state'], F(1,100)))
```

Solver results can be `feasible`, `infeasible` or `unknown`. A timeout, unresolved algebraic comparison or exhausted jump/root budget returns unknown. It is never converted to incompatibility. Extremely complicated algebraic numbers can still be expensive; no practical runtime bound is promised.

## Source model and reusable layers

For one core `u -> v`, write `x=x_u`, `y=x_v`, with food activity one. Its currents are `p=a(x-y)` and `q=b(y-x^2)`; its endpoint productions are `2q-p` and `p-q`. `Core.currents` returns each separately. `ActivityProblem.total_accounts` sums food and species production only as an **additional account**, after preserving all per-core constraints. An exact counterexample in the output has positive aggregate production for every species while its unit-factor shortcut triangle is incompatible per core.

`Core.lower` and `Core.upper` implement the monotone response band:

```text
G(x) = (rho*x + 2*x*x)/(rho+2)
F(x) = (rho*x +   x*x)/(rho+1)
G(x)+t <= y <= F(x)-t.
```

The normalized margin differs from a production rate. Positive `lower_weight` and `upper_weight` replace the two margins by weighted demands. For a physical tail/head demand `(w_u,w_v)`, use weights `w_u/(a+2b)` and `w_v/(a+b)`. Zero weights are outside this implementation's assumptions.

`ratio_lower` and `ratio_upper` encode **one activity vector for all ratio realizations**. The robust lower band uses the upper ratio and the upper band uses the lower ratio. Independent relative factor error `r` produces ratio endpoints `rho*(1-r)/(1+r)` and `rho*(1+r)/(1-r)`. `Core.uncertain_factor_activity_minima` separately computes production-magnitude minima over a declared activity/factor box, after verifying the positive-current conditions that justify its corner formula.

## Implemented cycle mechanism

`CycleAccelerator` implements the synchronous label-correcting control flow of Algorithm 1 at a declared rational margin. Each label consists of an anchor and a simple implication path. If extending a violated implication would revisit a vertex, the resulting rooted cycle is detected. The solver seeks the least fixed point **strictly above the current label**, inside the root species' upper box. Intermediate transport values are constrained to be nonnegative to select the correct inverse branch; they are deliberately not constrained by species boxes, because later overflow tests handle those.

Every accepted root is checked against the complete cycle map. Only its anchor is raised. All transported labels are recomputed from anchors after a jump, preserving the paper's distinction between root seeds and derived values. The JSON trace records each cycle, pre-jump value, cycle image, root, phase and final simple-path ancestry. A separate full-system algebraic query checks both feasibility and the absence of any feasible state with a smaller coordinate. Thus a returned weak-margin state is the least one, and minimizes every coordinatewise nondecreasing inventory at that margin.

The arithmetic backend uses Z3's exact quantifier-free nonlinear real arithmetic, including algebraic numbers. Cycle roots are selected by repeatedly excluding roots at or above the current candidate until the remaining query is unsatisfiable. There are finitely many admissible roots for a violated analytic cycle; a user budget can interrupt this process with unknown. This backend may combine algebraic fields and does not have the paper's projected-comparison complexity guarantee.

The unit example at `t=1/100` reaches `(alpha,alpha-7/100)` with `alpha=(5-sqrt(13))/10` in one jump. Its coordinates are irrational. Ordinary cycle iteration approaches alpha without attaining it; the plotted floating-point sequence is only an illustration. `round_down` performs exact dyadic comparisons and one-sided rounding, preserves singleton boxes and independently rechecks a rational witness at at least half the original margin. That witness is not claimed to attain the original weak margin or its least inventory.

## Strictness, capacity and elimination

`strict_decision` submits the complete strict polynomial system to the general exact backend. A feasible algebraic state is converted to a positive dyadic margin and then an independently checked rational witness. Unsatisfiability decides strict incompatibility, including the diamond that is feasible at margin zero but incompatible at every positive margin. This is **not** an implementation of the paper's positive-infinitesimal trace/CAD algorithm, and trying successively smaller margins is not used as an infeasibility proof.

`capacity_bracket` uses exact weak-feasibility queries to bracket a nonnegative optimum. If zero margin is infeasible, it reports that fact without claiming to compute the negative optimum. If there are no edges, margin capacity is unbounded. The unit edge gives exactly `1/48` at `(1/2,17/48)`; the universal unweighted ceiling is `(3-2*sqrt(2))/8`, not attained by rational ratios. Bisection on the margin is valid; bisection on an arbitrary species coordinate generally is not.

`ClosedUnionNext` implements the least admissible value at or above a request for a finite union of rational closed intervals. Its abstract example keeps the gap between `[.1,.2]` and `[.6,.8]`: a request `.3` jumps to `.6`, so an outgoing cap `.4` cannot be met. Replacing the set by its interval hull would invent a solution. This example demonstrates the elimination lemma, without claiming that this particular union is the projection of the default triangle.

`GridElimination` is a useful exact finite-domain specialization of Algorithm 3. All points and tests are rational; maps are rounded upward to grid indices, next-maps retain every admissible grid point, vertices are eliminated in DFS postorder, and the least grid state is reconstructed backwards. Tests compare it with exhaustive lattice search. A returned grid witness is also real-feasible after exact checking. **Grid infeasibility does not imply real infeasibility**, and the least grid point need not be the real least point. The full continuous envelope construction, projected CAD, positive-infinitesimal execution and FPT implementation are not provided or benchmarked. The paper itself presents those as algorithms and conventional complexity proofs, not as a benchmarked complete solver.

## Chemical certificate and scaling

The canonical triangle has factors `(2,1),(2,1),(1,1)` and state `(.1,.065,.043)`. Its smallest normalized residual is `209/120000`; its sharp fixed-state independent factor radius is `19/301`, with strict positivity only below that radius. At 5% factor uncertainty the fixed-state minimum is `869/800000`. Allowing independent activity errors of `1/10000` as well gives the exact joint-box minimum `1175221/2000000000`, by monotonicity over the whole box rather than sampling.

Each module consumes food `5071/40000` and contributes hub production `49/1000`. Replicating modules preserves one common hub activity and every local certificate. For at least two modules the longest undirected simple path has four edges, while food demand grows linearly. Dividing all factors by the module count preserves the response bands and constant aggregate food demand but divides each production residual by that count. Structural tractability does not remove resource costs.

With reference concentration 1 mM and reference flux 1 mM/min, nominal concentrations are `(100,65,43)` micromolar, activity tolerance is 0.1 micromolar and the certified joint-box production floor is about 0.5876 micromolar/min. These are an explicitly stipulated normalized model, not measured kinetics. Food and internal species must have compatible elemental composition/charge for the channels to be chemically meaningful. Static instantaneous productivity establishes neither a steady state nor persistence.

## Evidence and files

`paper_checks.py` wraps the supplied `check_paper.py` in a callable replay without changing its calculations. It rechecks response identities, the exact unit jump, policy omission, the identity diamond, the shortcut obstruction, graph/path examples, capacity, robustness, module arithmetic and order-d identities for d=2..6. The reusable cycle solver itself covers order two. `source_provenance.json` records the original hash and adaptation.

Outputs include source-identity checks, exact cycle/root ancestry, an independent leastness result, policy and zero-margin counterexamples, strict and robust decisions with rational witnesses, finite-grid elimination, an aggregate-production counterexample, continuum uncertainty minima, food accounting, capacity brackets and two PNG/SVG figures. Exact algebraic values use Z3 root-object expressions; accompanying decimals are display approximations.

Seven tests check the irrational jump/leastness/rounding, omitted policies and singleton boxes, strictness and aggregate-production distinctions, grid elimination against exhaustive lattice enumeration, uncertainty endpoints/corners/tolerance, weighted capacity and min-closure, and unknown budgets/invalid graphs/food conservation. The positive witnesses are checked with rational arithmetic independently of the backend. Negative algebraic verdicts trust the pinned solver; no proof-assistant certificate is exported. Lean is not rerun, and no end-to-end verified solver is claimed.

License: MIT is proposed for new example code, pending the owner's choice. No license grant is made here; attribution does not settle the supplied paper code's licensing.