Symmetric formulas for patterns of bounded treedepth
Lax461425.FormulasForPatterns · concepts/Lax461425/FormulasForPatterns.lean · lax-461425
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Over a field of characteristic zero, for and every pattern of treedepth at most , the homomorphism polynomial is computed by a matrix-symmetric formula of orbit size at most .
For an elimination forest of height at most , the formula has a sum gate for every vertex and every assignment of values in to the proper ancestors of . It sums over the values of the product of the edge variables from to its ancestors and of the sum gates of the children of . 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 , and input gates lie in orbits of size at most .
Concept map
Lean source view on GitHub
| 1 | import Lax461425.PatternWidths |
| 2 | import Lax461425.CircuitProperties |
| 3 | import Lax461425.MatrixSymmetry |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Symmetric formulas for patterns of bounded treedepth |
| 8 | type: theorem |
| 9 | --- |
| 10 | Over a field of characteristic zero, for and every pattern of treedepth at most |
| 11 | , the homomorphism polynomial is computed by a matrix-symmetric formula of |
| 12 | orbit size at most . |
| 13 | |
| 14 | For an elimination forest of height at most , the formula has a sum gate for every vertex |
| 15 | and every assignment of values in to the proper ancestors of . It sums over the |
| 16 | values of the product of the edge variables from to its ancestors and of the sum gates |
| 17 | of the children of . Parallel edges are multiplied out one at a time. Each copy of a |
| 18 | subformula is multiplied by its own pair of mutually inverse constants, which are chosen |
| 19 | distinct and different from all other constants, so that automorphisms cannot exchange copies. |
| 20 | Hence every internal gate lies in an orbit of size at most , and input gates lie in orbits |
| 21 | of size at most . |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax461425.FormulasForPatterns |
| 25 | |
| 26 | open Circuits CircuitProperties MatrixSymmetry HomomorphismPolynomials PatternWidths |
| 27 | |
| 28 | /-- The homomorphism polynomial of a pattern of treedepth at most `t` has a matrix-symmetric |
| 29 | formula of orbit size at most `n ^ (t + 2)`. -/ |
| 30 | axiom 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 | |
| 35 | end Lax461425.FormulasForPatterns |
| 36 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments