Lax Lean Archive

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

Symmetric complexity classes

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

definition

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

    Definition

    Families computed by matrix-symmetric circuits with polynomially bounded gate orbits. Polynomial bounds allow a constant factor and use n+1n + 1, including the zero-size matrix.

    Concept map
    5 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax461425.CircuitProperties
    2import Lax461425.MatrixSymmetry
    3import Lax461425.SymmetricFamilies
    4
    5open Lax461425.CircuitProperties
    6
    7/-!
    8---
    9title: Symmetric complexity classes
    10type: definition
    11---
    12Families computed by matrix-symmetric circuits with polynomially bounded gate orbits.
    13Polynomial bounds allow a constant factor and use `n + 1`, including the zero-size matrix.
    14-/
    15
    16namespace Lax461425.SymmetricClasses
    17
    18open Circuits MatrixSymmetry SymmetricFamilies
    19
    20/-- A polynomial bound, including finitely many exceptional indices. -/
    21def PolynomiallyBounded (q : ℕ → ℕ) : Prop :=
    22 ∃ c d : ℕ, ∀ n, q n ≤ c * (n + 1) ^ d
    23
    24/-- Polynomial gate-orbit witnesses satisfying an additional circuit property. -/
    25def InSymClass {K : Type*} [CommSemiring K]
    26 (P : ∀ n, Circuit (Fin n × Fin n) K → Prop) (f : MatrixFamily K) : Prop :=
    27 ∃ b : ℕ → ℕ, PolynomiallyBounded b ∧ ∀ n, ∃ C : Circuit (Fin n × Fin n) K,
    28 C.Computes (f n) ∧ IsMatrixSymmetric C ∧ MatrixSymmetry.orbitSize C ≤ b n ∧ P n C
    29
    30/-- Symmetric polynomial-orbit circuits. No degree or total-size bound is imposed. -/
    31def InSymVP {K : Type*} [CommSemiring K] (f : MatrixFamily K) : Prop :=
    32 InSymClass (fun _ _ => True) f
    33
    34/-- Symmetric polynomial-orbit skew circuits. -/
    35def InSymVS {K : Type*} [CommSemiring K] (f : MatrixFamily K) : Prop :=
    36 InSymClass (fun _ C => IsSkew C) f
    37
    38/-- Symmetric polynomial-orbit formulas. -/
    39def InSymVF {K : Type*} [CommSemiring K] (f : MatrixFamily K) : Prop :=
    40 InSymClass (fun _ C => IsFormula C) f
    41
    42end Lax461425.SymmetricClasses
    43
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…