Characterisation of symmetric VF
Lax461425.SymmetricVFCharacterisation · concepts/Lax461425/SymmetricVFCharacterisation.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 formulas 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 treedepth at most . This is a result of Dwivedi, Pago, and Seppelt (STOC 2026). Symmetric formulas have rigidifications of bounded support depth, so it follows from the characterisation of bounded-depth matrix-symmetric circuits, since bounded -forestwidth for bounded amounts to bounded treedepth.
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.TreedepthForestwidth |
| 5 | import Lax461425.FormulaSupportDepth |
| 6 | import Lax461425.FormulasForPatterns |
| 7 | import Lax461425.HomomorphismSpanning |
| 8 | import Mathlib.LinearAlgebra.Span.Defs |
| 9 | |
| 10 | /-! |
| 11 | --- |
| 12 | title: Characterisation of symmetric VF |
| 13 | type: theorem |
| 14 | --- |
| 15 | Over a field of characteristic zero, a family of polynomials is computed by |
| 16 | matrix-symmetric formulas 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 treedepth at most . This is a result of Dwivedi, Pago, and Seppelt |
| 19 | (STOC 2026). Symmetric formulas have rigidifications of bounded support depth, so it follows |
| 20 | from the characterisation of bounded-depth matrix-symmetric circuits, since bounded |
| 21 | -forestwidth for bounded amounts to bounded treedepth. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax461425.SymmetricVFCharacterisation |
| 25 | |
| 26 | open SymmetricFamilies SymmetricClasses HomomorphismPolynomials PatternWidths |
| 27 | |
| 28 | /-- `symVF` consists of the families spanned by homomorphism polynomials of patterns of |
| 29 | bounded treedepth. -/ |
| 30 | axiom characterisation {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K) : |
| 31 | InSymVF f ↔ ∃ t : ℕ, ∀ n, |
| 32 | f n ∈ Submodule.span K {q | ∃ F : Pattern, TreedepthLE t F ∧ hom K F n = q} |
| 33 | |
| 34 | end Lax461425.SymmetricVFCharacterisation |
| 35 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments