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. The archytaszx command starts an interactive shell for the Dirac language (or runs .azx scripts such as examples/shor.azx); the language is summarised in the docstring of archytaszx/repl/lang.py and :help lists the engine commands. Engine commands start with : in the shell. Output styles are --mathtext (default), --unicode, --ascii and --latex; several flags print every output in each style, and --order holds the output until an error or the end and then groups it by style.

The same language is usable from Python:

from archytaszx import azx               # a shared Program; archytaszx.Program() for a fresh one
azx("var n")
azx.psi = azx.H ** azx.n | azx.ket(0) ** azx.n      # |psi> = H^@n |0>^@n
azx["|phi>"] = azx["|psi> - 2 |0><0|psi>"]
y = azx.measure | azx.psi
azx.phi.latex()                          # also rendered by Jupyter

Proofs found by the engine can be re-checked by the proof kernel (archytaszx.semantics.kernel, :certificate kernel) and exported to Lean 4 (:certificate lean proof.lean).

The export targets the Lean library bundled in archytaszx/lean (Lean 4.35, Mathlib). There a diagram is a tensor network over ℂ: the sum, over its wire labels, of the product of its generators' tensors. Every rewrite rule is a lemma proved there once. An exported proof states Equal E s N s' N' (s·⟦N⟧ = s'·⟦N'⟧) between the start and goal diagrams. Each step is an instance of a rule lemma, applied inside the rest of the diagram by a frame lemma, plus a relabelling checked by decide. The theorem states the diagrams' own scalars; their identity is a linear_combination whose coefficients the engine computes and Lean's ring checks.

Families over bang-box multiplicities are networks whose bundled wires carry a chain of multiplicities and a value below d^(k₁⋯kₙ), read as nested base-d digits. Spiders may bundle any number of legs; a node in node boxes is copies of copies (Bun); the environment holds every multiplicity as a list (F.env (ksOf [k, j])). A rule applied inside node boxes is lifted to every multiplicity by induction, one box at a time, peeling one copy per step. An induction proof, nested ones included, becomes a Lean induction over the same peeling. Dimension equalities a rewrite assumed are hypotheses of the theorem (outside bang boxes); a scalar outside the exact model (π, irrational powers, conjugates, sums) is an opaque complex variable, named in the header, over which the theorem is stated.

Lean re-checks the whole proof independently of the engine; #print axioms main should list only propext, Classical.choice and Quot.sound. What remains trusted is how a diagram is written as a network. A step with no lemma becomes an axiom named unproved_*, listed in the header; the REPL reports their number.

:decide verdicts take the same route. A normal-form or saturation verdict becomes a kernel theorem from the rewrites that reached it. Other rungs, symbolic contraction among them, are proved by the normaliser of symbolic sums, else by a proof search. :induct works the same way. When no proof is found, the REPL prints proof: none the kernel re-checks and names the method the verdict rests on.

The normaliser (ArchytasZX.Sym, SymNorm, SymCanon, SymNet) proves equalities for every value of the dimensions and phases. A network's entry is translated, once and generically (eval_tr), into a sum of terms: a coefficient times sums over bound indices of Kronecker deltas [M ∣ p] and roots of unity ω_D^p, with p an integer polynomial in the indices and M, D monomials in the dimension symbols. Each move is proved once: a bound index unused, pinned by a delta whose modulus divides its range, summed by the character sum Σ_k ω_D^(kA+B) = D [D ∣ A] ω_D^B, or counted by gcd(a, D); each delta's pivot substituted into the factors it determines; roots of unity merged; constant factors evaluated; bound indices renamed and factors sorted. nfEx composes them, nfEx_den proves it keeps the value, and equal_sym turns an empty normal form of s·⟦N⟧ - s'·⟦N'⟧ into Equal E s N s' N'. The Lean kernel computes the normal form (decide +kernel); archytaszx.semantics.lean_sym mirrors it to decide whether to export. Phase parameters are atoms ex g, whole turns of an integer phase symbol dropped; phases stored at index j need d > j, stated as a floor hypothesis. A phase rule p(k)/D, p an integer polynomial and D a dimension monomial, is a root-of-unity factor at the spider's bound index (rule_ex), so quadratic phases are reached when their sums cancel.

A family is proved for every value of every multiplicity by induction on one multiplicity at a time, outermost box first; a box nested in a box of the same symbol, and a compound multiplicity such as k + 1, get a variable of their own that the theorem then instantiates. A node box meeting the rest only at the boundary peels one copy per step: the hypothesis is plugged into the peeled networks and the peeled copies are proved the same way, scaled by the factor a scalar geometric in the multiplicity gains per copy. A port box on Z and X spiders or a W node's outputs steps by Equal.of_port (ArchytasZX.Port): at k ≥ 1 the split network is the network at an assignment that advances each X or W bundle's lowest digit by its peeled leg, times a factor of the boundary alone, so equal networks have equal splits. The zero networks, and for a port box the one-copy networks, go to the normaliser.

Scalars that differ between the sides by an exact factor are proved with their common part, outside the exact model or depending on a multiplicity, multiplied on afterwards. A node whose legs differ in dimension, such as d^p and d^q, is proved under the hypothesis d^p = d^q, which the theorem states and the REPL reports. A rewrite proof resting on a deferred dimension constraint is proved over the merged network and transported to the diagrams' own dimensions (Equal.of_mapDim'), the constraint a hypothesis of the theorem. A rewrite proof with a step lacking a lemma, or one that does not translate, is replaced by the normaliser's proof when that one exists. What has no Lean proof path is listed in LEAN_GAPS.txt.

Verdicts that two diagrams differ (:decide, :prove, :check, :induct) export a Lean refutation: ¬ ∀ params, Equal …, proved at the counterexample or a default sample point. There eval_cyc evaluates both networks exactly as polynomials in ζ = om M, computed by the Lean kernel (decide +kernel). At one boundary assignment the scaled difference is rewritten, by linear_combination over the relations of √x, ζ^M = 1 and the prime-gon sums, into a nonzero integer vector of length at most φ(M). cyc_ne shows that vector does not vanish, by the degree of the cyclotomic minimal polynomial. √p for an odd prime is a quadratic Gauss sum, checked by its square and the sign of its real part. A point involving π or an irrational phase is refuted by ball arithmetic (ArchytasZX.Ball): every subterm gets an enclosure from π's 20-digit bounds, square roots and a Taylor bound on exp, and a ball away from zero contradicts the equality. Diagrams whose interfaces differ are refuted on their leg dimensions; families whose boundaries are written differently are refuted after instantiating their multiplicities.

cd archytaszx/lean && lake exe cache get && lake build      # once
lake env lean /path/to/proof.lean

From Python, archytaszx.semantics.lean_net.check(source, path) does both steps.

Imports

The sub-package __init__.py files are empty. The only re-exports are Program, Value and azx of archytaszx.embed, 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.