ArchytasZX

A qufinite ZX-calculus engine for reasoning and interacting with quantum states that leverages symbolic algebra to remove qudit-count and dimensionality limits.

Example:

prove_by_induction(boxed, fused, witness={"d": 2})
# proved=True  verdict=proved_uniform  index='m'  held_symbolic={'d'}

One call, one proof, an entire doubly indexed family of identities for every qudit count and every qudit dimension at once.

---

Why

Coming soon.

Install

Python ≥ 3.11. numpy and sympy are the only runtime dependencies.

pip install archytaszx

To work on the engine itself, install from a clone instead:

git clone https://github.com/Arhip-Dmitriev/ArchytasZX.git
cd ArchytasZX
python -m venv .venv && source .venv/bin/activate
pip install -e '.[dev]'
python -m pytest

The distribution is named ArchytasZX and installs from PyPI as archytaszx (the index normalizes the two to the same name); the importable package is archytaszx. There is no REPL and no command-line entry point yet — archytaszx/repl/shell.py is a skeleton awaiting implementation. The engine can currently only be used as a Python library, and has generally limited use.

Imports

The sub-package __init__.py files are empty. There are no re-exports, so from archytaszx import Diagram will fail — import by full module path. It is verbose during the development phase:

# Layer A -- symbolic algebra
from archytaszx.algebra.dimension import Dim, unify_all
from archytaszx.algebra.phase import Phase, PhaseVector
from archytaszx.algebra.scalar import Scalar

# Layer B -- diagram data model
from archytaszx.diagram.graph import Diagram, Direction, PortRef
from archytaszx.diagram.generators import Z_SPIDER, X_SPIDER, FOURIER_BOX, TRIANGLE, W_NODE
from archytaszx.diagram.generators import TRIANGLE_INVERSE, DIM_BINDER, DIM_SPLITTER
from archytaszx.diagram.bangbox import abstract_subgraph_count, abstract_port_count, peel_one
from archytaszx.diagram.validate import validate, validate_or_raise

# Layer C -- rewriting
from archytaszx.rewrite.match import find_matches
from archytaszx.rewrite.engine import apply
from archytaszx.rewrite.rules_library import SPIDER_FUSION, FOURIER_CANCELLATION, ZX_CAP

# Layer D -- semantics, proof, certificates
from archytaszx.semantics.check import compare, score, compare_symbolic
from archytaszx.semantics.contract_symbolic import contract_symbolic
from archytaszx.semantics.induction import prove_by_induction
from archytaszx.semantics.certificate import certify, verify

# The restricted Dirac front end
from archytaszx.repl.parser import parse_dirac_source

Errors

Every module raises only its own hierarchy, under a base <Area>Error:

Exception	Meaning
<Area>GrammarError	Wrong call
<Area>DomainError	Unimplemented as of now

Quickstart

1. Fuse two spiders over a symbolic dimension

Build a state-prep Z spider whose output feeds a copy spider, with the dimension left as the symbol d, and fuse them.

from archytaszx.algebra.dimension import Dim
from archytaszx.diagram.generators import Z_SPIDER
from archytaszx.diagram.graph import Diagram, Direction, PortRef
from archytaszx.rewrite.match import find_matches
from archytaszx.rewrite.engine import apply
from archytaszx.rewrite.rules_library import SPIDER_FUSION

d = Dim.symbol("d")

g = Diagram()
a = g.add_node(Z_SPIDER, input_dims=[], output_dims=[d, d])
b = g.add_node(Z_SPIDER, input_dims=[d], output_dims=[d, d])
g.add_wire(PortRef(a, Direction.OUTPUT, 0), PortRef(b, Direction.INPUT, 0))
g.set_boundary_outputs([
    PortRef(a, Direction.OUTPUT, 1),
    PortRef(b, Direction.OUTPUT, 0),
    PortRef(b, Direction.OUTPUT, 1),
])

result = apply(g, SPIDER_FUSION, find_matches(g)[0])

len(result.diagram.nodes)             # 1         -- two spiders became one
len(result.diagram.boundary_outputs)  # 3         -- the boundary is unchanged
result.diagram.scalar                 # Scalar(1) -- exact, never discarded

d was never given a value. The exact scalar the rule introduces is tracked rather than dropped, which is what makes the result an equality rather than a proportionality.

2. Check it, and get a replayable certificate

from archytaszx.semantics.check import compare
from archytaszx.semantics.certificate import certify, verify

compare(g, result.diagram, {"d": 5}).matched   # True -- numeric oracle at d = 5

certificate = certify(g, [result], label="fuse A into B")
verify(certificate, {"d": 3}).verified         # True

verify replays the derivation from the recorded steps and oracle-checks the input against the re-derived output. Tampering with any recorded field (the scalar, the rule name, a consumed wire, a side-condition outcome, a multiplicity) fails the replay.

3. Prove it for every count at once

Wrap the same graph in a bang box with symbolic multiplicity m, and discharge the identity for every value of m with d still symbolic.

from archytaszx.diagram.bangbox import abstract_subgraph_count
from archytaszx.semantics.induction import prove_by_induction

boxed, box_id, mult = abstract_subgraph_count(g, frozenset({a, b}), 1, stem="m")
fused = apply(boxed, SPIDER_FUSION, find_matches(boxed)[0]).diagram

proof = prove_by_induction(boxed, fused, witness={"d": 2})

proof.proved          # True
proof.verdict         # Verdict.PROVED_UNIFORM
proof.index           # 'm': the multiplicity inducted on
proof.discharge       # StepDischarge.UNIFORM_REWRITE -- which tier settled it
proof.held_symbolic   # frozenset({'d'}) -- what stayed universally quantified

The verdict distinguishes a proof for all n from a finite schema check, and discharge names the tier that did the work. SCHEMA_CHECKED is reported separately from the two PROVED_* verdicts.

4. Dirac in, with concrete numbers

from archytaszx.repl.parser import parse_dirac_source

p = parse_dirac_source("sum_{k=0}^{3-1} |k>^{30}; copy")

len(p.nodes)         # 2
len(p.bang_boxes)    # 1
dict(p.parameters)   # {'d': 3, 'n': 29}

The user typed 3 and 30. What came back is symbolic in both axes, with the values recorded in the parameter environment for substitution back on output. The tensor power costs one leg under a bang box, not thirty, and stays open to induction. Prefix a numeral with literal to suppress abstraction.

The full tour

Every layer end to end — validation, matching, certificates, the numeric and symbolic oracles, the Dirac front end, and a proof by induction:

python examples/api_tour.py

docs/TUTORIAL.md is the matching API reference, section for section. examples/demo_visual.py is a wide-terminal walkthrough that prints the full unfiltered trace next to the diagram pictures (working, but outdated).

Architecture

Four layers, with the dependency direction running downward: algebra ← diagram ← rewrite ← semantics.

A — Symbolic algebra substrate (archytaszx/algebra/) Dimension expressions — a concrete integer, a symbol such as d, or arithmetic such as d^n or d1·d2 — normalised through one canonical form with a unifier that decides or constrains when two must agree, and abstract/substitute as inverse directions. Phases as concrete values, root-of-unity indices, or free symbolic parameters, carried in vectors whose length is tied to d. Exact scalars built from roots of unity ω_d = e^{2πi/d} and free symbols, with a character-sum simplifier that knows Σ_{k=0}^{d-1} ω_d^{jk} = d·[j ≡ 0 mod d].

B — Diagram data model (archytaszx/diagram/) Ports carrying their own dimension label; nodes carrying a generator type, ordered input and output ports, and a symbolic phase slot; diagrams holding nodes, wires, ordered boundary lists, a parameter environment, and an exact scalar accumulator. Bang boxes annotate a scoped subgraph with a multiplicity symbol and support instantiate, copy, kill, merge and peel.

C — Rewrite engine (archytaszx/rewrite/) A rule bundles a left-hand pattern, a right-hand builder, side conditions, quantifiers over counts and dimensions, and the exact scalar it introduces. The matcher finds occurrences and checks every side condition before a rule may fire. The engine applies a rule at a match, returns a new diagram, and records structured provenance from which a certificate is emitted.

D — Semantics oracle and proof (archytaszx/semantics/) Three rungs in order of preference: rewriting first; symbolic contraction with d kept formal as the general fallback, and the path by which a supplied concrete value of any size is evaluated; numeric contraction at small concrete instantiations as the verification oracle of last resort. Alongside them, induction over bang-box multiplicities and replayable certificates.

Numeric contraction is the oracle. A spider's denotation is d^rank entries, so it saturates within single digits of legs. Large concrete values are answered by substituting the parameter environment into the closed symbolic form, which costs nothing in the size of the value.

Project status

This is a research prototype under active development. The API is unstable, the rule library is very limited, and nothing here should be treated as a useful, finished tool at this moment.

Working today

Area	State
Dimension algebra	Integers, symbols, products, powers; one canonical form; abstract/substitute both directions
Phase and scalar algebra	Symbolic phase vectors tied to d; exact scalars with no silent global factors
Diagram model	Per-port dimensions, ordered boundaries, parameter environment, deep copy
Validation	Joint (leg-order independent) dimension resolution, per-node policy checks, a diagram-global consistency pass, boundary and port checks, symbol-role separation; typed finding kinds
Generators	Z spider, X spider, Fourier box, triangle and its inverse, W node, dimension binder and splitter
Rewrite core	Rule/pattern/builder abstraction, matcher, engine, structured provenance
Rule library	spider_fusion, fourier_cancellation, zx_cap, z_fusion_prime_d (dimension-guarded)
Numeric oracle	Denotation, contraction, exact comparison, opt-in up-to-global-phase mode
Symbolic contraction	Arbitrary diagram closed with d formal, through the character-sum simplifier
Induction	Base + step over a bang-box multiplicity, four-tier step ladder, five distinct verdicts
Certificates	Per-step provenance, independent replay, tamper detection
Dirac front end	One restricted grammar: a summed ket family

Not yet implemented

The broader rule library and strategy layer · the normal-form decision procedure · equality saturation and the e-graph · tactics and proof search · match and denotation caching · scalable sheet-wire notation · the diagram-to-Dirac printer · the general declaration syntax and the interactive REPL.

Known limits inside what is implemented

• The dimension unifier cancels common factors and then decides the reduced equation. It still reports DEFERRED where an equation has several solution branches: a product of symbols against a concrete (d1*d2 == 6), and equations with symbolic exponents (d**n == d**m). Deferred and bound dimension findings are recorded as assumptions, and both reach the certificate.
• A dimension guard is three-valued. A rule restricted to prime d refuses to fire at a composite d and equally refuses at a symbolic d, which cannot be decided.
• Symbolic contraction handles a symbolic multiplicity only where the bang box is closed off from the rest of the diagram; a box meeting a wire or a boundary slot has a rank that varies with the count.
• compare_symbolic has three outcomes, not two — equal, unequal, and indeterminate (the residual still carries an undecided index sum). Read .reason whenever a comparison comes back unmatched.
• The induction step case settles a family whose peeled copies the scalar layer can close; the rest falls through to rewriting at symbolic n or to a finite schema check, which reports itself as one.

Development

python -m pytest          # default tier: 1408 tests, ~45s
python -m pytest -m slow  # 28 multi-thousand-seed fuzz sweeps and oracle differentials, ~15m
python -m pytest -m ""    # both tiers together
ruff format . && ruff check . && mypy archytaszx

ruff format is authoritative for layout; mypy runs in strict mode. Counts and timings measured 2026-09-08.

Main References

• Wang, Qufinite ZX-calculus: a unified framework of qudit ZX-calculi — arXiv:2104.06429
• Kissinger et al., on bang boxes and scalable notation — arXiv:2204.11702
• van de Wetering, ZX-calculus for the working quantum computer scientist — arXiv:2012.13966

Citation

If you use ArchytasZX in academic work, please cite it via CITATION.cff, or:

@software{dmitriev_archytaszx,
  author  = {Dmitriev, Arkhip Alekseyevich},
  title   = {ArchytasZX: a qufinite ZX-calculus engine with symbolic qudit count and dimension},
  year    = {2026},
  url     = {https://github.com/Arhip-Dmitriev/ArchytasZX},
  license = {Apache-2.0}
}

Contributing

Issues — bug reports, counterexamples, questions about the mathematics — are a vital part of the development process. See CONTRIBUTING.md for setup, the required checks, and how to report a soundness bug.

License

Apache License 2.0 — see LICENSE.