From 7a90e8914bb0c58e005b63a8ef1349858dd92bae Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:38:40 -0400 Subject: [PATCH 1/2] feat(arithmetic): certify Ryser witnesses for permanent VNP membership --- Complexity.lean | 2 + .../Circuit/Arithmetic/Permanent.lean | 222 ++++++++++++++++++ Complexity/Foundations/Data/Matrix/Ryser.lean | 160 +++++++++++++ ComplexityTests/PermanentVNP.lean | 73 ++++++ 4 files changed, 457 insertions(+) create mode 100644 Complexity/Computability/Circuit/Arithmetic/Permanent.lean create mode 100644 Complexity/Foundations/Data/Matrix/Ryser.lean create mode 100644 ComplexityTests/PermanentVNP.lean diff --git a/Complexity.lean b/Complexity.lean index d8bc086f06..3277bcff8e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -513,6 +513,7 @@ public import Complexity.Computability.Circuit.Arithmetic.GeneralLowerBound public import Complexity.Computability.Circuit.Arithmetic.Hessian public import Complexity.Computability.Circuit.Arithmetic.Hessian.SourceComplexity public import Complexity.Computability.Circuit.Arithmetic.Pairing +public import Complexity.Computability.Circuit.Arithmetic.Permanent public import Complexity.Computability.Circuit.Arithmetic.Power public import Complexity.Computability.Circuit.Arithmetic.RelativeRank public import Complexity.Computability.Circuit.Arithmetic.RelativeRankUpper @@ -2617,6 +2618,7 @@ public import Complexity.Foundations.Data.Matrix.IntegerBits public import Complexity.Foundations.Data.Matrix.PairChunks public import Complexity.Foundations.Data.Matrix.Permanent public import Complexity.Foundations.Data.Matrix.Reindex +public import Complexity.Foundations.Data.Matrix.Ryser public import Complexity.Foundations.Data.Matrix.TotallyRegular public import Complexity.Foundations.Data.MvPolynomial.AffineTaylor public import Complexity.Foundations.Data.MvPolynomial.Catalecticant diff --git a/Complexity/Computability/Circuit/Arithmetic/Permanent.lean b/Complexity/Computability/Circuit/Arithmetic/Permanent.lean new file mode 100644 index 0000000000..8cb41c7fc0 --- /dev/null +++ b/Complexity/Computability/Circuit/Arithmetic/Permanent.lean @@ -0,0 +1,222 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Arithmetic.Determinant +public import Complexity.Computability.Circuit.Arithmetic.VNP +import Complexity.Foundations.Data.Matrix.Ryser +import Complexity.Foundations.Data.Nat.PolynomialBound.Closure + +/-! +# The permanent belongs to VNP + +The permanent family `permFamily K` belongs to the existing nonuniform class `VNP K` over every +commutative ring `K`. Its witness is the inner polynomial of Ryser's formula +[Schauz, Theorem 1.2, p. 3][Schauz2006]: + +`(∏ j, (2 * Y j - 1)) * ∏ i, ∑ j, Y j * X (i, j)`. + +The first `n * n` variables are matrix entries in row-major order; the last `n` are Boolean +column selectors. The witness has degree at most `3 * n` and an arithmetic circuit with at most +`2 * n ^ 2 + 4 * n + 5` gates, constants included. Substituting Boolean selectors and summing +with the existing `booleanSum` yields the generic permanent as a formal polynomial. No field, +nontriviality or characteristic assumption is needed. + +The witness is certified through the existing synthesis API. Only nonuniform circuit existence +and gate counts are proved; construction runtime is not certified. Valiant's VNP-hardness of +the permanent, including its restriction on characteristic, remains unproved here. + +## Main definitions + +* `Cslib.Circuits.Arithmetic.ryserPoly`: the explicit witness polynomial. + +## Main results + +* `Cslib.Circuits.Arithmetic.totalDegree_ryserPoly_le`: degree at most `3 * n`. +* `Cslib.Circuits.Arithmetic.exists_circuit_ryserPoly`: a quadratic gate bound for the witness. +* `Cslib.Circuits.Arithmetic.booleanSum_ryserPoly`: summing over selectors gives the permanent. +* `Cslib.Circuits.Arithmetic.permFamily_mem_VNP`: the permanent family is in `VNP`. + +## References + +* [U. Schauz, *Colorings and orientations of matrices and graphs*][Schauz2006], Theorem 1.2 +* [L. G. Valiant, *Completeness classes in algebra*][Valiant1979Algebra] + +The witness and Boolean substitution proof adapt the saved Complexitylib development at +revision `5b8acca7`; the synthesis proof and explicit gate bound are new. +-/ + +@[expose] public section + +namespace Cslib.Circuits.Arithmetic + +open MvPolynomial Finset + +universe u + +variable {R : Type u} [CommRing R] + +/-- The inner polynomial of Ryser's formula in `n * n + n` variables: the first `n * n` variables +are the entries of `genericMatrix R n` and the last `n` variables are `{0, 1}`-valued column +indicators. -/ +noncomputable def ryserPoly (R : Type u) [CommRing R] (n : ℕ) : + MvPolynomial (Fin (n * n + n)) R := + (∏ j : Fin n, (2 * X (Fin.natAdd (n * n) j) - 1)) * + ∏ i : Fin n, ∑ j : Fin n, + X (Fin.natAdd (n * n) j) * X (Fin.castAdd n (finProdFinEquiv (i, j))) + +private theorem totalDegree_X_le' {σ : Type*} (i : σ) : + (X i : MvPolynomial σ R).totalDegree ≤ 1 := + (totalDegree_monomial_le _ _).trans (by simp) + +/-- The Ryser inner polynomial has total degree at most `3 * n`. -/ +theorem totalDegree_ryserPoly_le (n : ℕ) : (ryserPoly R n).totalDegree ≤ 3 * n := by + rw [ryserPoly] + refine (totalDegree_mul _ _).trans ?_ + have h1 : (∏ j : Fin n, (2 * X (Fin.natAdd (n * n) j) - 1 : + MvPolynomial (Fin (n * n + n)) R)).totalDegree ≤ n := by + refine (totalDegree_finsetProd _ _).trans ?_ + calc _ ≤ ∑ _j : Fin n, 1 := Finset.sum_le_sum fun j _ => ?_ + _ = n := by simp + rw [sub_eq_add_neg, show (2 : MvPolynomial (Fin (n * n + n)) R) = C 2 from (map_ofNat C 2).symm] + refine (totalDegree_add _ _).trans (max_le ?_ ?_) + · exact (totalDegree_mul _ _).trans (by simpa using totalDegree_X_le' _) + · rw [← map_one C, ← map_neg C, totalDegree_C] + omega + have h2 : (∏ i : Fin n, ∑ j : Fin n, + (X (Fin.natAdd (n * n) j) * X (Fin.castAdd n (finProdFinEquiv (i, j))) : + MvPolynomial (Fin (n * n + n)) R)).totalDegree ≤ 2 * n := by + refine (totalDegree_finsetProd _ _).trans ?_ + calc _ ≤ ∑ _i : Fin n, 2 := Finset.sum_le_sum fun i _ => ?_ + _ = 2 * n := by simp [mul_comm] + refine totalDegree_finsetSum_le fun j _ => ?_ + refine (totalDegree_mul _ _).trans ?_ + exact Nat.add_le_add (totalDegree_X_le' _) (totalDegree_X_le' _) + omega + +/-- The polynomial family of Ryser inner polynomials over `R`. -/ +private noncomputable def ryserFamily (R : Type u) [CommRing R] : PolynomialFamily R where + vars n := n * n + n + poly n := ryserPoly R n + +/-- The Ryser inner polynomial family is a p-family. -/ +private theorem isPFamily_ryserFamily : (ryserFamily R).IsPFamily := + ⟨(PolynomiallyBounded.id.mul PolynomiallyBounded.id).add PolynomiallyBounded.id, + ((PolynomiallyBounded.const 3).mul PolynomiallyBounded.id).mono_of_le + (totalDegree_ryserPoly_le (R := R))⟩ + +private noncomputable abbrev interp (n : ℕ) := + arithInterpretationWith R (C : R → MvPolynomial (Fin n) R) + +private theorem synthesis_prod {N : ℕ} + {s : Set ((Fin N → MvPolynomial (Fin N) R) → MvPolynomial (Fin N) R)} + {ι : Type*} (indices : Finset ι) + (factor : ι → (Fin N → MvPolynomial (Fin N) R) → MvPolynomial (Fin N) R) + (cost : ι → ℕ) (hone : (fun _ => 1) ∈ s) + (h : ∀ i ∈ indices, Synthesis (interp (R := R) N) s {factor i} (cost i)) : + Synthesis (interp (R := R) N) s {fun x => ∏ i ∈ indices, factor i x} + (∑ i ∈ indices, (cost i + 1)) := by + have := Synthesis.finset_fold (· * ·) 1 + (fun f g => Synthesis.arith_mul (Set.mem_insert f {g}) (Set.mem_insert_of_mem f rfl)) + indices (Synthesis.of_mem hone) h + simpa only [Finset.prod_eq_fold, Nat.add_zero] using this + +private noncomputable abbrev witness (n : ℕ) + (x : Fin (n * n + n) → MvPolynomial (Fin (n * n + n)) R) := + (∏ j : Fin n, (C 2 * x (Fin.natAdd (n * n) j) + C (-1))) * + ∏ i : Fin n, ∑ j : Fin n, + x (Fin.natAdd (n * n) j) * x (Fin.castAdd n (finProdFinEquiv (i, j))) + +private theorem witness_X (n : ℕ) : witness (R := R) n X = ryserPoly R n := by + simp only [witness, ryserPoly, map_ofNat, map_neg, map_one, sub_eq_add_neg] + +private theorem synthesis_ryserPoly (n : ℕ) : + Synthesis (interp (R := R) (n * n + n)) (inputs (n * n + n)) {witness (R := R) n} + (2 * n ^ 2 + 4 * n + 5) := by + let constants : Set ((Fin (n * n + n) → MvPolynomial (Fin (n * n + n)) R) → + MvPolynomial (Fin (n * n + n)) R) := + (({fun _ => 0} ∪ {fun _ => 1}) ∪ {fun _ => C 2}) ∪ {fun _ => C (-1)} + let s := inputs (n * n + n) ∪ constants + have h0 : (fun _ => 0) ∈ s := by simp [s, constants] + have h1 : (fun _ => 1) ∈ s := by simp [s, constants] + have h2 : (fun _ => C (2 : R)) ∈ s := by simp [s, constants] + have hn : (fun _ => C (-1 : R)) ∈ s := by simp [s, constants] + have hx (i : Fin (n * n + n)) : (fun x => x i) ∈ s := Or.inl ⟨i, rfl⟩ + have hsign (j : Fin n) : Synthesis (interp (R := R) (n * n + n)) s + {fun x => C 2 * x (Fin.natAdd (n * n) j) + C (-1)} 2 := by + have hmul := Synthesis.arith_mul (constant := C) h2 (hx (Fin.natAdd (n * n) j)) + exact hmul.trans (Synthesis.arith_add (Set.mem_union_right _ rfl) + (Set.mem_union_left _ hn)) + have hsigns := synthesis_prod univ _ (fun _ : Fin n => 2) h1 (fun j _ => hsign j) + have hrow (i : Fin n) : Synthesis (interp (R := R) (n * n + n)) s + {fun x => ∑ j : Fin n, + x (Fin.natAdd (n * n) j) * x (Fin.castAdd n (finProdFinEquiv (i, j)))} (2 * n) := by + have := Synthesis.arith_sum (constant := C) univ + (fun j x => x (Fin.natAdd (n * n) j) * x (Fin.castAdd n (finProdFinEquiv (i, j)))) + (fun _ : Fin n => 1) h0 + (fun j _ => Synthesis.arith_mul (hx (Fin.natAdd (n * n) j)) + (hx (Fin.castAdd n (finProdFinEquiv (i, j))))) + simpa only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul, + mul_comm] using this + have hrows := synthesis_prod univ _ (fun _ : Fin n => 2 * n) h1 (fun i _ => hrow i) + have hbody := hsigns.combine hrows + (Synthesis.arith_mul (Set.mem_insert _ _) (Set.mem_insert_of_mem _ rfl)) + have hc0 : Synthesis (interp (R := R) (n * n + n)) (inputs (n * n + n)) {fun _ => 0} 1 := by + simpa only [map_zero] using Synthesis.arith_const (constant := C) (0 : R) + have hc1 : Synthesis (interp (R := R) (n * n + n)) (inputs (n * n + n)) {fun _ => 1} 1 := by + simpa only [map_one] using Synthesis.arith_const (constant := C) (1 : R) + have hc2 : Synthesis (interp (R := R) (n * n + n)) (inputs (n * n + n)) + {fun _ => C (2 : R)} 1 := Synthesis.arith_const 2 + have hcn : Synthesis (interp (R := R) (n * n + n)) (inputs (n * n + n)) + {fun _ => C (-1 : R)} 1 := Synthesis.arith_const (-1) + have hc : Synthesis (interp (R := R) (n * n + n)) (inputs (n * n + n)) constants 4 := + ((hc0.union hc1).union hc2).union hcn + refine (hc.trans hbody).mono Set.Subset.rfl Set.Subset.rfl ?_ + simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul] + nlinarith + +/-- A circuit computing the Ryser witness with at most `2 * n ^ 2 + 4 * n + 5` gates, +including constants. Only nonuniform existence and gate count are certified. -/ +theorem exists_circuit_ryserPoly (n : ℕ) : + ∃ c : Circuit (arithSignature R) (n * n + n) 1, + c.polynomial 0 = ryserPoly R n ∧ c.size ≤ 2 * n ^ 2 + 4 * n + 5 := by + obtain ⟨c, hc, hs⟩ := (synthesis_ryserPoly (R := R) n).exists_circuit_polynomial + exact ⟨c, hc.trans (witness_X n), hs⟩ + +private theorem ryserFamily_mem_VP : ryserFamily R ∈ VP R := + VP.of_synthesis isPFamily_ryserFamily + ((((PolynomiallyBounded.const 2).mul (PolynomiallyBounded.id.pow 2)).add + ((PolynomiallyBounded.const 4).mul PolynomiallyBounded.id)).add (PolynomiallyBounded.const 5)) + (witness (R := R)) witness_X synthesis_ryserPoly + +/-- Summing `ryserPoly R n` over all `{0, 1}` assignments to the `n` indicator variables yields +the permanent of `genericMatrix R n`. -/ +theorem booleanSum_ryserPoly (n : ℕ) : + booleanSum n (ryserPoly R n) = (genericMatrix R n).permanent := by + rw [Matrix.permanent_eq_ryser_bool, booleanSum] + refine Finset.sum_congr rfl fun e _ => ?_ + rw [ryserPoly, map_mul, map_prod, map_prod] + congr 1 + · refine Finset.prod_congr rfl fun j _ => ?_ + rw [map_sub, map_mul, map_ofNat, map_one, projection_X] + simp only [booleanAssignment, Fin.append_right, Sum.elim_inr] + cases e j <;> norm_num + · refine Finset.prod_congr rfl fun i _ => ?_ + rw [map_sum] + refine Finset.sum_congr rfl fun j _ => ?_ + rw [map_mul, projection_X, projection_X] + simp only [booleanAssignment, Fin.append_right, Fin.append_left, Sum.elim_inr, Sum.elim_inl] + cases e j <;> simp [genericMatrix] + +/-- **The permanent family belongs to `VNP`** over every commutative ring `R`. +The witness has `n` selectors and is computed by polynomial-size arithmetic circuits. This +is the membership direction of Valiant's completeness theorem; no hardness is asserted. -/ +theorem permFamily_mem_VNP : permFamily R ∈ VNP R := + ⟨fun n => n, ryserPoly R, ryserFamily_mem_VP, fun n => (booleanSum_ryserPoly n).symm⟩ + +end Cslib.Circuits.Arithmetic diff --git a/Complexity/Foundations/Data/Matrix/Ryser.lean b/Complexity/Foundations/Data/Matrix/Ryser.lean new file mode 100644 index 0000000000..b50e5b783c --- /dev/null +++ b/Complexity/Foundations/Data/Matrix/Ryser.lean @@ -0,0 +1,160 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, next to `LinearAlgebra/Matrix/Permanent`) + +public import Complexity.Init +public import Mathlib.LinearAlgebra.Matrix.Permanent +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Data.Fintype.BigOperators +import Mathlib.Data.Fintype.Pigeonhole + +/-! +# Ryser's Boolean-sum formula for the permanent + +Ryser's inclusion–exclusion identity expresses the permanent as a signed sum over Boolean +column selectors [Schauz, Theorem 1.2, p. 3][Schauz2006]. The sign is the product of `1` for each +selected column and `-1` for each unselected column. Each summand multiplies the selected row +sums. The proof works over every commutative ring, including characteristic two and the zero +ring; Schauz's section-wide convention is an integral domain of characteristic zero. + +The proof expands the row product into a sum over all functions from rows to columns. Summing +the signs cancels every nonsurjective function. On a finite square matrix, the surviving +functions are exactly the permutations. The empty matrix has permanent `1` and contributes +one empty Boolean assignment. + +## Main results + +* `Matrix.permanent_eq_ryser_bool`: Ryser's formula as a sum over `ι → Bool`. + +## References + +* [U. Schauz, *Colorings and orientations of matrices and graphs*][Schauz2006], Theorem 1.2 + +The proof is adapted from the saved Complexitylib development at revision `5b8acca7`. +-/ + +@[expose] public section + +namespace Matrix + +open Equiv Equiv.Perm Finset Fintype + +variable {n : Type*} [Fintype n] [DecidableEq n] {R : Type*} [CommRing R] + +/-- Boolean-indicator form of Ryser's inclusion–exclusion formula for the permanent +[Schauz, Theorem 1.2, p. 3][Schauz2006], generalized to every commutative ring. -/ +theorem permanent_eq_ryser_bool (A : Matrix n n R) : + A.permanent = + ∑ e : n → Bool, + (∏ j : n, if e j then (1 : R) else -1) * + ∏ i : n, ∑ j : n, if e j then A i j else 0 := by + have hprod (e : n → Bool) : + (∏ i : n, ∑ j : n, if e j then A i j else 0) = + ∑ f : n → n, (if ∀ i, e (f i) = true then (1 : R) else 0) * ∏ i : n, A i (f i) := by + rw [Fintype.prod_sum] + refine Finset.sum_congr rfl fun f _ => ?_ + split_ifs with hf + · rw [one_mul] + exact Finset.prod_congr rfl fun i _ => by simp [hf i] + · rw [zero_mul] + push Not at hf + obtain ⟨i, hi⟩ := hf + exact Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi]) + have hstep1 : + (∑ e : n → Bool, + (∏ j : n, if e j then (1 : R) else -1) * + ∏ i : n, ∑ j : n, if e j then A i j else 0) = + ∑ f : n → n, + (∑ e : n → Bool, + (∏ j : n, if e j then (1 : R) else -1) * + (if ∀ i, e (f i) = true then (1 : R) else 0)) * + ∏ i : n, A i (f i) := by + calc _ = ∑ e : n → Bool, ∑ f : n → n, + ((∏ j : n, if e j then (1 : R) else -1) * + (if ∀ i, e (f i) = true then (1 : R) else 0)) * ∏ i : n, A i (f i) := by + refine Finset.sum_congr rfl fun e _ => ?_ + rw [hprod e, Finset.mul_sum] + exact Finset.sum_congr rfl fun f _ => (mul_assoc _ _ _).symm + _ = _ := by + rw [Finset.sum_comm] + exact Finset.sum_congr rfl fun f _ => (Finset.sum_mul _ _ _).symm + rw [hstep1] + have hfactor (f : n → n) (e : n → Bool) : + (∏ j : n, if e j then (1 : R) else -1) * + (if ∀ i, e (f i) = true then (1 : R) else 0) = + ∏ j : n, if e j then (1 : R) else if j ∈ univ.image f then 0 else -1 := by + split_ifs with hf + · rw [mul_one] + refine Finset.prod_congr rfl fun j _ => ?_ + by_cases hej : e j = true + · simp [hej] + · have hj : j ∉ univ.image f := by + intro hmem + obtain ⟨i, _, rfl⟩ := Finset.mem_image.mp hmem + exact hej (hf i) + simp [hej, hj] + · rw [mul_zero] + push Not at hf + obtain ⟨i, hi⟩ := hf + symm + refine Finset.prod_eq_zero (Finset.mem_univ (f i)) ?_ + have hmem : f i ∈ univ.image f := Finset.mem_image_of_mem f (Finset.mem_univ i) + simp [hi, hmem] + have hsum_e (f : n → n) : + (∑ e : n → Bool, + (∏ j : n, if e j then (1 : R) else -1) * + (if ∀ i, e (f i) = true then (1 : R) else 0)) = + if Function.Surjective f then (1 : R) else 0 := by + simp_rw [hfactor] + rw [← Fintype.prod_sum (fun (j : n) (b : Bool) => + if b = true then (1 : R) else if j ∈ univ.image f then 0 else -1)] + have h1 (j : n) : + (∑ b : Bool, if b = true then (1 : R) else if j ∈ univ.image f then 0 else -1) = + if j ∈ univ.image f then (1 : R) else 0 := by + rw [Fintype.sum_bool] + by_cases hj : j ∈ univ.image f <;> simp [hj] + simp_rw [h1] + split_ifs with hsurj + · refine Finset.prod_eq_one fun j _ => ?_ + obtain ⟨i, rfl⟩ := hsurj j + have hmem : f i ∈ univ.image f := Finset.mem_image_of_mem f (Finset.mem_univ i) + simp [hmem] + · unfold Function.Surjective at hsurj + push Not at hsurj + obtain ⟨j, hj⟩ := hsurj + refine Finset.prod_eq_zero (Finset.mem_univ j) ?_ + have hj' : j ∉ univ.image f := by simpa using hj + simp [hj'] + have hstep2 : + (∑ f : n → n, + (∑ e : n → Bool, + (∏ j : n, if e j then (1 : R) else -1) * + (if ∀ i, e (f i) = true then (1 : R) else 0)) * + ∏ i : n, A i (f i)) = + ∑ f : n → n, (if Function.Surjective f then (1 : R) else 0) * ∏ i : n, A i (f i) := + Finset.sum_congr rfl fun f _ => by rw [hsum_e f] + rw [hstep2, ← permanent_transpose, permanent] + have hbij : + (∑ σ : Perm n, ∏ i : n, Aᵀ (σ i) i) = + ∑ f ∈ univ.filter (fun f : n → n => Function.Surjective f), ∏ i : n, A i (f i) := by + refine Finset.sum_bij (fun (σ : Perm n) _ => (σ : n → n)) ?_ ?_ ?_ ?_ + · intro σ _ + exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, σ.surjective⟩ + · intro σ₁ _ σ₂ _ h + exact DFunLike.coe_injective h + · intro f hf + have hsurj : Function.Surjective f := (Finset.mem_filter.mp hf).2 + exact ⟨Equiv.ofBijective f (Finite.surjective_iff_bijective.mp hsurj), + Finset.mem_univ _, rfl⟩ + · intro σ _ + rfl + rw [hbij, Finset.sum_filter] + refine Finset.sum_congr rfl fun f _ => ?_ + split_ifs <;> simp + +end Matrix diff --git a/ComplexityTests/PermanentVNP.lean b/ComplexityTests/PermanentVNP.lean new file mode 100644 index 0000000000..449c7c9e90 --- /dev/null +++ b/ComplexityTests/PermanentVNP.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Circuit.Arithmetic.Permanent +import Complexity.Foundations.Data.Matrix.Permanent +import Mathlib.Algebra.Field.ZMod + +/-! +# Concrete checks for the permanent's VNP witness + +The two-column witness has signed values `0`, `-10`, `-21` and `60` on the four selectors for +`!![2, 3; 5, 7]`, summing to `29`. Its circuit is checked on a nontrivial selector. The empty +matrix and characteristic two test the boundary cases of the ring-general Ryser identity. +-/ + +namespace ComplexityTests.PermanentVNP + +open Cslib Cslib.Circuits Cslib.Circuits.Arithmetic MvPolynomial + +example : booleanSum 0 (ryserPoly ℤ 0) = 1 := by + simp [ryserPoly] + +example : aeval (![2, 3, 5, 7, 0, 0] : Fin 6 → ℤ) (ryserPoly ℤ 2) = 0 := by + norm_num [ryserPoly, Fin.prod_univ_two, Fin.sum_univ_two, finProdFinEquiv, + Fin.natAdd, Fin.castAdd] + +example : aeval (![2, 3, 5, 7, 1, 0] : Fin 6 → ℤ) (ryserPoly ℤ 2) = -10 := by + norm_num [ryserPoly, Fin.prod_univ_two, Fin.sum_univ_two, finProdFinEquiv, + Fin.natAdd, Fin.castAdd] + +example : aeval (![2, 3, 5, 7, 0, 1] : Fin 6 → ℤ) (ryserPoly ℤ 2) = -21 := by + norm_num [ryserPoly, Fin.prod_univ_two, Fin.sum_univ_two, finProdFinEquiv, + Fin.natAdd, Fin.castAdd] + +example : aeval (![2, 3, 5, 7, 1, 1] : Fin 6 → ℤ) (ryserPoly ℤ 2) = 60 := by + norm_num [ryserPoly, Fin.prod_univ_two, Fin.sum_univ_two, finProdFinEquiv, + Fin.natAdd, Fin.castAdd] + +example : aeval (![2, 3, 5, 7] : Fin 4 → ℤ) (booleanSum 2 (ryserPoly ℤ 2)) = 29 := by + rw [booleanSum_ryserPoly, Matrix.permanent_succ_row_zero, + Fin.sum_univ_two, Matrix.permanent_succ_row_zero, Matrix.permanent_succ_row_zero, + Fin.sum_univ_one, Fin.sum_univ_one] + norm_num [Matrix.permanent, genericMatrix, finProdFinEquiv] + +example : ∃ c : Circuit (arithSignature ℤ) 6 1, c.size ≤ 21 ∧ + c.eval (arithInterpretation ℤ) ![2, 3, 5, 7, 1, 0] 0 = -10 := by + obtain ⟨c, hc, hs⟩ := exists_circuit_ryserPoly (R := ℤ) 2 + refine ⟨c, hs, ?_⟩ + rw [← c.eval_polynomial, hc] + norm_num [ryserPoly, Fin.prod_univ_two, Fin.sum_univ_two, finProdFinEquiv, + Fin.natAdd, Fin.castAdd] + +-- In characteristic two the sign factor becomes `1`; membership still concerns formal +-- polynomials, and the Boolean sum has the expected two distinct permutation monomials. +example : booleanSum 2 (ryserPoly (ZMod 2) 2) = + X (0 : Fin 4) * X 3 + X 1 * X 2 := by + rw [booleanSum_ryserPoly, Matrix.permanent_succ_row_zero, + Fin.sum_univ_two, Matrix.permanent_succ_row_zero, Matrix.permanent_succ_row_zero, + Fin.sum_univ_one, Fin.sum_univ_one] + simp [Matrix.permanent, genericMatrix, finProdFinEquiv] + +example : aeval (![1, 1, 1, 1] : Fin 4 → ZMod 2) + (booleanSum 2 (ryserPoly (ZMod 2) 2)) = 0 := by + rw [booleanSum_ryserPoly, Matrix.permanent_succ_row_zero, + Fin.sum_univ_two, Matrix.permanent_succ_row_zero, Matrix.permanent_succ_row_zero, + Fin.sum_univ_one, Fin.sum_univ_one] + norm_num [Matrix.permanent, genericMatrix, finProdFinEquiv] + decide + +end ComplexityTests.PermanentVNP From 396da27b995fd1be6dab34923919d97b4853c70b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:38:40 -0400 Subject: [PATCH 2/2] doc(arithmetic): record the permanent membership milestone --- .../Circuit/Arithmetic/Determinant.lean | 4 ++-- Complexity/Computability/Circuit/Arithmetic/VNP.lean | 3 ++- ROADMAP.md | 10 ++++++---- references.bib | 12 ++++++++++++ 4 files changed, 22 insertions(+), 7 deletions(-) diff --git a/Complexity/Computability/Circuit/Arithmetic/Determinant.lean b/Complexity/Computability/Circuit/Arithmetic/Determinant.lean index 01cf492318..29d6ed3c43 100644 --- a/Complexity/Computability/Circuit/Arithmetic/Determinant.lean +++ b/Complexity/Computability/Circuit/Arithmetic/Determinant.lean @@ -33,8 +33,8 @@ entries, which a sharper count would exploit. Only the gate count is certified; obtained from a synthesis bound, not constructed by a certified uniform procedure. The permanent family `permFamily K` of generic permanents is also a p-family -(`isPFamily_permFamily`). Nothing here places it in `VP` or proves Valiant's `VNP`-completeness of -the permanent. +(`isPFamily_permFamily`). The separate `Arithmetic/Permanent` module proves membership in `VNP`. +Nothing here places it in `VP` or proves Valiant's `VNP`-completeness of the permanent. ## Main definitions diff --git a/Complexity/Computability/Circuit/Arithmetic/VNP.lean b/Complexity/Computability/Circuit/Arithmetic/VNP.lean index 85fd610bc1..04af50f42d 100644 --- a/Complexity/Computability/Circuit/Arithmetic/VNP.lean +++ b/Complexity/Computability/Circuit/Arithmetic/VNP.lean @@ -27,7 +27,8 @@ semiring `K`. A family is *VNP-complete* when it lies in `VNP K` and every family in `VNP K` is a p-projection of it. A VNP-complete family is in `VP` exactly when `VNP ⊆ VP`. Valiant's theorem that the permanent -is VNP-complete over fields of characteristic other than two is not proved here. +is VNP-complete over fields of characteristic other than two is not proved here. The membership +direction, over every commutative ring, is in `Arithmetic/Permanent`. ## Main definitions diff --git a/ROADMAP.md b/ROADMAP.md index 90254e6377..3ca7036450 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -375,10 +375,12 @@ DLOGTIME-uniform AC⁰ under explicit conventions. Corollary 4); the full range of `d`; and the `0/1`-substitution remark. Also the Kabanets–Impagliazzo theorem (a deterministic PIT algorithm implies NEXP ⊄ P/poly or the permanent has no polynomial-size arithmetic circuits); Valiant's VNP-completeness of the permanent over - fields of characteristic other than two; formula and branching-program models, identity testing, - hitting sets, and tensor and rank methods, including partial-derivative measures (Nisan–Wigderson - depth-3 bounds and shifted partials) and the depth-reduction chasms at depth four (Agrawal–Vinay) - and depth three (Gupta–Kamath–Kayal–Saptharishi), with uniform construction costs certified + fields of characteristic other than two (membership now has an explicit Ryser witness over + every commutative ring; VNP-hardness remains open); formula and branching-program models, + identity testing, hitting sets, and tensor and rank methods, including partial-derivative + measures (Nisan–Wigderson depth-3 bounds and shifted partials) and the depth-reduction chasms at + depth four (Agrawal–Vinay) and depth three (Gupta–Kamath–Kayal–Saptharishi), with uniform + construction costs certified separately from gate counts. - **Real-algebraic decision procedures:** port the Sturm–Tarski query evaluator, recursive evaluator, implicit arithmetic, native space certificates and the ETR upper bound from diff --git a/references.bib b/references.bib index 6012526f44..3952905519 100644 --- a/references.bib +++ b/references.bib @@ -3910,6 +3910,18 @@ @article{Schaefer1978 doi = {10.1016/0022-0000(78)90045-4} } +@article{Schauz2006, + author = {Schauz, Uwe}, + title = {Colorings and Orientations of Matrices and Graphs}, + journal = {The Electronic Journal of Combinatorics}, + volume = {13}, + number = {1}, + pages = {R61}, + year = {2006}, + doi = {10.37236/1087}, + url = {https://www.combinatorics.org/ojs/index.php/eljc/article/download/v13i1r61/pdf/} +} + @inproceedings{Scheder2021, author = {Scheder, Dominik}, title = {{PPSZ} is Better Than You Think},