Characterisation of symmetric VP
Lax461425.SymmetricVPCharacterisation · concepts/Lax461425/SymmetricVPCharacterisation.lean · lax-461425
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Over a field of characteristic zero, a family of polynomials is computed by matrix-symmetric circuits of polynomial orbit size if, and only if, there is a constant such that every is a linear combination of homomorphism polynomials of patterns of treewidth at most . This is the main result of Dawar, Pago, and Seppelt (ITCS 2026). It follows from the characterisation of bounded-depth matrix-symmetric circuits, as every circuit has finite support depth and every tree decomposition has finite depth.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax461425.SymmetricClasses |
| 2 | import Lax461425.PatternWidths |
| 3 | import Lax461425.BoundedDepthCharacterisation |
| 4 | import Lax461425.TreewidthForestwidth |
| 5 | import Lax461425.SupportTheorem |
| 6 | import Lax461425.Rigidification |
| 7 | import Lax461425.HomomorphismSpanning |
| 8 | import Mathlib.LinearAlgebra.Span.Defs |
| 9 | |
| 10 | /-! |
| 11 | --- |
| 12 | title: Characterisation of symmetric VP |
| 13 | type: theorem |
| 14 | --- |
| 15 | Over a field of characteristic zero, a family of polynomials is computed by |
| 16 | matrix-symmetric circuits of polynomial orbit size if, and only if, there is a constant |
| 17 | such that every is a linear combination of homomorphism polynomials of |
| 18 | patterns of treewidth at most . This is the main result of Dawar, Pago, and Seppelt |
| 19 | (ITCS 2026). It follows from the characterisation of bounded-depth matrix-symmetric circuits, |
| 20 | as every circuit has finite support depth and every tree decomposition has finite depth. |
| 21 | -/ |
| 22 | |
| 23 | namespace Lax461425.SymmetricVPCharacterisation |
| 24 | |
| 25 | open SymmetricFamilies SymmetricClasses HomomorphismPolynomials PatternWidths |
| 26 | |
| 27 | /-- `symVP` consists of the families spanned by homomorphism polynomials of patterns of |
| 28 | bounded treewidth. -/ |
| 29 | axiom characterisation {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K) : |
| 30 | InSymVP f ↔ ∃ k : ℕ, ∀ n, |
| 31 | f n ∈ Submodule.span K {q | ∃ F : Pattern, TreewidthLE k F ∧ hom K F n = q} |
| 32 | |
| 33 | end Lax461425.SymmetricVPCharacterisation |
| 34 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments