Example code
An autocatalytic network may contain several irreducible RAFs: reaction sets that lose self-support if any reaction is removed. Finding some does not establish that the list is complete. This example implements the exact completeness test, returns a missing member when one exists, and builds the paper's reaction networks that encode the selection of sufficient starting statements and the search for fully connected groups of graph vertices (cliques). The checker also accepts your own network and supplied family as JSON.
An irreducible RAF is a nonempty, food-generated, catalysed reaction set with no proper RAF inside it. It is inclusion-minimal, not necessarily smallest. RAFOracle tests irreducibility by deleting each reaction and computing the maximum RAF inside the remainder. Checking only whether the remainder itself is a RAF would miss smaller surviving subsets.
CompletenessChecker first validates the supplied family. It then chooses one reaction from each listed irrRAF and deletes those choices. If any such deletion leaves a RAF, that survivor contains an unlisted irreducible member. If every choice destroys all RAFs, the list is complete. Overlapping lists are supported: two choices can name the same deleted reaction. Duplicate entries do not increase the family size, and the empty list is complete exactly when the network contains no RAF.
The three-reaction example in the figure has all three pairs as irrRAFs. Listing and covers every reaction but misses . Choosing from both listed sets exposes the missing member. The saved report includes the deletion choices, residual RAF and the verified missing set.
The paper's main construction turns a small set of starting statements that derives all others into an unlisted irrRAF. Each supplied guard is a simple catalytic cycle of selectors. A decoder reads the unique selector omitted from its slot and produces that statement as an axiom. Implication reactions derive further statements; a closing reaction requires all statements and slot markers and produces the common catalyst. Catalysts are checked in the final closure, preserving ordinary RAF semantics even when the common catalyst appears last.
For the cyclic rules , , and one slot, the code reproduces 33 RAFs and four irrRAFs. Only the selector cycle was supplied. The returned missing member omits selector 0 and decodes to axiom , whose derivation reaches all three statements. A control with three independent statements and two slots has no sufficient axiom choice: its two listed cycles are complete, after all nine deletion tuples are checked.
CliqueReduction implements the paper's separate graph construction. Pair-verification gates force the omitted selectors of a missing irrRAF to choose distinct adjacent vertices. The default triangle with three slots yields the clique . Both reductions expose their literal reaction systems and decode returned witnesses back into the original problem.
The search has at most deletion tuples, where is the number of distinct listed irrRAFs and their largest size. The figure shows this count, not runtime. A configured budget that stops the search produces inconclusive, never complete. Report verification checks missing members directly; verifying a complete result reruns the criterion.
Download the package, install requirements.txt, run python example.py --output outputs, then python -m unittest -v. Editable rules, slot counts and graph edges appear first. Import the chemistry, oracle, checker or reductions independently, or run python example.py --input outputs/model_input.json --output custom_run with an edited input file.
Seven test groups reproduce all 768 two-statement reduction cases and independently enumerate all reaction subsets in the 512 cases with at most one slot. They also check graph instances, overlapping and invalid families, empty inputs, search limits and forged reports. The example concerns combinatorial RAFs; it makes no kinetic-persistence claim and does not replace the paper's Lean proofs or conventional complexity arguments.
Python source
"""Validate a supplied irrRAF family, certify completeness, or return a missing member."""
# EDITABLE INPUTS -------------------------------------------------------------
STATEMENTS = ("0", "1", "2")
IMPLICATIONS = ((("0",), "1"), (("1",), "2"), (("2",), "0"))
AXIOM_SLOTS = 1
# Demonstrate a complete family as well: 3 independent statements need 3 axioms.
CONTROL_STATEMENTS = ("0", "1", "2")
CONTROL_IMPLICATIONS = ()
CONTROL_SLOTS = 2
# Optional graph-to-RAF reduction, reproducing the paper's second mechanism.
GRAPH_VERTICES = 3
GRAPH_EDGES = ((0, 1), (1, 2), (0, 2))
CLIQUE_SLOTS = 3
# Safe, explicit search budget: exhausting it gives INCONCLUSIVE, never complete.
MAX_TRANSVERSALS = 100000
# ---------------------------------------------------------------------------
import argparse
from dataclasses import dataclass
import hashlib
from itertools import combinations, product
import json
import math
from pathlib import Path
import platform
@dataclass(frozen=True)
class Reaction:
name: str
reactants: frozenset[str]
products: frozenset[str]
catalysts: frozenset[str]
def __post_init__(self):
for field in ("reactants", "products", "catalysts"):
object.__setattr__(self, field, frozenset(getattr(self, field)))
@dataclass(frozen=True)
class ReactionSystem:
food: frozenset[str]
reactions: tuple[Reaction, ...]
def __post_init__(self):
object.__setattr__(self, "food", frozenset(self.food))
object.__setattr__(self, "reactions", tuple(self.reactions))
if len(self.ids) != len(self.reactions):
raise ValueError("Reaction identifiers must be unique")
@property
def ids(self):
return frozenset(r.name for r in self.reactions)
def select(self, allowed):
allowed = frozenset(allowed)
if not allowed <= self.ids:
raise ValueError("Unknown reaction identifier")
return tuple(r for r in self.reactions if r.name in allowed)
def closure_stages(self, allowed):
selected = self.select(allowed)
stages = [self.food]
while True:
next_state = stages[-1] | frozenset(x for r in selected if r.reactants <= stages[-1] for x in r.products)
if next_state == stages[-1]:
return tuple(stages)
stages.append(next_state)
def is_raf(self, allowed):
selected = self.select(allowed)
closure = self.closure_stages(allowed)[-1]
return bool(selected) and all(r.reactants <= closure and r.catalysts & closure for r in selected)
def to_dict(self):
return {"food": sorted(self.food), "reactions": [{"name": r.name,
"reactants": sorted(r.reactants), "products": sorted(r.products),
"catalysts": sorted(r.catalysts)} for r in self.reactions]}
@classmethod
def from_dict(cls, data):
return cls(frozenset(data["food"]), tuple(Reaction(**row) for row in data["reactions"]))
class RAFOracle:
def __init__(self, system):
self.system = system
self.calls = 0
def maximum(self, allowed=None):
self.calls += 1
remaining = self.system.ids if allowed is None else frozenset(allowed)
self.system.select(remaining)
while remaining:
closure = self.system.closure_stages(remaining)[-1]
keep = frozenset(r.name for r in self.system.select(remaining)
if r.reactants <= closure and r.catalysts & closure)
if keep == remaining:
break
remaining = keep
return remaining
def irreducible(self, allowed):
allowed = frozenset(allowed)
return self.system.is_raf(allowed) and all(not self.maximum(allowed-{r}) for r in sorted(allowed))
def extract(self, allowed):
"""One inclusion-minimal RAF; no minimum-cardinality claim."""
current = self.maximum(allowed)
for r in sorted(current):
if r in current:
smaller = self.maximum(current-{r})
if smaller:
current = smaller
return current
class CompletenessChecker:
def __init__(self, system):
self.system = system
def check(self, supplied, max_transversals=None):
# A family is a SET of reaction sets. Duplicate entries do not increase k.
family = tuple(sorted(set(map(frozenset, supplied)), key=lambda s: tuple(sorted(s))))
oracle = RAFOracle(self.system)
base = {"family": [sorted(s) for s in family], "k": len(family),
"largest_listed_size": max(map(len,family),default=1),
"transversal_bound": math.prod(map(len,family))}
for member in family:
if not member <= self.system.ids or not oracle.irreducible(member):
return {**base, "status": "invalid", "invalid_entry": sorted(member),
"reason": "Each distinct supplied member must be an irreducible RAF"}
validity_calls = oracle.calls
if max_transversals is not None and max_transversals < 0:
raise ValueError("Search budget must be nonnegative or None")
trace, seen = [], {}
for index, choices in enumerate(product(*(sorted(s) for s in family))):
if max_transversals is not None and index >= max_transversals:
return {**base, "status": "inconclusive", "validity_oracle_calls": validity_calls,
"tested_tuples": len(trace), "distinct_residual_queries": len(seen), "trace": trace}
deleted = frozenset(choices)
cached = deleted in seen
if not cached:
seen[deleted] = oracle.maximum(self.system.ids-deleted)
residual = seen[deleted]
trace.append({"choices": choices, "deleted": sorted(deleted),
"residual_maximum": sorted(residual), "cached": cached})
if residual:
missing = oracle.extract(residual)
if missing in family or not oracle.irreducible(missing):
raise ArithmeticError("Missing-member certificate failed")
return {**base, "status": "incomplete", "missing": sorted(missing),
"omissions": choices, "validity_oracle_calls": validity_calls,
"tested_tuples": len(trace), "distinct_residual_queries": len(seen), "trace": trace,
"missing_closure_stages": [sorted(s) for s in self.system.closure_stages(missing)]}
return {**base, "status": "complete", "validity_oracle_calls": validity_calls,
"tested_tuples": len(trace), "distinct_residual_queries": len(seen), "trace": trace}
def verify_report(self, report):
"""Recompute the finite claim; no trust in a saved success label or trace."""
status = report.get("status")
family = tuple(map(frozenset, report.get("family", ())))
oracle = RAFOracle(self.system)
if status == "incomplete":
try:
return (all(oracle.irreducible(s) for s in family)
and frozenset(report["missing"]) not in family
and oracle.irreducible(report["missing"]))
except (KeyError, ValueError):
return False
if status == "complete":
return self.check(family)["status"] == "complete"
return False
@dataclass(frozen=True)
class Implication:
premises: frozenset[str]
conclusion: str
def __post_init__(self):
object.__setattr__(self, "premises", frozenset(self.premises))
@dataclass(frozen=True)
class ImplicationSystem:
statements: tuple[str, ...]
rules: tuple[Implication, ...]
def __post_init__(self):
if len(set(self.statements)) != len(self.statements):
raise ValueError("Duplicate statement")
universe = set(self.statements)
if any(not r.premises <= universe or r.conclusion not in universe for r in self.rules):
raise ValueError("Rule refers to an unknown statement")
def stages(self, axioms):
current = frozenset(axioms)
if not current <= set(self.statements):
raise ValueError("Unknown axiom")
stages = [current]
while True:
new = current | frozenset(r.conclusion for r in self.rules if r.premises <= current)
if new == current:
return tuple(stages)
stages.append(new)
current = new
def generators(self, budget):
return tuple(frozenset(s) for size in range(min(budget,len(self.statements))+1)
for s in combinations(self.statements,size) if self.stages(s)[-1] == frozenset(self.statements))
def normalized(self):
statements, rules = list(self.statements), list(self.rules)
while len(statements) < 2:
new = "_padding_"+str(len(statements))
while new in statements:
new += "_"
statements.append(new)
rules.append(Implication(frozenset(),new))
return ImplicationSystem(tuple(statements),tuple(rules))
class AxiomReduction:
"""Literal selector / decoder / implication / closing construction."""
def __init__(self, source, slots):
if not isinstance(slots,int) or slots < 0:
raise ValueError("Nonnegative integer slot count required")
self.source, self.slots = source.normalized(), slots
m = len(self.source.statements)
reactions = []
self.guards = tuple(frozenset(f"s:{i}:{u}" for u in range(m)) for i in range(slots))
for i in range(slots):
for u in range(m):
reactions.append(Reaction(f"s:{i}:{u}", {"f"}, {f"x:{i}:{u}",f"c:{i}:{u}"}, {"z",f"c:{i}:{(u+1)%m}"}))
reactions.append(Reaction(f"d:{i}:{u}", {f"x:{i}:{v}" for v in range(m) if v != u}, {f"b:{i}",f"A:{u}"}, {"z"}))
lookup = {s:i for i,s in enumerate(self.source.statements)}
for j, rule in enumerate(self.source.rules):
reactions.append(Reaction(f"p:{j}", {"f"}|{f"A:{lookup[v]}" for v in rule.premises}, {f"A:{lookup[rule.conclusion]}"}, {"z"}))
reactions.append(Reaction("close", {f"b:{i}" for i in range(slots)}|{f"A:{u}" for u in range(m)}, {"z"}, {"z"}))
self.system = ReactionSystem(frozenset(("f",)), tuple(reactions))
def decode_missing(self, missing):
missing = frozenset(missing)
if missing in self.guards or "close" not in missing or not RAFOracle(self.system).irreducible(missing):
raise ValueError("Supply an unlisted irrRAF of this constructed system")
choices = []
for guard in self.guards:
omitted = guard-missing
if len(omitted) != 1:
raise ArithmeticError("Omission pattern failed")
u = int(next(iter(omitted)).split(":")[-1])
choices.append(self.source.statements[u])
stages = self.source.stages(choices)
if stages[-1] != frozenset(self.source.statements):
raise ArithmeticError("Extracted axioms do not generate the universe")
return {"slot_choices": choices, "axioms": sorted(set(choices)),
"derivation_stages": [sorted(s) for s in stages]}
def source_witness(self, choices):
if len(choices) != self.slots or self.source.stages(choices)[-1] != frozenset(self.source.statements):
raise ValueError("Supply one generating choice per slot")
indices = [self.source.statements.index(s) for s in choices]
result = {r for i,g in enumerate(self.guards) for r in g if r != f"s:{i}:{indices[i]}"}
result |= {f"d:{i}:{u}" for i,u in enumerate(indices)}
result |= {f"p:{j}" for j in range(len(self.source.rules))}|{"close"}
if not self.system.is_raf(result):
raise ArithmeticError("Forward witness failed")
return frozenset(result)
class CliqueReduction:
"""Paper's independent ETH reduction, retaining all ordered pair gates."""
def __init__(self, vertices, edges, slots):
if vertices < 2 or slots < 0:
raise ValueError("At least two vertices and nonnegative slots required")
self.vertices, self.slots = vertices, slots
self.edges = frozenset(frozenset(e) for e in edges)
if any(len(e) != 2 or not e <= set(range(vertices)) for e in self.edges):
raise ValueError("A simple graph on the stated vertices is required")
# Guards are identical to the axiom construction; only decoder products
# and the verifier differ. Build this network independently for clarity.
reactions = []
self.guards = tuple(frozenset(f"s:{i}:{u}" for u in range(vertices)) for i in range(slots))
for i in range(slots):
for u in range(vertices):
reactions.append(Reaction(f"s:{i}:{u}", {"f"}, {f"x:{i}:{u}",f"c:{i}:{u}"}, {"z",f"c:{i}:{(u+1)%vertices}"}))
reactions.append(Reaction(f"d:{i}:{u}", {f"x:{i}:{v}" for v in range(vertices) if v != u}, {f"b:{i}"}, {"z"}))
positions = tuple(product(range(slots),range(vertices)))
pairs = tuple(product(positions,repeat=2))
for index, ((i,u),(j,v)) in enumerate(pairs):
forbidden = i != j and frozenset((u,v)) not in self.edges
for side, position in (("l",(i,u)),("r",(j,v))):
inputs = {f"x:{position[0]}:{position[1]}"} if forbidden else {"f"}
reactions.append(Reaction(f"{side}:{index}", inputs, {f"y:{index}"}, {"z"}))
reactions.append(Reaction("close", {f"b:{i}" for i in range(slots)}|{f"y:{i}" for i in range(len(pairs))}, {"z"}, {"z"}))
self.system = ReactionSystem(frozenset(("f",)),tuple(reactions))
def decode_missing(self, missing):
missing = frozenset(missing)
if missing in self.guards or not RAFOracle(self.system).irreducible(missing):
raise ValueError("Expected an unlisted irreducible RAF")
vertices = []
for guard in self.guards:
omitted = guard-missing
if len(omitted) != 1:
raise ArithmeticError("Expected one omitted selector per slot")
vertices.append(int(next(iter(omitted)).split(":")[-1]))
if len(set(vertices)) != self.slots or any(frozenset(pair) not in self.edges for pair in combinations(vertices,2)):
raise ArithmeticError("Decoded choices are not a clique")
return vertices
def literal_family(system):
"""Independent all-subsets predicate enumeration for small examples only."""
if len(system.reactions) > 18:
raise ValueError("Literal enumeration is limited to 18 reactions")
rafs, irreducibles = [], []
for size in range(1,len(system.reactions)+1):
for subset in combinations(sorted(system.ids),size):
subset = frozenset(subset)
if system.is_raf(subset):
rafs.append(subset)
if not any(i < subset for i in irreducibles):
irreducibles.append(subset)
return tuple(rafs), tuple(irreducibles)
def coverage_example():
return ReactionSystem(frozenset(("f",)),tuple(Reaction(s,{"f"},{s},set("abc")-{s}) for s in "abc"))
def main():
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("--output",type=Path,default=Path("outputs"))
parser.add_argument("--input",type=Path,help="JSON with food, reactions, and supplied_family; skips built-in demonstrations")
args = parser.parse_args()
args.output.mkdir(parents=True,exist_ok=True)
if args.input:
data = json.loads(args.input.read_text())
system = ReactionSystem.from_dict(data)
report = CompletenessChecker(system).check(data["supplied_family"],MAX_TRANSVERSALS)
(args.output/"certification.json").write_text(json.dumps(report,indent=2)+"\n")
print(report["status"])
return
source = ImplicationSystem(STATEMENTS,tuple(Implication(frozenset(p),c) for p,c in IMPLICATIONS))
reduction = AxiomReduction(source,AXIOM_SLOTS)
checker = CompletenessChecker(reduction.system)
report = checker.check(reduction.guards,MAX_TRANSVERSALS)
decoded = reduction.decode_missing(report["missing"]) if report["status"] == "incomplete" else None
control_source = ImplicationSystem(CONTROL_STATEMENTS,tuple(Implication(frozenset(p),c) for p,c in CONTROL_IMPLICATIONS))
control = AxiomReduction(control_source,CONTROL_SLOTS)
control_report = CompletenessChecker(control.system).check(control.guards,MAX_TRANSVERSALS)
overlap = coverage_example()
overlap_report = CompletenessChecker(overlap).check(({"a","b"},{"a","c"}),MAX_TRANSVERSALS)
clique = CliqueReduction(GRAPH_VERTICES,GRAPH_EDGES,CLIQUE_SLOTS)
clique_report = CompletenessChecker(clique.system).check(clique.guards,MAX_TRANSVERSALS)
decoded_clique = clique.decode_missing(clique_report["missing"]) if clique_report["status"] == "incomplete" else None
# Literal enumeration is an optional independent check, never needed by the
# reusable completeness checker. Larger edited examples remain runnable.
if len(reduction.system.reactions) <= 18:
rafs, irr = literal_family(reduction.system)
counts = {"rafs":len(rafs),"irreducibles":len(irr),"members":[sorted(s) for s in irr]}
else:
counts = {"skipped":"More than 18 reactions; literal enumeration would be exponential"}
results = {"axiom_instance": report,"decoded_axioms":decoded,"literal_check":counts,
"complete_control":control_report,"coverage_is_not_completeness":overlap_report,
"clique_instance":clique_report,"decoded_clique":decoded_clique}
(args.output/"results.json").write_text(json.dumps(results,indent=2)+"\n")
source_data = {**reduction.system.to_dict(),"supplied_family":[sorted(g) for g in reduction.guards]}
(args.output/"model_input.json").write_text(json.dumps(source_data,indent=2)+"\n")
import matplotlib
matplotlib.use("Agg")
import matplotlib.pyplot as plt
plt.rcParams.update({"font.size":11,"axes.spines.top":False,"axes.spines.right":False,"svg.hashsalt":"irrraf-completeness-v1"})
fig, axes = plt.subplots(1,2,figsize=(12,4.8),layout="constrained")
# Show the small coverage loss with its independently enumerated exact family.
_, overlap_irr = literal_family(overlap)
members = [sorted(s) for s in overlap_irr]
axes[0].imshow([[int(r in member) for r in "abc"] for member in members],cmap="Blues",vmin=0,vmax=1,aspect="auto")
axes[0].set(xticks=range(3),xticklabels=["a","b","c"],yticks=range(3),
yticklabels=["Listed {a,b}","Listed {a,c}","Missing {b,c}"],title="Covering every reaction can still miss an irrRAF")
for row,member in enumerate(members):
for col,r in enumerate("abc"):
axes[0].text(col,row,"present" if r in member else "absent",ha="center",va="center",color="white" if r in member else "#333333")
for largest in (2,3,5,10):
axes[1].plot(range(1,9),[largest**k for k in range(1,9)],"o-",label=f"Largest listed size {largest}")
axes[1].set(yscale="log",xlabel="Number k of distinct listed irrRAFs",ylabel="Upper bound on deletion tuples",title="Upper bound on completeness-search\ncombinations")
axes[1].legend(frameon=False,fontsize=9)
for ext in ("png","svg"):
fig.savefig(args.output/f"completeness.{ext}",dpi=165)
plt.close(fig)
console = "\n".join(["Completeness of irreducible RAF families",
f"Default source: {len(source.statements)} statements, {len(source.rules)} rules, {AXIOM_SLOTS} slots",
"Literal check: "+str({k:v for k,v in counts.items() if k != "members"}),
"Supplied guard family: "+report["status"],"Decoded source witness: "+str(decoded),
"Independent-statement control: "+control_report["status"]+f" after {control_report.get('tested_tuples',0)} tuples",
"Overlapping coverage list: "+overlap_report["status"]+"; missing "+str(overlap_report.get("missing")),
"Graph reduction: "+clique_report["status"]+"; decoded clique "+str(decoded_clique),
"Tuple bounds are combinatorial counts, not measured runtimes. No Lean re-execution claimed."])
print(console)
(args.output/"console.txt").write_text(console+"\n")
metadata = {"paper_sha256":"c89e78a1ffadcaaca3ac047d71817feef3b32d26f6c0af1b1d245082499e35ea",
"source_sha256":hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
"python":platform.python_version(),"matplotlib":matplotlib.__version__,
"inputs":{"statements":STATEMENTS,"implications":IMPLICATIONS,"slots":AXIOM_SLOTS,
"control_statements":CONTROL_STATEMENTS,"control_implications":CONTROL_IMPLICATIONS,"control_slots":CONTROL_SLOTS,
"graph_vertices":GRAPH_VERTICES,"graph_edges":GRAPH_EDGES,"clique_slots":CLIQUE_SLOTS,"max_transversals":MAX_TRANSVERSALS},
"output_sha256":{p.name:hashlib.sha256(p.read_bytes()).hexdigest() for p in sorted(args.output.iterdir())
if p.is_file() and p.name != "run_metadata.json"}}
(args.output/"run_metadata.json").write_text(json.dumps(metadata,indent=2)+"\n")
if __name__ == "__main__":
main()
Run output
Completeness of irreducible RAF families
Default source: 3 statements, 3 rules, 1 slots
Literal check: {'rafs': 33, 'irreducibles': 4}
Supplied guard family: incomplete
Decoded source witness: {'slot_choices': ['0'], 'axioms': ['0'], 'derivation_stages': [['0'], ['0', '1'], ['0', '1', '2']]}
Independent-statement control: complete after 9 tuples
Overlapping coverage list: incomplete; missing ['b', 'c']
Graph reduction: incomplete; decoded clique [0, 1, 2]
Tuple bounds are combinatorial counts, not measured runtimes. No Lean re-execution claimed.