Lax Lean Archive

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

Symmetric formula witnesses

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

    Over a field of characteristic zero, every matrix-invariant polynomial on an n×nn × n matrix, for n≥1n ≥ 1, is the hypercube sum of a polynomial with 2n22n² auxiliary variables that is computed by a jointly symmetric formula with gate orbits of size at most 4n24n².

    Concept map
    9 concepts; 2 descendants 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.CircuitProperties
    2import Lax461425.SymmetricFamilies
    3import Lax461425.SymmetricClasses
    4import Lax461425.SymmetricVNP
    5import Lax461425.HomomorphismSpanning
    6
    7open Lax461425.CircuitProperties
    8
    9/-!
    10---
    11title: Symmetric formula witnesses
    12type: theorem
    13---
    14Over a field of characteristic zero, every matrix-invariant polynomial on an `n × n`
    15matrix, for `n ≥ 1`, is the hypercube sum of a polynomial with `2n²` auxiliary variables
    16that is computed by a jointly symmetric formula with gate orbits of size at most `4n²`.
    17-/
    18
    19namespace Lax461425.SymmetricFormulaWitness
    20
    21open Circuits MatrixSymmetry SymmetricFamilies SymmetricClasses SymmetricVNP
    22
    23/-- Matrix-invariant polynomials have jointly symmetric formula witnesses with `2n²`
    24auxiliary variables and gate orbits of size at most `4n²`. -/
    25axiom formula_witness {K : Type*} [Field K] [CharZero K] {n : ℕ}
    26 (hn : 1 ≤ n) (p : MatrixPolynomial n K) (hp : MatrixInvariant p) :
    27 ∃ (ρ : Γ n →* Equiv.Perm (Fin (2 * n ^ 2)))
    28 (g : MvPolynomial ((Fin n × Fin n) ⊕ Fin (2 * n ^ 2)) K)
    29 (C : Circuit ((Fin n × Fin n) ⊕ Fin (2 * n ^ 2)) K),
    30 C.Computes g ∧ Symmetric (jointAction ρ) C ∧
    31 orbitSize (jointAction ρ) C ≤ 4 * n ^ 2 ∧ IsFormula C ∧ boolSum g = p
    32
    33end Lax461425.SymmetricFormulaWitness
    34
    Show Proof
    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…