Depth Hierarchies for Symmetric Algebraic Circuits
No public endorsements yet.
Loading review…
Sign in with ORCIDAbstract
This submission formalises a depth hierarchy theorem for matrix-symmetric algebraic circuits, together with the characterisation of bounded-depth matrix-symmetric circuits by homomorphism polynomials on which it rests. A circuit with variables for is matrix-symmetric if every permutation of rows and columns extends to an automorphism of the circuit. Its orbit size is the maximum size of an orbit of gates under these automorphisms, its support size is the least such that every gate is fixed by the pointwise stabiliser of some set of at most rows and columns, and its support depth is the maximum number of wires along a path at which the minimal support of a gate is not contained in that of its parent.
Depth hierarchy. For , let be the full -ary tree of depth , viewed as a bipartite pattern. Over a field of characteristic zero, for , every reduced matrix-symmetric circuit of support depth at most computing the homomorphism polynomial has orbit size at least , whereas for it is computed by a reduced matrix-symmetric circuit of support depth at most and orbit size at most .
Characterisation. The patterns are measured by their -forestwidth , the least width of a tree decomposition of of depth at most with an empty root bag, a variant of the -treewidth of Bhargav, Chen, Curticapean, and Dwivedi. For , , and , a polynomial in the matrix variables is computed by a reduced matrix-symmetric circuit of support size at most and support depth at most if, and only if, is a linear combination of homomorphism polynomials of bipartite multigraphs with . One direction is an explicit circuit construction for a single pattern, which additionally bounds orbit size, depth, and size; the other extracts homomorphism polynomials from a circuit by induction on its gates. Reduced matrix-symmetric circuits are shown to be rigid, and every matrix-symmetric circuit is shown to admit a reduced one computing the same polynomial without increasing size, depth, or orbit size.
Further ingredients. The lower bound combines the characterisation with two further results, both proved here. The first is a support theorem: for and , a reduced matrix-symmetric circuit of orbit size less than has support size at most . It is derived from a self-contained proof, for , of the theorem of Dixon and Mortimer that a subgroup of of small index contains the pointwise stabiliser of a small set in the alternating group, via Bochert's bound on bases of groups without 3-cycles, an analysis of orbits and block systems, and the simplicity of the alternating group. The second is a non-uniform homomorphism distinguishing closure result: if a graph class contains and is closed under minors and under Roberson's weak oddomorphisms, is connected, and is a minor of the underlying graph of , then is not in the linear span of the homomorphism polynomials of patterns in for every at least the size of a CFI graph of . Its proof uses CFI graphs, a contraction formula for homomorphism counts, and a lifting of minor models.
Concepts
- thm✓
BoundedDepthCharacterisation - thm✓
CircuitsForPatterns - thm✓
DepthHierarchy - thm✓
DixonMortimer - thm✓
NonUniformClosure - thm✓
PatternsFromCircuits - thm✓
SupportTheorem - lem✓
ReducedRigid - lem✓
Rigidification
- def
Circuits - def
Forestwidth - def
HomomorphismPolynomials - def
MatrixSymmetry - def
Oddomorphisms - def
Supports
Concept map
Proofs
Proof networkview on GitHub
Proof list
Lean sources for these proofs: proofs/ on GitHub
Proof code is not displayed; the archive records each proof's checked relationship between claims.
Related submissions
Submission map
Cite this
This is only the formalizers. The authors of the formalized results may be different (see References).
@misc{lax-461425,
author = {Anuj Dawar and Prateek Dwivedi and Benedikt Pago and Tim Seppelt},
title = {Depth Hierarchies for Symmetric Algebraic Circuits},
year = {2026},
howpublished = {Lax Archive, lax-461425},
url = {https://laxarchive.org/lax-461425/},
note = {draft},
}
References
- Anuj Dawar and Gregory Wilsenach. Symmetric Arithmetic Circuits. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) 168:36:1–36:18, 2020. doi:10.4230/LIPIcs.ICALP.2020.36
- Anuj Dawar, Benedikt Pago and Tim Seppelt. Symmetric Algebraic Circuits and Homomorphism Polynomials. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026) 362:46:1–46:15, 2026. doi:10.4230/LIPIcs.ITCS.2026.46
- Prateek Dwivedi, Benedikt Pago and Tim Seppelt. Lower Bounds in Algebraic Complexity via Symmetry and Homomorphism Polynomials. In Proceedings of the 58th Annual ACM Symposium on Theory of Computing (STOC 2026) 631–640, 2026. doi:10.1145/3798129.3800779
- C. S. Bhargav, Shiteng Chen, Radu Curticapean and Prateek Dwivedi. Monotone Bounded-Depth Complexity of Homomorphism Polynomials. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) 345:19:1–19:18, 2025. doi:10.4230/LIPIcs.MFCS.2025.19
- John D. Dixon and Brian Mortimer. Permutation Groups. Springer 163, 1996.
- David E. Roberson. Oddomorphisms and homomorphism indistinguishability over graphs of bounded degree. Journal of Combinatorial Theory, Series B 181:1–61, 2026. doi:10.1016/j.jctb.2026.07.003
- Jin-Yi Cai, Martin Fürer and Neil Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica 12(4):389–410, 1992. doi:10.1007/BF01305232
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments