Symmetric VNP and hypercube-sum witnesses
Lax461425.SymmetricVNP · concepts/Lax461425/SymmetricVNP.lean · lax-461425
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The symmetry and orbit definitions below allow a group to act jointly on matrix variables and auxiliary variables. Orbits use every extending circuit automorphism. A family lies in symmetric VNP if it is a sum over the Boolean hypercube of a polynomial computed by such a jointly symmetric circuit with polynomial gate orbits.
Concept map
Lean source view on GitHub
| 1 | import Lax461425.CircuitProperties |
| 2 | import Lax461425.MatrixSymmetry |
| 3 | import Lax461425.SymmetricFamilies |
| 4 | import Lax461425.SymmetricClasses |
| 5 | |
| 6 | open Lax461425.CircuitProperties |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: Symmetric VNP and hypercube-sum witnesses |
| 11 | type: definition |
| 12 | --- |
| 13 | The symmetry and orbit definitions below allow a group to act jointly on matrix variables |
| 14 | and auxiliary variables. Orbits use every extending circuit automorphism. A family lies in |
| 15 | symmetric VNP if it is a sum over the Boolean hypercube of a polynomial computed by such a |
| 16 | jointly symmetric circuit with polynomial gate orbits. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax461425.SymmetricVNP |
| 20 | |
| 21 | open Circuits MatrixSymmetry SymmetricFamilies SymmetricClasses |
| 22 | open scoped Classical |
| 23 | |
| 24 | /-- The permutation action on matrix variables. -/ |
| 25 | def matrixAction (n : ℕ) : Γ n →* Equiv.Perm (Fin n × Fin n) where |
| 26 | toFun γ := Equiv.prodCongr γ.1 γ.2 |
| 27 | map_one' := rfl |
| 28 | map_mul' _ _ := rfl |
| 29 | |
| 30 | /-- The joint action on matrix and auxiliary variables. -/ |
| 31 | def jointAction {n : ℕ} {Y : Type*} (ρ : Γ n →* Equiv.Perm Y) : |
| 32 | Γ n →* Equiv.Perm ((Fin n × Fin n) ⊕ Y) where |
| 33 | toFun γ := Equiv.sumCongr (matrixAction n γ) (ρ γ) |
| 34 | map_one' := by ext x; cases x <;> simp [matrixAction] |
| 35 | map_mul' γ δ := by ext x; cases x <;> simp [matrixAction] |
| 36 | |
| 37 | /-- Sum over Boolean auxiliary assignments; distinct Booleans are counted separately even |
| 38 | in positive characteristic. -/ |
| 39 | noncomputable def boolSum {X Y K : Type*} [Fintype Y] [CommSemiring K] |
| 40 | (g : MvPolynomial (X ⊕ Y) K) : MvPolynomial X K := |
| 41 | ∑ e : Y → Bool, MvPolynomial.eval₂ MvPolynomial.C |
| 42 | (Sum.elim MvPolynomial.X (fun y => MvPolynomial.C (if e y then 1 else 0))) g |
| 43 | |
| 44 | /-- Every element of the acting group extends to a circuit automorphism. -/ |
| 45 | def Symmetric {G V K : Type*} [Group G] (ρ : G →* Equiv.Perm V) |
| 46 | (C : Circuit V K) : Prop := |
| 47 | ∀ γ : G, ∃ σ : C.Gate ≃ C.Gate, Extends C σ (ρ γ) |
| 48 | |
| 49 | /-- Orbit under all automorphisms extending some element of the acting group. -/ |
| 50 | def orbit {G V K : Type*} [Group G] (ρ : G →* Equiv.Perm V) |
| 51 | (C : Circuit V K) (g : C.Gate) : Set C.Gate := |
| 52 | {g' | ∃ (γ : G) (σ : C.Gate ≃ C.Gate), Extends C σ (ρ γ) ∧ σ g = g'} |
| 53 | |
| 54 | /-- The largest gate orbit for a specified variable action. -/ |
| 55 | noncomputable def orbitSize {G V K : Type*} [Group G] (ρ : G →* Equiv.Perm V) |
| 56 | (C : Circuit V K) : ℕ := |
| 57 | Finset.univ.sup fun g => (orbit ρ C g).ncard |
| 58 | |
| 59 | /-- Hypercube-sum witnesses with polynomially many auxiliary variables and polynomial gate |
| 60 | orbits for the joint action. -/ |
| 61 | def InHyperCubeSumClass {K : Type*} [CommSemiring K] |
| 62 | (P : ∀ {V : Type}, Circuit V K → Prop) (f : MatrixFamily K) : Prop := |
| 63 | ∃ q b : ℕ → ℕ, PolynomiallyBounded q ∧ PolynomiallyBounded b ∧ ∀ n, |
| 64 | ∃ (ρ : Γ n →* Equiv.Perm (Fin (q n))) |
| 65 | (g : MvPolynomial ((Fin n × Fin n) ⊕ Fin (q n)) K) |
| 66 | (C : Circuit ((Fin n × Fin n) ⊕ Fin (q n)) K), |
| 67 | C.Computes g ∧ Symmetric (jointAction ρ) C ∧ |
| 68 | orbitSize (jointAction ρ) C ≤ b n ∧ P C ∧ boolSum g = f n |
| 69 | |
| 70 | /-- The symmetric analogue of VNP. -/ |
| 71 | def InSymVNP {K : Type*} [CommSemiring K] (f : MatrixFamily K) : Prop := |
| 72 | InHyperCubeSumClass (fun _ => True) f |
| 73 | |
| 74 | /-- The formula-witness variant of symmetric VNP. -/ |
| 75 | def InSymVNPFormula {K : Type*} [CommSemiring K] (f : MatrixFamily K) : Prop := |
| 76 | InHyperCubeSumClass (fun C => IsFormula C) f |
| 77 | |
| 78 | end Lax461425.SymmetricVNP |
| 79 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments