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

Characterisation of symmetric VF

Lax461425.SymmetricVFCharacterisation · concepts/Lax461425/SymmetricVFCharacterisation.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 formulas of polynomial orbit size if, and only if, there is a constant tt such that every pnp_n is a linear combination of homomorphism polynomials hom⁡F,n\hom_{F,n} of patterns FF of treedepth at most tt. 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 Δ\Delta-forestwidth for bounded Δ\Delta amounts to bounded treedepth.

    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.TreedepthForestwidth
    5import Lax461425.FormulaSupportDepth
    6import Lax461425.FormulasForPatterns
    7import Lax461425.HomomorphismSpanning
    8import Mathlib.LinearAlgebra.Span.Defs
    9
    10/-!
    11---
    12title: Characterisation of symmetric VF
    13type: theorem
    14---
    15Over a field of characteristic zero, a family of polynomials (pn)(p_n) is computed by
    16matrix-symmetric formulas of polynomial orbit size if, and only if, there is a constant tt
    17such that every pnp_n is a linear combination of homomorphism polynomials hom⁡F,n\hom_{F,n} of
    18patterns FF of treedepth at most tt. This is a result of Dwivedi, Pago, and Seppelt
    19(STOC 2026). Symmetric formulas have rigidifications of bounded support depth, so it follows
    20from the characterisation of bounded-depth matrix-symmetric circuits, since bounded
    21Δ\Delta-forestwidth for bounded Δ\Delta amounts to bounded treedepth.
    22-/
    23
    24namespace Lax461425.SymmetricVFCharacterisation
    25
    26open SymmetricFamilies SymmetricClasses HomomorphismPolynomials PatternWidths
    27
    28/-- `symVF` consists of the families spanned by homomorphism polynomials of patterns of
    29bounded treedepth. -/
    30axiom 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
    34end Lax461425.SymmetricVFCharacterisation
    35
    Show Proof

    Discussion

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

    Loading discussion…