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

Symmetric ABP characterisation

Lax461425.SymmetricABPCharacterisation · concepts/Lax461425/SymmetricABPCharacterisation.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

    Families computed by matrix-symmetric ABPs with polynomial vertex orbits and families computed by matrix-symmetric skew circuits with polynomial gate orbits coincide over a field of characteristic zero, that is, symVBP=symVSsymVBP = symVS. The inclusion symVBP⊆symVSsymVBP ⊆ symVS is the theorem on symmetric skew circuits from symmetric ABPs; the reverse inclusion follows from the characterisation of matrix-symmetric skew circuits by bounded-pathwidth patterns.

    Concept map
    23 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitHub

    1import Lax461425.SymmetricABPs
    2import Lax461425.SkewFromABP
    3import Lax461425.ABPsForPatterns
    4import Lax461425.SkewCircuitCharacterisation
    5import Lax461425.HomomorphismSpanning
    6
    7/-!
    8---
    9title: Symmetric ABP characterisation
    10type: theorem
    11---
    12Families computed by matrix-symmetric ABPs with polynomial vertex orbits and families
    13computed by matrix-symmetric skew circuits with polynomial gate orbits coincide over a
    14field of characteristic zero, that is, `symVBP = symVS`. The inclusion `symVBP ⊆ symVS`
    15is the theorem on symmetric skew circuits from symmetric ABPs; the reverse inclusion follows
    16from the characterisation of matrix-symmetric skew circuits by bounded-pathwidth patterns.
    17-/
    18
    19namespace Lax461425.SymmetricABPCharacterisation
    20
    21open SymmetricABPs SymmetricFamilies SymmetricClasses SymmetricVNP
    22
    23/-- Symmetric polynomial-orbit skew-circuit families have symmetric
    24polynomial-orbit ABPs. -/
    25axiom inSymVBP_of_inSymVS {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K)
    26 (hf : InSymVS f) : InSymVBP f
    27
    28/-- Symmetric polynomial-orbit ABPs and skew circuits define the same class. -/
    29axiom characterisation {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K) :
    30 InSymVBP f ↔ InSymVS f
    31
    32end Lax461425.SymmetricABPCharacterisation
    33
    Show ProofShow Proof

    Discussion

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

    Loading discussion…