Lax Lean Archive

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

Circuits for patterns of bounded forestwidth

Lax461425.CircuitsForPatterns · concepts/Lax461425/CircuitsForPatterns.lean · lax-461425

proven

Loading review…

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

    Let Δ≥1\Delta \geq 1, k≥2k \geq 2, and n≥2k+1n \geq 2k + 1. Let FF be a pattern with fwΔ(F)≤k−1\mathrm{fw}_\Delta(F) \leq k - 1. Then hom⁡F,n\hom_{F,n} is computed by a reduced matrix-symmetric circuit of support size ≤k\leq k, support depth ≤Δ\leq \Delta, orbit size ≤nk\leq n^k, depth ≤2Δ+1\leq 2\Delta + 1, and size ≤5nk(∣V(F)∣+∣E(F)∣)+1\leq 5 n^k (|V(F)| + |E(F)|) + 1, where ∣E(F)∣|E(F)| counts edges with multiplicity.

    Concept map
    6 concepts
    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.Supports
    2import Lax461425.Forestwidth
    3
    4/-!
    5---
    6title: Circuits for patterns of bounded forestwidth
    7type: theorem
    8---
    9Let Δ≥1\Delta \geq 1, k≥2k \geq 2, and n≥2k+1n \geq 2k + 1. Let FF be a pattern with
    10fwΔ(F)≤k−1\mathrm{fw}_\Delta(F) \leq k - 1. Then hom⁡F,n\hom_{F,n} is computed by a reduced
    11matrix-symmetric circuit of support size ≤k\leq k, support depth ≤Δ\leq \Delta, orbit size
    12≤nk\leq n^k, depth ≤2Δ+1\leq 2\Delta + 1, and size ≤5nk(∣V(F)∣+∣E(F)∣)+1\leq 5 n^k (|V(F)| + |E(F)|) + 1, where
    13∣E(F)∣|E(F)| counts edges with multiplicity.
    14-/
    15
    16namespace Lax461425.CircuitsForPatterns
    17
    18open Circuits MatrixSymmetry Supports HomomorphismPolynomials Forestwidth
    19
    20/-- The homomorphism polynomial of a pattern of `Δ`-forestwidth at most `k - 1` is computed by a
    21reduced matrix-symmetric circuit of support size `≤ k`, support depth `≤ Δ`, orbit size
    22`≤ n ^ k`, depth `≤ 2Δ + 1`, and size `≤ 5 n ^ k (|V(F)| + |E(F)|) + 1`. -/
    23axiom exists_circuit {K : Type*} [Field K] [CharZero K] {Δ k n : ℕ} (hΔ : 1 ≤ Δ) (hk : 2 ≤ k)
    24 (hn : 2 * k + 1 ≤ n) (F : Pattern) (hF : ForestwidthLE Δ (k - 1) F) :
    25 ∃ C : Circuit (Fin n × Fin n) K,
    26 C.Computes (hom K F n) ∧ C.IsReduced ∧ IsMatrixSymmetric C ∧
    27 supportSize C ≤ k ∧
    28 supportDepth C ≤ Δ ∧
    29 orbitSize C ≤ n ^ k ∧
    30 C.depth ≤ 2 * Δ + 1 ∧
    31 C.size ≤ 5 * n ^ k * (Fintype.card F.A + Fintype.card F.B + ∑ a, ∑ b, F.mult a b) + 1
    32
    33end Lax461425.CircuitsForPatterns
    34
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…