# Screen literal networks for productive autocatalytic cores

The input consists of two nonnegative integer matrices. A row names a species; a column names one reversible reaction identity. L records what is literally on the reactant side and P what is literally on the product side. N=P−L records net change, but it does **not** replace the two literal matrices: A→2A has both-side participation even though its net column is positive only.

A candidate selects internal species X and reaction identities S. Every selected reaction must contain a selected species on each literal side. A signed flow v must make Nv strictly positive on X; species outside X have no production constraint. A negative entry reverses that reaction. A motif is such a candidate, and a productive autocatalytic core (PAC) is inclusion-minimal in both selected sets. Neither a target nor an allowed-food list is supplied.

## Run and reuse

Python 3.11 was used. Install `pip install -r requirements.txt`, run `python example.py`, and run `python -m unittest -v`. Use `--output replay` to write elsewhere. Edit the matrices, species/reaction labels, candidate budget and CNF formula at the top of the driver. The default is the three-reaction cycle A→2B, B→2C, C→2A. The exact determinant is 7 and the integer flow (7,7,7) produces seven units of every internal species.

`LiteralSource` validates literal matrices and builds exact signed integer certificates. `SquareSearch` enumerates equally sized species/reaction subsets. The paper proves that a PAC exists exactly when some nonempty admissible square restriction is nonsingular. The solver returns **yes**, **no_exhaustive**, or **unknown_budget**; exhausting the candidate budget never becomes a negative scientific conclusion. This intentionally transparent solver is exponential. Its reusable exact verifier is the practical foundation for adding heuristic, SAT, MILP or branch-and-bound candidate generators without trusting their answers.

Square supports are tried in increasing size. The first successful support is also a PAC: any proper submotif would contain a smaller square witness, already excluded. In contrast, `LiteralSource.certificate` applied directly to a supplied support establishes only a motif and therefore PAC existence, not minimality. The independent original `check_certificate.py` verifies literal participation, zero flow outside S and strict integer production. Run it on `outputs/configured_certificate.json` for an independently checked YES result. Its acceptance does not test minimality. Integer flows use |det A| A⁻¹1 and are checked against the paper's factorial coefficient bound.

## Why unconstrained search remains difficult

`DirectedLinkage` turns a directed graph with four terminals into a literal source. Graph arcs become species; internal vertices and two merged boundary vertices become reactions. The incidence saturation argument in the paper forces any admissible nonsingular restriction to encode two disjoint paths. The desired endpoint pairing has boundary determinant −3; the crossed pairing has determinant zero. The example independently checks all 16 direct-terminal graphs and a boundary-free cycle negative case.

`CNF` implements the paper's full switch-stack/variable-rail/clause-gate construction. The fixed 20-vertex, 29-arc switch is completely re-enumerated over all simple input/output paths; control forcing, residual role preservation and mutual exclusivity are checked afresh. A satisfying assignment builds two explicit vertex-disjoint paths, then an exact integer productivity certificate in the compiled reaction network. Repeated literals are distinct occurrences. Empty formulas, empty clauses, contradictory clauses and unused variable slots are supported. An empty formula still has a dummy switch and four distinct terminals.

The default two-variable formula is (x1) AND (NOT x1 OR x2). The program finds its assignment, compiles the network, checks its paths and independently verifies productivity. It does **not** enumerate every selected support of that much larger source. For unsatisfiable boundary formulas, NO-PAC is an inference from the paper's reduction theorem after exhaustive assignment enumeration, clearly identified as such. It is not a hidden result of direct network search. The polynomial reduction is not a polynomial SAT/PAC solver: assignment enumeration is exponential too.

`BinarySourceCodec` follows Appendix B and the inspected `BinaryFields.lean`/`BinarySourceData.lean`: canonical least-significant-bit-first natural digits, each prefixed by 1, followed by 0; zero has no digits. Dimensions precede both matrices in reaction-major order. It rejects noncanonical fields, truncation and extra fields. Labels are not encoded. A zero-dimensional source with an enormous declared dimension is subject to an explicit allocation safety limit in this Python decoder; that implementation limit is not part of the mathematical language. The example does not implement the formal SAT binary parser or prove a total machine-level polynomial-time transducer. Lean and the actual transition-count proofs are not rerun.

## What the certificate does and does not mean

The comparisons show that cancelling literal participation can turn YES into NO, negative flows matter, closed conservative cycles cannot grow every species, and selecting A while treating F as external can permit A+F→2A even though the full reaction conserves total molecular count. A selected subset can therefore be productive when the whole network is not.

These are structural flow certificates. There is no mass-action law, concentration trajectory, elemental composition, finite food inventory or operating time in the decision problem. The SAT reduction's bounded stoichiometric coefficients do not make it an elementary chemically realized reactor. Adding those restrictions asks a different question. The code does not claim a physically calibrated kinetic model where the paper supplies none.

Outputs include selected supports, exact integer flows/production, counterexamples, all simple-switch check counts, the compiled formula source and paths, source bit encoding, figures, hashes and explicit failed-certificate/budget results. The original independent certificate checker is copied unchanged with its hash recorded in `source_provenance.json`; the search, codec and constructive reduction are new paper-local implementations.

MIT is proposed for newly authored example code pending the owner's license decision. This README makes no license grant.