While this submission is a draft, it cannot be used by other submissions.

Characterisation of symmetric VP

Lax461425.SymmetricVPCharacterisation · concepts/Lax461425/SymmetricVPCharacterisation.lean · lax-461425

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Over a field of characteristic zero, a family of polynomials (pn)(p_n) is computed by matrix-symmetric circuits of polynomial orbit size if, and only if, there is a constant kk such that every pnp_n is a linear combination of homomorphism polynomials hom⁡F,n\hom_{F,n} of patterns FF of treewidth at most kk. 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
    20 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitHub

    1import Lax461425.SymmetricClasses
    2import Lax461425.PatternWidths
    3import Lax461425.BoundedDepthCharacterisation
    4import Lax461425.TreewidthForestwidth
    5import Lax461425.SupportTheorem
    6import Lax461425.Rigidification
    7import Lax461425.HomomorphismSpanning
    8import Mathlib.LinearAlgebra.Span.Defs
    9
    10/-!
    11---
    12title: Characterisation of symmetric VP
    13type: theorem
    14---
    15Over a field of characteristic zero, a family of polynomials (pn)(p_n) is computed by
    16matrix-symmetric circuits of polynomial orbit size if, and only if, there is a constant kk
    17such that every pnp_n is a linear combination of homomorphism polynomials hom⁡F,n\hom_{F,n} of
    18patterns FF of treewidth at most kk. This is the main result of Dawar, Pago, and Seppelt
    19(ITCS 2026). It follows from the characterisation of bounded-depth matrix-symmetric circuits,
    20as every circuit has finite support depth and every tree decomposition has finite depth.
    21-/
    22
    23namespace Lax461425.SymmetricVPCharacterisation
    24
    25open SymmetricFamilies SymmetricClasses HomomorphismPolynomials PatternWidths
    26
    27/-- `symVP` consists of the families spanned by homomorphism polynomials of patterns of
    28bounded treewidth. -/
    29axiom 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
    33end Lax461425.SymmetricVPCharacterisation
    34
    Show Proof

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…