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

Characterisation of matrix-symmetric skew circuits

Lax461425.SkewCircuitCharacterisation · concepts/Lax461425/SkewCircuitCharacterisation.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 reduced matrix-symmetric skew circuit on an n×nn × n matrix with support size at most kk, where 2≤k2 ≤ k and 2k+1≤n2k + 1 ≤ n, computes a linear combination of homomorphism polynomials of patterns of pathwidth at most 2k2k. Together with symmetric ABPs for patterns of bounded pathwidth, it follows that a family of polynomials (pn)(p_n) is computed by matrix-symmetric skew 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 pathwidth at most kk.

    Concept map
    20 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitHub

    1import Lax461425.SymmetricFamilies
    2import Lax461425.SymmetricClasses
    3import Lax461425.SymmetricVNP
    4import Lax461425.SymmetricABPs
    5import Lax461425.SkewFromABP
    6import Lax461425.PatternWidths
    7import Lax461425.Supports
    8import Lax461425.SupportTheorem
    9import Lax461425.Rigidification
    10import Lax461425.ReducedRigid
    11import Mathlib.LinearAlgebra.Span.Defs
    12
    13/-!
    14---
    15title: Characterisation of matrix-symmetric skew circuits
    16type: theorem
    17---
    18Over a field of characteristic zero, a reduced matrix-symmetric skew circuit on an `n × n`
    19matrix with support size at most `k`, where `2 ≤ k` and `2k + 1 ≤ n`, computes a linear
    20combination of homomorphism polynomials of patterns of pathwidth at most `2k`.
    21Together with symmetric ABPs for patterns of bounded pathwidth, it follows that a family of
    22polynomials (pn)(p_n) is computed by matrix-symmetric skew circuits of polynomial orbit size
    23if, and only if, there is a constant kk such that every pnp_n is a
    24linear combination of homomorphism polynomials hom⁡F,n\hom_{F,n} of patterns FF of pathwidth at
    25most kk.
    26-/
    27namespace Lax461425.SkewCircuitCharacterisation
    28
    29open Circuits CircuitProperties MatrixSymmetry Supports
    30open SymmetricFamilies SymmetricClasses SymmetricVNP SymmetricABPs HomomorphismPolynomials
    31open PatternWidths
    32
    33/-- A bounded-support reduced skew circuit computes a combination of bounded-pathwidth
    34homomorphism polynomials. -/
    35axiom mem_span_hom {K : Type*} [Field K] [CharZero K] {k n : ℕ} (hk : 2 ≤ k)
    36 (hn : 2 * k + 1 ≤ n) (C : Circuit (Fin n × Fin n) K)
    37 (hred : C.IsReduced) (hsym : IsMatrixSymmetric C) (hsize : supportSize C ≤ k)
    38 (hskew : IsSkew C) {p : MatrixPolynomial n K} (hp : C.Computes p) :
    39 p ∈ Submodule.span K {q | ∃ F : Pattern, PathwidthLE (2 * k) F ∧ hom K F n = q}
    40
    41/-- `symVS` consists of the families spanned by homomorphism polynomials of patterns of
    42bounded pathwidth. -/
    43axiom characterisation {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K) :
    44 InSymVS f ↔ ∃ k : ℕ, ∀ n,
    45 f n ∈ Submodule.span K {q | ∃ F : Pattern, PathwidthLE k F ∧ hom K F n = q}
    46
    47end Lax461425.SkewCircuitCharacterisation
    48
    Show ProofShow Proof

    Discussion

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

    Loading discussion…