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

Symmetric formulas for patterns of bounded treedepth

Lax461425.FormulasForPatterns · concepts/Lax461425/FormulasForPatterns.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, for n≥1n \geq 1 and every pattern FF of treedepth at most tt, the homomorphism polynomial hom⁡F,n\hom_{F,n} is computed by a matrix-symmetric formula of orbit size at most nt+2n^{t+2}.

    For an elimination forest of height at most tt, the formula has a sum gate for every vertex vv and every assignment of values in [n][n] to the proper ancestors of vv. It sums over the values of vv the product of the edge variables from vv to its ancestors and of the sum gates of the children of vv. Parallel edges are multiplied out one at a time. Each copy of a subformula is multiplied by its own pair of mutually inverse constants, which are chosen distinct and different from all other constants, so that automorphisms cannot exchange copies. Hence every internal gate lies in an orbit of size at most ntn^t, and input gates lie in orbits of size at most n2n^2.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax461425.PatternWidths
    2import Lax461425.CircuitProperties
    3import Lax461425.MatrixSymmetry
    4
    5/-!
    6---
    7title: Symmetric formulas for patterns of bounded treedepth
    8type: theorem
    9---
    10Over a field of characteristic zero, for n≥1n \geq 1 and every pattern FF of treedepth at most
    11tt, the homomorphism polynomial hom⁡F,n\hom_{F,n} is computed by a matrix-symmetric formula of
    12orbit size at most nt+2n^{t+2}.
    13
    14For an elimination forest of height at most tt, the formula has a sum gate for every vertex
    15vv and every assignment of values in [n][n] to the proper ancestors of vv. It sums over the
    16values of vv the product of the edge variables from vv to its ancestors and of the sum gates
    17of the children of vv. Parallel edges are multiplied out one at a time. Each copy of a
    18subformula is multiplied by its own pair of mutually inverse constants, which are chosen
    19distinct and different from all other constants, so that automorphisms cannot exchange copies.
    20Hence every internal gate lies in an orbit of size at most ntn^t, and input gates lie in orbits
    21of size at most n2n^2.
    22-/
    23
    24namespace Lax461425.FormulasForPatterns
    25
    26open Circuits CircuitProperties MatrixSymmetry HomomorphismPolynomials PatternWidths
    27
    28/-- The homomorphism polynomial of a pattern of treedepth at most `t` has a matrix-symmetric
    29formula of orbit size at most `n ^ (t + 2)`. -/
    30axiom exists_formula {K : Type*} [Field K] [CharZero K] {n t : ℕ} (hn : 1 ≤ n)
    31 (F : Pattern) (hF : TreedepthLE t F) :
    32 ∃ C : Circuit (Fin n × Fin n) K,
    33 C.Computes (hom K F n) ∧ IsFormula C ∧ IsMatrixSymmetric C ∧ orbitSize C ≤ n ^ (t + 2)
    34
    35end Lax461425.FormulasForPatterns
    36
    Show Proof

    Discussion

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

    Loading discussion…