Lax Lean Archive

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

Symmetric depth hierarchy

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

    For Δ,n≥1\Delta, n \geq 1, let TΔ,nT_{\Delta,n} denote the full nn-ary tree of depth Δ\Delta, viewed as a pattern.

    1. For Δ≥1\Delta \geq 1 and n≥20n \geq 20, every matrix-symmetric circuit of support depth ≤Δ\leq \Delta computing hom⁡TΔ,n,n\hom_{T_{\Delta,n},n} has orbit size at leastnlog⁡2n−Δlog⁡2log⁡2n−3.n^{\log_2 n - \Delta \log_2 \log_2 n - 3}.
    2. For Δ≥1\Delta \geq 1 and n≥5n \geq 5, there is a matrix-symmetric circuit of support depth ≤Δ+1\leq \Delta + 1 and orbit size ≤n2\leq n^2 computing hom⁡TΔ,n,n\hom_{T_{\Delta,n},n}.
    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 exists_circuit proven

    2 orbitSize_ge proven

    Lean source view on GitHub

    1import Mathlib.Analysis.SpecialFunctions.Log.Base
    2import Mathlib.Analysis.SpecialFunctions.Pow.Real
    3import Mathlib.Data.Set.Finite.List
    4import Lax461425.Supports
    5import Lax461425.HomomorphismPolynomials
    6
    7/-!
    8---
    9title: Symmetric depth hierarchy
    10type: theorem
    11---
    12For Δ,n≥1\Delta, n \geq 1, let TΔ,nT_{\Delta,n} denote the full nn-ary tree of depth Δ\Delta,
    13viewed as a pattern.
    14
    151. For Δ≥1\Delta \geq 1 and n≥20n \geq 20, every matrix-symmetric circuit of support depth
    16 ≤Δ\leq \Delta computing hom⁡TΔ,n,n\hom_{T_{\Delta,n},n} has orbit size at least
    17
    18nlog⁡2n−Δlog⁡2log⁡2n−3.n^{\log_2 n - \Delta \log_2 \log_2 n - 3}.
    19
    202. For Δ≥1\Delta \geq 1 and n≥5n \geq 5, there is a matrix-symmetric circuit of support depth
    21 ≤Δ+1\leq \Delta + 1 and orbit size ≤n2\leq n^2 computing hom⁡TΔ,n,n\hom_{T_{\Delta,n},n}.
    22
    23-/
    24
    25namespace Lax461425.DepthHierarchy
    26
    27open Circuits MatrixSymmetry Supports HomomorphismPolynomials
    28
    29/-- The words over `Fin n` of length at most `Δ` whose length satisfies `p`. -/
    30abbrev Words (Δ n : ℕ) (p : ℕ → Prop) : Type :=
    31 {w : List (Fin n) // w.length ≤ Δ ∧ p w.length}
    32
    33instance (Δ n : ℕ) (p : ℕ → Prop) : Finite (Words Δ n p) :=
    34 ((List.finite_length_le (Fin n) Δ).subset fun _ hw => hw.1).to_subtype
    35
    36/-- The full `n`-ary tree `T_{Δ,n}` of depth `Δ`: its vertices are the words over `Fin n` of
    37length at most `Δ`, words of even length on the left and of odd length on the right, and a word
    38`w` is adjacent to the words `w ++ [i]`. -/
    39noncomputable def fullTree (Δ n : ℕ) : Pattern where
    40 A := Words Δ n Even
    41 B := Words Δ n Odd
    42 fintypeA := Fintype.ofFinite _
    43 fintypeB := Fintype.ofFinite _
    44 decEqA := inferInstance
    45 decEqB := inferInstance
    46 mult a b := by
    47 classical
    48 exact if (∃ i, b.1 = a.1 ++ [i]) ∨ ∃ i, a.1 = b.1 ++ [i] then 1 else 0
    49
    50/-- Every reduced matrix-symmetric circuit of support depth `≤ Δ` computing `hom_{T_{Δ,n},n}`
    51has orbit size at least `n ^ (log₂ n - Δ log₂ log₂ n - 3)`. -/
    52axiom orbitSize_ge {K : Type*} [Field K] [CharZero K] {Δ n : ℕ} (hΔ : 1 ≤ Δ) (hn : 20 ≤ n)
    53 (C : Circuit (Fin n × Fin n) K) (hC : C.Computes (hom K (fullTree Δ n) n))
    54 (hred : C.IsReduced) (hsym : IsMatrixSymmetric C) (hdepth : supportDepth C ≤ Δ) :
    55 (n : ℝ) ^ (Real.logb 2 n - Δ * Real.logb 2 (Real.logb 2 n) - 3) ≤ orbitSize C
    56
    57/-- `hom_{T_{Δ,n},n}` is computed by a reduced matrix-symmetric circuit of support depth
    58`≤ Δ + 1` and orbit size `≤ n ^ 2`. -/
    59axiom exists_circuit {K : Type*} [Field K] [CharZero K] {Δ n : ℕ} (hΔ : 1 ≤ Δ) (hn : 5 ≤ n) :
    60 ∃ C : Circuit (Fin n × Fin n) K,
    61 C.Computes (hom K (fullTree Δ n) n) ∧ C.IsReduced ∧ IsMatrixSymmetric C ∧
    62 supportDepth C ≤ Δ + 1 ∧ orbitSize C ≤ n ^ 2
    63
    64end Lax461425.DepthHierarchy
    65
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…