From 5c57ebc0d76306257bbb0e15d96db407d6e58ef2 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:53:50 -0400 Subject: [PATCH 1/2] feat(arithmetic): project arithmetic formulas to generic permanents --- Complexity.lean | 2 + .../Circuit/Arithmetic/Permanent/Formula.lean | 467 ++++++++++++++++++ .../Data/Matrix/Permanent/Blocks.lean | 176 +++++++ ComplexityTests/PermanentFormulas.lean | 88 ++++ 4 files changed, 733 insertions(+) create mode 100644 Complexity/Computability/Circuit/Arithmetic/Permanent/Formula.lean create mode 100644 Complexity/Foundations/Data/Matrix/Permanent/Blocks.lean create mode 100644 ComplexityTests/PermanentFormulas.lean diff --git a/Complexity.lean b/Complexity.lean index 1d5a0e2e38..099b588bca 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.Formula public import Complexity.Computability.Circuit.Arithmetic.Power public import Complexity.Computability.Circuit.Arithmetic.RelativeRank public import Complexity.Computability.Circuit.Arithmetic.RelativeRankUpper @@ -2619,6 +2620,7 @@ public import Complexity.Foundations.Data.Matrix.Binary 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.Permanent.Blocks public import Complexity.Foundations.Data.Matrix.Reindex public import Complexity.Foundations.Data.Matrix.TotallyRegular public import Complexity.Foundations.Data.MvPolynomial.AffineTaylor diff --git a/Complexity/Computability/Circuit/Arithmetic/Permanent/Formula.lean b/Complexity/Computability/Circuit/Arithmetic/Permanent/Formula.lean new file mode 100644 index 0000000000..f618d0ac42 --- /dev/null +++ b/Complexity/Computability/Circuit/Arithmetic/Permanent/Formula.lean @@ -0,0 +1,467 @@ +/- +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.Formula +import Complexity.Foundations.Data.Matrix.Permanent.Blocks + +/-! +# Arithmetic formulas are projections of the permanent + +Every existing arithmetic formula `F : Formula (arithSignature K) n` computes a formal +polynomial that is a projection of the generic permanent of dimension `F.size + 1`. Here `K` +is any commutative semiring and size counts every operation node, including constants, with +input leaves free. Substitution uses the existing `IsProjection`: each matrix entry is a +variable or a scalar, without an extra scalar multiplier on the result. + +This is the permanent's formula-simulation property +[Orzel et al., Definition 1 and Lemma 4][OrzelSrinivasanTavenasYehudayoff2025]. The explicit +linear bound and semiring generality are proved directly. That source uses fields of +characteristic other than two and permits a nonzero scalar multiplier in projections. No +characteristic restriction or multiplier is needed for formula simulation. Valiant's full +VNP-hardness reduction and uniform construction runtime are separate, unproved obligations. + +The private invariant represents a polynomial by a permanent with one distinguished root, +whose internal block has permanent `1`. Addition and multiplication combine two such matrices +with one additional internal vertex. No new formula or complexity-class model is introduced. + +## Main results + +* `Cslib.Circuits.Formula.isProjection_permanent`: dimension `F.size + 1` suffices. +* `Cslib.Circuits.Formula.isProjection_permanent_toCircuit`: the existing formula compiler + computes the same polynomial. +* `Cslib.Circuits.Arithmetic.IsProjection.permanent_mul`: multiply projections by adding dimensions. +* `Cslib.Circuits.Arithmetic.isProjection_permanent_mono`: pad to a larger dimension. + +## References + +* [I. Orzel et al.][OrzelSrinivasanTavenasYehudayoff2025], *The Algebraic Cost of a Boolean Sum*, + Definition 1 (p. 47:3), Lemma 4 (p. 47:4) and projection conventions (p. 47:5) + +The rooted construction and proof adapt saved Complexitylib source at revision `5b8acca7`. +-/ + +@[expose] public section + +namespace Matrix + +open Equiv Equiv.Perm Finset Fintype + +variable {m n : Type*} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] +variable {R : Type*} [CommSemiring R] + +/-- Involution on `(Unit ⊕ m) ⊕ (Unit ⊕ n)` swapping the two root elements `inl (inl ())` and +`inr (inl ())`. -/ +private def swapRootEquiv (m n : Type*) : + ((Unit ⊕ m) ⊕ (Unit ⊕ n)) ≃ ((Unit ⊕ m) ⊕ (Unit ⊕ n)) where + toFun + | .inl (.inl u) => .inr (.inl u) + | .inl (.inr i) => .inl (.inr i) + | .inr (.inl u) => .inl (.inl u) + | .inr (.inr j) => .inr (.inr j) + invFun + | .inl (.inl u) => .inr (.inl u) + | .inl (.inr i) => .inl (.inr i) + | .inr (.inl u) => .inl (.inl u) + | .inr (.inr j) => .inr (.inr j) + left_inv x := by rcases x with (⟨⟨⟩⟩ | i) | (⟨⟨⟩⟩ | j) <;> rfl + right_inv x := by rcases x with (⟨⟨⟩⟩ | i) | (⟨⟨⟩⟩ | j) <;> rfl + +/-- Rooted permanent multiplication block matrix on `Unit ⊕ (m ⊕ (Unit ⊕ n))`. -/ +private def rootedMul (M₁ : Matrix (Unit ⊕ m) (Unit ⊕ m) R) (M₂ : Matrix (Unit ⊕ n) (Unit ⊕ n) R) : + Matrix (Unit ⊕ (m ⊕ (Unit ⊕ n))) (Unit ⊕ (m ⊕ (Unit ⊕ n))) R := + (fromBlocks M₁ 0 (fromBlocks (1 : Matrix Unit Unit R) 0 0 0) M₂).submatrix + (Equiv.sumAssoc Unit m (Unit ⊕ n)).symm + ((Equiv.sumAssoc Unit m (Unit ⊕ n)).symm.trans (swapRootEquiv m n)) + +/-- The permanent of `rootedMul M₁ M₂` is the product of the permanents of `M₁` and `M₂`. -/ +private theorem permanent_rootedMul (M₁ : Matrix (Unit ⊕ m) (Unit ⊕ m) R) + (M₂ : Matrix (Unit ⊕ n) (Unit ⊕ n) R) : + (rootedMul M₁ M₂).permanent = M₁.permanent * M₂.permanent := by + rw [rootedMul, permanent_submatrix_equiv_equiv, permanent_fromBlocks_zero₁₂] + +/-- If the internal blocks of `M₁` and `M₂` have permanent `1`, then so does the internal block of +`rootedMul M₁ M₂`. -/ +private theorem permanent_toBlocks₂₂_rootedMul (M₁ : Matrix (Unit ⊕ m) (Unit ⊕ m) R) + (M₂ : Matrix (Unit ⊕ n) (Unit ⊕ n) R) + (h₁ : M₁.toBlocks₂₂.permanent = 1) (h₂ : M₂.toBlocks₂₂.permanent = 1) : + (rootedMul M₁ M₂).toBlocks₂₂.permanent = 1 := by + have hblk : (rootedMul M₁ M₂).toBlocks₂₂ = + fromBlocks M₁.toBlocks₂₂ (of fun i => Sum.elim (M₁.toBlocks₂₁ i) 0) 0 + (fromBlocks (1 : Matrix Unit Unit R) M₂.toBlocks₁₂ 0 M₂.toBlocks₂₂) := by + ext (i₁ | (⟨⟩ | i₂)) (j₁ | (⟨⟩ | j₂)) <;> rfl + rw [hblk, permanent_fromBlocks_zero₂₁, permanent_fromBlocks_zero₂₁, permanent_one, + h₁, h₂, mul_one, mul_one] + +/-- Rooted permanent addition block matrix on `Unit ⊕ (m ⊕ (Unit ⊕ n))`. -/ +private def rootedAdd (M₁ : Matrix (Unit ⊕ m) (Unit ⊕ m) R) (M₂ : Matrix (Unit ⊕ n) (Unit ⊕ n) R) : + Matrix (Unit ⊕ (m ⊕ (Unit ⊕ n))) (Unit ⊕ (m ⊕ (Unit ⊕ n))) R := + (fromBlocks + M₁ + (fromBlocks M₂.toBlocks₁₁ M₂.toBlocks₁₂ 0 0) + (fromBlocks (1 : Matrix Unit Unit R) 0 0 0) + (fromBlocks (1 : Matrix Unit Unit R) 0 M₂.toBlocks₂₁ M₂.toBlocks₂₂)).submatrix + (Equiv.sumAssoc Unit m (Unit ⊕ n)).symm + (Equiv.sumAssoc Unit m (Unit ⊕ n)).symm + +/-- If the internal blocks of `M₁` and `M₂` have permanent `1`, then so does the internal block of +`rootedAdd M₁ M₂`. -/ +private theorem permanent_toBlocks₂₂_rootedAdd (M₁ : Matrix (Unit ⊕ m) (Unit ⊕ m) R) + (M₂ : Matrix (Unit ⊕ n) (Unit ⊕ n) R) + (h₁ : M₁.toBlocks₂₂.permanent = 1) (h₂ : M₂.toBlocks₂₂.permanent = 1) : + (rootedAdd M₁ M₂).toBlocks₂₂.permanent = 1 := by + have hblk : (rootedAdd M₁ M₂).toBlocks₂₂ = + fromBlocks M₁.toBlocks₂₂ 0 0 + (fromBlocks (1 : Matrix Unit Unit R) 0 M₂.toBlocks₂₁ M₂.toBlocks₂₂) := by + ext (i₁ | (⟨⟩ | i₂)) (j₁ | (⟨⟩ | j₂)) <;> rfl + rw [hblk, permanent_fromBlocks_zero, permanent_fromBlocks_zero₁₂, permanent_one, + h₁, h₂, mul_one, mul_one] + +/-- If the internal blocks of `M₁` and `M₂` have permanent `1`, then the permanent of +`rootedAdd M₁ M₂` is the sum of the permanents of `M₁` and `M₂`. -/ +private theorem permanent_rootedAdd (M₁ : Matrix (Unit ⊕ m) (Unit ⊕ m) R) + (M₂ : Matrix (Unit ⊕ n) (Unit ⊕ n) R) + (h₁ : M₁.toBlocks₂₂.permanent = 1) (h₂ : M₂.toBlocks₂₂.permanent = 1) : + (rootedAdd M₁ M₂).permanent = M₁.permanent + M₂.permanent := by + rw [rootedAdd, permanent_submatrix_equiv] + let B₁ : Matrix ((Unit ⊕ m) ⊕ (Unit ⊕ n)) ((Unit ⊕ m) ⊕ (Unit ⊕ n)) R := + fromBlocks M₁ (fromBlocks M₂.toBlocks₁₁ M₂.toBlocks₁₂ 0 0) 0 + (fromBlocks (1 : Matrix Unit Unit R) 0 M₂.toBlocks₂₁ M₂.toBlocks₂₂) + let B₂ : Matrix ((Unit ⊕ m) ⊕ (Unit ⊕ n)) ((Unit ⊕ m) ⊕ (Unit ⊕ n)) R := + fromBlocks M₁ (fromBlocks M₂.toBlocks₁₁ M₂.toBlocks₁₂ 0 0) + (fromBlocks (1 : Matrix Unit Unit R) 0 0 0) + (fromBlocks (0 : Matrix Unit Unit R) 0 M₂.toBlocks₂₁ M₂.toBlocks₂₂) + rw [permanent_add_of_row_eq _ B₁ B₂ (Sum.inr (Sum.inl ())) + (fun j => by rcases j with (⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂) <;> simp [B₁, B₂]) + (fun i hi j => by + rcases i with (⟨⟨⟩⟩ | i₁) | (⟨⟨⟩⟩ | i₂) + · rcases j with (⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂) <;> rfl + · rcases j with (⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂) <;> rfl + · exact (hi rfl).elim + · rcases j with (⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂) <;> rfl) + (fun i hi j => by + rcases i with (⟨⟨⟩⟩ | i₁) | (⟨⟨⟩⟩ | i₂) + · rcases j with (⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂) <;> rfl + · rcases j with (⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂) <;> rfl + · exact (hi rfl).elim + · rcases j with (⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂) <;> rfl)] + have hB₁ : B₁.permanent = M₁.permanent := by + rw [permanent_fromBlocks_zero₂₁, permanent_fromBlocks_zero₁₂, permanent_one, h₂, mul_one, + mul_one] + have hB₂_swap : B₂.submatrix (swapRootEquiv m n) (Equiv.refl _) = + fromBlocks (fromBlocks (1 : Matrix Unit Unit R) 0 M₁.toBlocks₂₁ M₁.toBlocks₂₂) 0 + (fromBlocks M₁.toBlocks₁₁ M₁.toBlocks₁₂ 0 0) M₂ := by + ext ((⟨⟨⟩⟩ | i₁) | (⟨⟨⟩⟩ | i₂)) ((⟨⟨⟩⟩ | j₁) | (⟨⟨⟩⟩ | j₂)) <;> rfl + have hB₂ : B₂.permanent = M₂.permanent := by + rw [← permanent_submatrix_equiv_equiv (swapRootEquiv m n) (Equiv.refl _), hB₂_swap, + permanent_fromBlocks_zero₁₂, permanent_fromBlocks_zero₁₂, permanent_one, h₁, mul_one, + one_mul] + rw [hB₁, hB₂] + +end Matrix + +namespace Cslib.Circuits.Arithmetic + +open MvPolynomial Finset + +universe u + +variable {K : Type u} [CommSemiring K] {n m : ℕ} {σ : Type*} + +/-- Evaluating the permanent of `genericMatrix K n` at `x` gives the permanent of the matrix of +values `x (finProdFinEquiv (i, j))`. -/ +private theorem aeval_permanent_genericMatrix {A : Type*} [CommSemiring A] [Algebra K A] + (x : Fin (n * n) → A) : + aeval x (genericMatrix K n).permanent = + (Matrix.of fun i j : Fin n => x (finProdFinEquiv (i, j))).permanent := by + rw [AlgHom.map_permanent] + congr 1 + ext i j + simp [genericMatrix] + +/-- Applying a projection `ρ` to `(genericMatrix K m).permanent` gives the permanent of the +specialized matrix. -/ +private theorem projection_permanent_genericMatrix {σ : Type*} (ρ : Fin (m * m) → σ ⊕ K) : + projection ρ (genericMatrix K m).permanent = + (Matrix.of fun i j : Fin m => + Sum.elim X (fun a => C a) (ρ (finProdFinEquiv (i, j)))).permanent := + aeval_permanent_genericMatrix _ + +/-- A polynomial in `MvPolynomial σ K` is a projection substitution entry if it is either a +variable `X i` or a constant `C c`. -/ +private def IsSubstEntry (p : MvPolynomial σ K) : Prop := + ∃ s : σ ⊕ K, Sum.elim X (fun a => C a) s = p + +namespace IsSubstEntry + +private theorem C (c : K) : IsSubstEntry (MvPolynomial.C c : MvPolynomial σ K) := + ⟨Sum.inr c, rfl⟩ + +private theorem X (i : σ) : IsSubstEntry (MvPolynomial.X i : MvPolynomial σ K) := + ⟨Sum.inl i, rfl⟩ + +private theorem zero : IsSubstEntry (0 : MvPolynomial σ K) := + ⟨Sum.inr 0, map_zero _⟩ + +private theorem one : IsSubstEntry (1 : MvPolynomial σ K) := + ⟨Sum.inr 1, map_one _⟩ + +end IsSubstEntry + +/-- A matrix over `MvPolynomial σ K` is a specialization of a generic matrix if every entry is a +variable `X i` or a constant `C c`. -/ +private def IsSubstMatrix {α β : Type*} (M : Matrix α β (MvPolynomial σ K)) : Prop := + ∀ i j, IsSubstEntry (M i j) + +namespace IsSubstMatrix + +private theorem zero {α β : Type*} : IsSubstMatrix (0 : Matrix α β (MvPolynomial σ K)) := + fun _ _ => .zero + +private theorem one {α : Type*} [DecidableEq α] : + IsSubstMatrix (1 : Matrix α α (MvPolynomial σ K)) := + fun i j => by + rw [Matrix.one_apply] + split_ifs <;> [exact .one; exact .zero] + +private theorem fromBlocks {α₁ α₂ β₁ β₂ : Type*} + {A : Matrix α₁ β₁ (MvPolynomial σ K)} {B : Matrix α₁ β₂ (MvPolynomial σ K)} + {C : Matrix α₂ β₁ (MvPolynomial σ K)} {D : Matrix α₂ β₂ (MvPolynomial σ K)} + (hA : IsSubstMatrix A) (hB : IsSubstMatrix B) (hC : IsSubstMatrix C) (hD : IsSubstMatrix D) : + IsSubstMatrix (Matrix.fromBlocks A B C D) := by + rintro (i | i) (j | j) + · exact hA i j + · exact hB i j + · exact hC i j + · exact hD i j + +private theorem submatrix {α β α' β' : Type*} {M : Matrix α β (MvPolynomial σ K)} + (hM : IsSubstMatrix M) (f : α' → α) (g : β' → β) : + IsSubstMatrix (M.submatrix f g) := + fun i j => hM (f i) (g j) + +private theorem toBlocks₁₁ {α₁ α₂ β₁ β₂ : Type*} {M : Matrix (α₁ ⊕ α₂) (β₁ ⊕ β₂) (MvPolynomial σ K)} + (hM : IsSubstMatrix M) : IsSubstMatrix M.toBlocks₁₁ := + fun i j => hM (.inl i) (.inl j) + +private theorem toBlocks₁₂ {α₁ α₂ β₁ β₂ : Type*} {M : Matrix (α₁ ⊕ α₂) (β₁ ⊕ β₂) (MvPolynomial σ K)} + (hM : IsSubstMatrix M) : IsSubstMatrix M.toBlocks₁₂ := + fun i j => hM (.inl i) (.inr j) + +private theorem toBlocks₂₁ {α₁ α₂ β₁ β₂ : Type*} {M : Matrix (α₁ ⊕ α₂) (β₁ ⊕ β₂) (MvPolynomial σ K)} + (hM : IsSubstMatrix M) : IsSubstMatrix M.toBlocks₂₁ := + fun i j => hM (.inr i) (.inl j) + +private theorem toBlocks₂₂ {α₁ α₂ β₁ β₂ : Type*} {M : Matrix (α₁ ⊕ α₂) (β₁ ⊕ β₂) (MvPolynomial σ K)} + (hM : IsSubstMatrix M) : IsSubstMatrix M.toBlocks₂₂ := + fun i j => hM (.inr i) (.inr j) + +private theorem rootedMul {α β : Type*} + {M₁ : Matrix (Unit ⊕ α) (Unit ⊕ α) (MvPolynomial σ K)} + {M₂ : Matrix (Unit ⊕ β) (Unit ⊕ β) (MvPolynomial σ K)} + (h₁ : IsSubstMatrix M₁) (h₂ : IsSubstMatrix M₂) : + IsSubstMatrix (Matrix.rootedMul M₁ M₂) := + (h₁.fromBlocks .zero (IsSubstMatrix.one.fromBlocks .zero .zero .zero) h₂).submatrix _ _ + +private theorem rootedAdd {α β : Type*} + {M₁ : Matrix (Unit ⊕ α) (Unit ⊕ α) (MvPolynomial σ K)} + {M₂ : Matrix (Unit ⊕ β) (Unit ⊕ β) (MvPolynomial σ K)} + (h₁ : IsSubstMatrix M₁) (h₂ : IsSubstMatrix M₂) : + IsSubstMatrix (Matrix.rootedAdd M₁ M₂) := + (h₁.fromBlocks (h₂.toBlocks₁₁.fromBlocks h₂.toBlocks₁₂ .zero .zero) + (IsSubstMatrix.one.fromBlocks .zero .zero .zero) + (IsSubstMatrix.one.fromBlocks .zero h₂.toBlocks₂₁ h₂.toBlocks₂₂)).submatrix _ _ + +/-- The permanent of any specialization matrix indexed by `α ≃ Fin m` is a projection of +`(genericMatrix K m).permanent`. -/ +private theorem isProjection_permanent {α : Type*} [Fintype α] [DecidableEq α] + {M : Matrix α α (MvPolynomial σ K)} (hM : IsSubstMatrix M) {m : ℕ} (e : Fin m ≃ α) : + IsProjection M.permanent (genericMatrix K m).permanent := by + choose ρ hρ using hM + refine ⟨fun idx => + let pq := finProdFinEquiv.symm idx + ρ (e pq.1) (e pq.2), ?_⟩ + rw [projection_permanent_genericMatrix, ← M.permanent_submatrix_equiv e] + exact congrArg Matrix.permanent (Matrix.ext fun i j => by simpa using hρ (e i) (e j)) + +end IsSubstMatrix + +/-- A polynomial `P` is a projection of `(genericMatrix K m).permanent` if and only if it is the +permanent of an `m × m` specialization matrix. -/ +private theorem isProjection_permanent_iff_exists_substMatrix {P : MvPolynomial σ K} {m : ℕ} : + IsProjection P (genericMatrix K m).permanent ↔ + ∃ M : Matrix (Fin m) (Fin m) (MvPolynomial σ K), IsSubstMatrix M ∧ M.permanent = P := by + constructor + · rintro ⟨ρ, rfl⟩ + refine ⟨Matrix.of fun i j => Sum.elim X (fun a => C a) (ρ (finProdFinEquiv (i, j))), + fun i j => ⟨ρ (finProdFinEquiv (i, j)), rfl⟩, + (projection_permanent_genericMatrix ρ).symm⟩ + · rintro ⟨M, hM, rfl⟩ + exact hM.isProjection_permanent (Equiv.refl _) + +/-- The constant polynomial `1` is a projection of the `m × m` generic permanent for every `m`. -/ +private theorem isProjection_permanent_one (m : ℕ) : + IsProjection (1 : MvPolynomial σ K) (genericMatrix K m).permanent := + isProjection_permanent_iff_exists_substMatrix.mpr ⟨1, .one, Matrix.permanent_one⟩ + +/-- **Multiplicative closure of permanent projections**: if `P` is a projection of the `m × m` +generic permanent and `Q` is a projection of the `k × k` generic permanent, then `P * Q` is a +projection of the `(m + k) × (m + k)` generic permanent. -/ +theorem IsProjection.permanent_mul {P Q : MvPolynomial σ K} {m k : ℕ} + (hP : IsProjection P (genericMatrix K m).permanent) + (hQ : IsProjection Q (genericMatrix K k).permanent) : + IsProjection (P * Q) (genericMatrix K (m + k)).permanent := by + obtain ⟨M₁, hM₁, rfl⟩ := isProjection_permanent_iff_exists_substMatrix.mp hP + obtain ⟨M₂, hM₂, rfl⟩ := isProjection_permanent_iff_exists_substMatrix.mp hQ + rw [← Matrix.permanent_fromBlocks_zero M₁ M₂] + exact (hM₁.fromBlocks .zero .zero hM₂).isProjection_permanent finSumFinEquiv.symm + +/-- **Monotonicity of permanent projections in the matrix dimension**: if `m ≤ k` and `P` is a +projection of `(genericMatrix K m).permanent`, then `P` is a projection of +`(genericMatrix K k).permanent`. -/ +theorem isProjection_permanent_mono {P : MvPolynomial σ K} {m k : ℕ} (hmk : m ≤ k) + (hP : IsProjection P (genericMatrix K m).permanent) : + IsProjection P (genericMatrix K k).permanent := by + have hmul := hP.permanent_mul (isProjection_permanent_one (K := K) (σ := σ) (k - m)) + rwa [mul_one, Nat.add_sub_of_le hmk] at hmul + +/-- A polynomial `P` has a *rooted permanent representation* of internal dimension `m` if it is +the permanent of a `(1 + m) × (1 + m)` specialization matrix `M` on `Unit ⊕ Fin m` whose internal +block `M.toBlocks₂₂` has permanent `1`. -/ +private def IsRootedPermProjection (m : ℕ) (P : MvPolynomial σ K) : Prop := + ∃ M : Matrix (Unit ⊕ Fin m) (Unit ⊕ Fin m) (MvPolynomial σ K), + IsSubstMatrix M ∧ M.toBlocks₂₂.permanent = 1 ∧ M.permanent = P + +namespace IsRootedPermProjection + +/-- A rooted permanent representation of internal dimension `m` gives a projection of the +`(m + 1) × (m + 1)` generic permanent. -/ +private theorem to_isProjection_permanent {m : ℕ} {P : MvPolynomial σ K} + (h : IsRootedPermProjection m P) : + IsProjection P (genericMatrix K (m + 1)).permanent := by + obtain ⟨M, hM, -, rfl⟩ := h + have e : Fin (m + 1) ≃ Unit ⊕ Fin m := + (finCongr (Nat.add_comm m 1)).trans + (finSumFinEquiv.symm.trans (Equiv.sumCongr finOneEquiv (Equiv.refl _))) + exact hM.isProjection_permanent e + +/-- Every single-entry substitution `P` (a variable or constant) has a rooted permanent +representation of internal dimension `0`. -/ +private theorem of_isSubstEntry {P : MvPolynomial σ K} (hP : IsSubstEntry P) : + IsRootedPermProjection 0 P := by + refine ⟨Matrix.fromBlocks (Matrix.of fun _ _ => P) 0 0 0, + IsSubstMatrix.fromBlocks (fun _ _ => hP) .zero .zero .zero, + Matrix.permanent_isEmpty, ?_⟩ + rw [Matrix.permanent_fromBlocks_zero, Matrix.permanent_unique, Matrix.permanent_isEmpty, mul_one] + rfl + +/-- Every constant `C c` has a rooted permanent representation of internal dimension `0`. -/ +private theorem C (c : K) : IsRootedPermProjection 0 (MvPolynomial.C c : MvPolynomial σ K) := + .of_isSubstEntry (.C c) + +/-- Every variable `X i` has a rooted permanent representation of internal dimension `0`. -/ +private theorem X (i : σ) : IsRootedPermProjection 0 (MvPolynomial.X i : MvPolynomial σ K) := + .of_isSubstEntry (.X i) + +/-- Equivalence `Fin (m₁ + 1 + m₂) ≃ Fin m₁ ⊕ (Unit ⊕ Fin m₂)` used to flatten internal blocks of +rooted permanent representations. -/ +private def innerEquiv (m₁ m₂ : ℕ) : Fin (m₁ + 1 + m₂) ≃ Fin m₁ ⊕ (Unit ⊕ Fin m₂) := + (finCongr (Nat.add_assoc m₁ 1 m₂)).trans + (finSumFinEquiv.symm.trans + (Equiv.sumCongr (Equiv.refl _) + (finSumFinEquiv.symm.trans (Equiv.sumCongr finOneEquiv (Equiv.refl _))))) + +/-- Equivalence `Unit ⊕ Fin (m₁ + 1 + m₂) ≃ Unit ⊕ (Fin m₁ ⊕ (Unit ⊕ Fin m₂))`. -/ +private def outerEquiv (m₁ m₂ : ℕ) : + Unit ⊕ Fin (m₁ + 1 + m₂) ≃ Unit ⊕ (Fin m₁ ⊕ (Unit ⊕ Fin m₂)) := + Equiv.sumCongr (Equiv.refl Unit) (innerEquiv m₁ m₂) + +/-- **Additive closure of rooted permanent representations**: if `P` and `Q` have rooted permanent +representations of internal dimensions `m₁` and `m₂`, then `P + Q` has one of internal dimension +`m₁ + 1 + m₂`. -/ +private theorem add {m₁ m₂ : ℕ} {P Q : MvPolynomial σ K} + (hP : IsRootedPermProjection m₁ P) (hQ : IsRootedPermProjection m₂ Q) : + IsRootedPermProjection (m₁ + 1 + m₂) (P + Q) := by + obtain ⟨M₁, hM₁, hU₁, rfl⟩ := hP + obtain ⟨M₂, hM₂, hU₂, rfl⟩ := hQ + refine ⟨(Matrix.rootedAdd M₁ M₂).submatrix (outerEquiv m₁ m₂) (outerEquiv m₁ m₂), + (hM₁.rootedAdd hM₂).submatrix _ _, ?_, ?_⟩ + · have hblk : ((Matrix.rootedAdd M₁ M₂).submatrix + (outerEquiv m₁ m₂) (outerEquiv m₁ m₂)).toBlocks₂₂ = + (Matrix.rootedAdd M₁ M₂).toBlocks₂₂.submatrix (innerEquiv m₁ m₂) (innerEquiv m₁ m₂) := rfl + rw [hblk, Matrix.permanent_submatrix_equiv, Matrix.permanent_toBlocks₂₂_rootedAdd M₁ M₂ hU₁ hU₂] + · rw [Matrix.permanent_submatrix_equiv, Matrix.permanent_rootedAdd M₁ M₂ hU₁ hU₂] + +/-- **Multiplicative closure of rooted permanent representations**: if `P` and `Q` have rooted +permanent representations of internal dimensions `m₁` and `m₂`, then `P * Q` has one of internal +dimension `m₁ + 1 + m₂`. -/ +private theorem mul {m₁ m₂ : ℕ} {P Q : MvPolynomial σ K} + (hP : IsRootedPermProjection m₁ P) (hQ : IsRootedPermProjection m₂ Q) : + IsRootedPermProjection (m₁ + 1 + m₂) (P * Q) := by + obtain ⟨M₁, hM₁, hU₁, rfl⟩ := hP + obtain ⟨M₂, hM₂, hU₂, rfl⟩ := hQ + refine ⟨(Matrix.rootedMul M₁ M₂).submatrix (outerEquiv m₁ m₂) (outerEquiv m₁ m₂), + (hM₁.rootedMul hM₂).submatrix _ _, ?_, ?_⟩ + · have hblk : ((Matrix.rootedMul M₁ M₂).submatrix + (outerEquiv m₁ m₂) (outerEquiv m₁ m₂)).toBlocks₂₂ = + (Matrix.rootedMul M₁ M₂).toBlocks₂₂.submatrix (innerEquiv m₁ m₂) (innerEquiv m₁ m₂) := rfl + rw [hblk, Matrix.permanent_submatrix_equiv, Matrix.permanent_toBlocks₂₂_rootedMul M₁ M₂ hU₁ hU₂] + · rw [Matrix.permanent_submatrix_equiv, Matrix.permanent_rootedMul M₁ M₂] + +end IsRootedPermProjection + +/-- Every arithmetic formula `F` computes a polynomial with a rooted permanent representation of +internal dimension at most `F.size`. -/ +private theorem _root_.Cslib.Circuits.Formula.exists_isRootedPermProjection + (F : Formula (arithSignature K) n) : + ∃ m ≤ F.size, IsRootedPermProjection m (F.eval (arithInterpretationWith K C) X) := by + induction F with + | input i => + exact ⟨0, le_rfl, .X i⟩ + | gate op args ih => + cases op with + | const c => + exact ⟨0, Nat.zero_le _, .C c⟩ + | add => + obtain ⟨m₀, hm₀, h₀⟩ := ih 0 + obtain ⟨m₁, hm₁, h₁⟩ := ih 1 + refine ⟨m₀ + 1 + m₁, ?_, h₀.add h₁⟩ + rw [Formula.size_gate] + change m₀ + 1 + m₁ ≤ (∑ j : Fin 2, (args j).size) + 1 + rw [Fin.sum_univ_two] + omega + | mul => + obtain ⟨m₀, hm₀, h₀⟩ := ih 0 + obtain ⟨m₁, hm₁, h₁⟩ := ih 1 + refine ⟨m₀ + 1 + m₁, ?_, h₀.mul h₁⟩ + rw [Formula.size_gate] + change m₀ + 1 + m₁ ≤ (∑ j : Fin 2, (args j).size) + 1 + rw [Fin.sum_univ_two] + omega + +/-- **Formula universality for the permanent**: the formal polynomial computed by an +arithmetic formula `F` is a projection of the `(F.size + 1) × (F.size + 1)` generic permanent. +This gives an explicit semiring version of the permanent part of +[Orzel et al., Lemma 4][OrzelSrinivasanTavenasYehudayoff2025]. `size` counts operation nodes, +including constants; the linear dimension bound is proved directly by the construction. -/ +theorem _root_.Cslib.Circuits.Formula.isProjection_permanent + (F : Formula (arithSignature K) n) : + IsProjection (F.eval (arithInterpretationWith K C) X) + (genericMatrix K (F.size + 1)).permanent := by + obtain ⟨m, hm, hroot⟩ := F.exists_isRootedPermProjection + exact isProjection_permanent_mono (Nat.add_le_add_right hm 1) hroot.to_isProjection_permanent + +/-- The formal polynomial `(F.toCircuit).polynomial 0` of any arithmetic formula `F` is a +projection of `(genericMatrix K (F.size + 1)).permanent`. -/ +theorem _root_.Cslib.Circuits.Formula.isProjection_permanent_toCircuit + (F : Formula (arithSignature K) n) : + IsProjection (F.toCircuit.polynomial 0) (genericMatrix K (F.size + 1)).permanent := by + simpa [Circuit.polynomial] using F.isProjection_permanent + +end Cslib.Circuits.Arithmetic diff --git a/Complexity/Foundations/Data/Matrix/Permanent/Blocks.lean b/Complexity/Foundations/Data/Matrix/Permanent/Blocks.lean new file mode 100644 index 0000000000..52bcd0a592 --- /dev/null +++ b/Complexity/Foundations/Data/Matrix/Permanent/Blocks.lean @@ -0,0 +1,176 @@ +/- +Copyright (c) 2026 Kenny Lau, Chris Hughes, Anne Baanen, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kenny Lau, Chris Hughes, Anne Baanen, Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, next to `LinearAlgebra/Matrix/Permanent`) + +public import Complexity.Init +public import Mathlib.Data.Matrix.Block +public import Mathlib.LinearAlgebra.Matrix.Permanent +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Data.Fintype.BigOperators +import Mathlib.GroupTheory.Perm.Finite + +/-! +# Reindexing, multilinearity and block identities for the permanent + +The permanent is unchanged by independent row and column reindexing, commutes with ring and +algebra homomorphisms, and is additive in each row and column. On a block triangular matrix +with square diagonal blocks, it is the product of their permanents. These identities work over +every commutative semiring, including empty index types. + +## Main results + +* `Matrix.permanent_submatrix_equiv_equiv`: independent row and column reindexing. +* `Matrix.permanent_updateRow_add`, `Matrix.permanent_updateCol_add`: multilinearity. +* `RingHom.map_permanent`, `AlgHom.map_permanent`: compatibility with homomorphisms. +* `Matrix.permanent_fromBlocks_zero₂₁`, `Matrix.permanent_fromBlocks_zero₁₂`: triangular blocks. + +## References + +The block proof adapts Mathlib's `Matrix.det_fromBlocks_zero₂₁` in +`Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean`, retaining its authors' credit. Other proof +material is adapted from the saved Complexitylib development at revision `5b8acca7`. +-/ + +@[expose] public section + +namespace Matrix + +open Equiv Equiv.Perm Finset Fintype + +variable {m n : Type*} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] +variable {R : Type*} [CommSemiring R] + +/-- Reindexing both rows and columns of a square matrix by the same equivalence preserves its +permanent. -/ +@[simp] theorem permanent_submatrix_equiv {m' : Type*} [Fintype m'] [DecidableEq m'] (e : m' ≃ m) + (A : Matrix m m R) : (A.submatrix e e).permanent = A.permanent := by + rw [permanent, permanent, ← (Equiv.permCongr e).sum_comp] + refine Finset.sum_congr rfl fun σ _ => ?_ + rw [← e.prod_comp] + exact Finset.prod_congr rfl fun i _ => by simp [submatrix_apply, Equiv.permCongr_apply] + +/-- Reindexing the rows and columns of a square matrix by any two equivalences preserves its +permanent. -/ +theorem permanent_submatrix_equiv_equiv {m' : Type*} [Fintype m'] [DecidableEq m'] + (e₁ e₂ : m' ≃ m) (A : Matrix m m R) : (A.submatrix e₁ e₂).permanent = A.permanent := by + have h : A.submatrix e₁ e₂ = (A.submatrix e₂ e₂).submatrix (e₁.trans e₂.symm) id := by + ext i j + simp [submatrix_apply] + rw [h, permanent_permute_cols, permanent_submatrix_equiv] + +/-- Multilinearity of the permanent in a column. -/ +@[simp] theorem permanent_updateCol_add (M : Matrix m m R) (j : m) (u v : m → R) : + (M.updateCol j (u + v)).permanent = + (M.updateCol j u).permanent + (M.updateCol j v).permanent := by + simp only [permanent, ← Finset.mul_prod_erase _ _ (Finset.mem_univ j), updateCol_self, + Pi.add_apply, add_mul, Finset.sum_add_distrib] + congr 1 <;> + refine Finset.sum_congr rfl fun p _ => + congrArg (_ * ·) (Finset.prod_congr rfl fun i hi => ?_) <;> + simp only [ne_eq, Finset.ne_of_mem_erase hi, not_false_eq_true, updateCol_ne] + +/-- Multilinearity of the permanent in a row. -/ +@[simp] theorem permanent_updateRow_add (M : Matrix m m R) (i : m) (u v : m → R) : + (M.updateRow i (u + v)).permanent = + (M.updateRow i u).permanent + (M.updateRow i v).permanent := by + rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_add, + updateCol_transpose, updateCol_transpose, permanent_transpose, permanent_transpose] + +/-- If two matrices `M₁, M₂` agree with `M` outside row `r` and their `r`-th rows sum to row `r` +of `M`, then `M.permanent = M₁.permanent + M₂.permanent`. -/ +theorem permanent_add_of_row_eq (M M₁ M₂ : Matrix m m R) (r : m) + (hr : ∀ j, M r j = M₁ r j + M₂ r j) + (h₁ : ∀ i ≠ r, ∀ j, M₁ i j = M i j) + (h₂ : ∀ i ≠ r, ∀ j, M₂ i j = M i j) : + M.permanent = M₁.permanent + M₂.permanent := by + have hM : M = M.updateRow r (M₁ r + M₂ r) := by + ext i j + by_cases hir : i = r + · subst hir; simp [hr j] + · simp [hir] + have hM₁ : M₁ = M.updateRow r (M₁ r) := by + ext i j + by_cases hir : i = r + · subst hir; simp + · simp [hir, h₁ i hir j] + have hM₂ : M₂ = M.updateRow r (M₂ r) := by + ext i j + by_cases hir : i = r + · subst hir; simp + · simp [hir, h₂ i hir j] + conv_lhs => rw [hM] + rw [permanent_updateRow_add, ← hM₁, ← hM₂] + +/-- Applying a ring homomorphism to the permanent of a matrix is the permanent of the mapped +matrix. -/ +theorem _root_.RingHom.map_permanent {S : Type*} [CommSemiring S] (f : R →+* S) + (M : Matrix m m R) : f M.permanent = (M.map f).permanent := by + simp [permanent, map_sum, map_prod] + +/-- Applying an algebra homomorphism to the permanent of a matrix is the permanent of the mapped +matrix. -/ +theorem _root_.AlgHom.map_permanent {R₀ A B : Type*} [CommSemiring R₀] [CommSemiring A] + [CommSemiring B] [Algebra R₀ A] [Algebra R₀ B] (f : A →ₐ[R₀] B) (M : Matrix m m A) : + f M.permanent = (M.map f).permanent := + f.toRingHom.map_permanent M + +/-- The permanent of a `2 × 2` block matrix with the lower-left block equal to zero is the product +of the permanents of the diagonal blocks. -/ +@[simp] theorem permanent_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) + (D : Matrix n n R) : (fromBlocks A B 0 D).permanent = A.permanent * D.permanent := by + classical + simp_rw [permanent] + convert + Eq.symm <| + sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_ + · simp_rw [Finset.sum_mul_sum, ← sum_product', univ_product_univ] + refine sum_nbij (fun σ => σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_ + · intro σ₁₂ _ + exact Set.mem_toFinset.mpr ⟨σ₁₂, rfl⟩ + · intro σ₁ _ σ₂ _ h + have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x := + DFunLike.congr_fun h + simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq, + Sum.inr.injEq] at h2 + ext x + · exact h2.left x + · exact h2.right x + · intro σ hσ + rw [mem_coe, Set.mem_toFinset] at hσ + obtain ⟨σ₁₂, hσ₁₂⟩ := hσ + exact ⟨σ₁₂, mem_univ _, by simpa using hσ₁₂⟩ + · simp only [forall_prop_of_true, Prod.forall, mem_univ] + intro σ₁ σ₂ + rw [Fintype.prod_sum_type] + simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁, + fromBlocks_apply₂₂] + · rintro σ - hσn + have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by + rw [Set.mem_toFinset] at hσn + simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using + mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn + obtain ⟨a, ha⟩ := not_forall.mp h1 + rcases hx : σ (Sum.inl a) with a2 | b + · exact absurd hx.symm ((not_exists.mp ha) a2) + · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a))] + rw [hx, fromBlocks_apply₂₁, Matrix.zero_apply] + +/-- The permanent of a `2 × 2` block matrix with the upper-right block equal to zero is the product +of the permanents of the diagonal blocks. -/ +@[simp] theorem permanent_fromBlocks_zero₁₂ (A : Matrix m m R) (C : Matrix n m R) + (D : Matrix n n R) : (fromBlocks A 0 C D).permanent = A.permanent * D.permanent := by + rw [← permanent_transpose, fromBlocks_transpose, transpose_zero, permanent_fromBlocks_zero₂₁, + permanent_transpose, permanent_transpose] + +/-- The permanent of a block-diagonal `2 × 2` matrix is the product of the permanents of its +diagonal blocks. -/ +theorem permanent_fromBlocks_zero (A : Matrix m m R) (D : Matrix n n R) : + (fromBlocks A (0 : Matrix m n R) 0 D).permanent = A.permanent * D.permanent := + permanent_fromBlocks_zero₂₁ A 0 D + +end Matrix diff --git a/ComplexityTests/PermanentFormulas.lean b/ComplexityTests/PermanentFormulas.lean new file mode 100644 index 0000000000..f4c99b427f --- /dev/null +++ b/ComplexityTests/PermanentFormulas.lean @@ -0,0 +1,88 @@ +/- +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.Formula +import Complexity.Foundations.Data.Matrix.Permanent +import Mathlib.Algebra.Field.ZMod + +/-! +# Permanent projections of concrete arithmetic formulas + +The mixed formula `(X₀ + 2) * (X₀ + X₁)` uses addition, multiplication, a repeated input and a +constant, and evaluates to `50` on `(3, 7)`. Its four operation nodes give a permanent projection +of dimension five over `ℕ`. Squaring in characteristic two remains the formal polynomial +`X₀²`. Empty blocks and constant-only formulas check the zero-dimensional boundary cases. +-/ + +namespace ComplexityTests.PermanentFormulas + +open Cslib Cslib.Circuits Cslib.Circuits.Arithmetic MvPolynomial + +private def mixed : Formula (arithSignature ℕ) 2 := + .gate₂ .mul rfl + (.gate₂ .add rfl (.input 0) (.gate (.const 2) Fin.elim0)) + (.gate₂ .add rfl (.input 0) (.input 1)) + +private theorem mixed_size : mixed.size = 4 := by + simp [mixed] + +example : mixed.eval (arithInterpretation ℕ) ![3, 7] = 50 := by + norm_num [mixed, Formula.eval, Formula.gate₂, arithInterpretation, arithInterpretationWith] + +private theorem mixed_projection : IsProjection + ((X 0 + 2) * (X 0 + X 1) : MvPolynomial (Fin 2) ℕ) + (genericMatrix ℕ 5).permanent := by + have h := mixed.isProjection_permanent + rw [mixed_size] at h + simpa [mixed, Formula.eval, Formula.gate₂, arithInterpretationWith] using h + +-- Multiplicative closure and padding use the same existing projection API. +example : IsProjection + (((X 0 + 2) * (X 0 + X 1)) * X 0 : MvPolynomial (Fin 2) ℕ) + (genericMatrix ℕ 8).permanent := by + have hx : IsProjection (X (0 : Fin 2) : MvPolynomial (Fin 2) ℕ) + (genericMatrix ℕ 1).permanent := + (Formula.input (σ := arithSignature ℕ) (n := 2) 0).isProjection_permanent + exact isProjection_permanent_mono (by decide : 5 + 1 ≤ 8) (mixed_projection.permanent_mul hx) + +example : IsProjection (mixed.toCircuit.polynomial 0) (genericMatrix ℕ 5).permanent := by + have h := mixed.isProjection_permanent_toCircuit + rw [mixed_size] at h + exact h + +private def square : Formula (arithSignature (ZMod 2)) 1 := + .gate₂ .mul rfl (.input 0) (.input 0) + +example : IsProjection (X 0 ^ 2 : MvPolynomial (Fin 1) (ZMod 2)) + (genericMatrix (ZMod 2) 2).permanent := by + have h := square.isProjection_permanent + rw [show square.size = 1 by decide] at h + simpa [square, Formula.eval, Formula.gate₂, arithInterpretationWith, sq] using h + +private def constantOnly : Formula (arithSignature ℕ) 0 := .gate (.const 7) Fin.elim0 + +example : IsProjection (C 7 : MvPolynomial (Fin 0) ℕ) (genericMatrix ℕ 2).permanent := by + have h := constantOnly.isProjection_permanent + rw [show constantOnly.size = 1 by decide] at h + simpa [constantOnly, Formula.eval, arithInterpretationWith] using h + +-- The upper-right block can be nonzero: square diagonal blocks still factor. +example : (Matrix.fromBlocks (!![2] : Matrix (Fin 1) (Fin 1) ℕ) + (!![3, 11] : Matrix (Fin 1) (Fin 2) ℕ) 0 !![2, 3; 5, 7]).permanent = 58 := by + rw [Matrix.permanent_fromBlocks_zero₂₁, Matrix.permanent_unique, + Matrix.permanent_succ_row_zero, Fin.sum_univ_two] + decide + +example (A : Matrix (Fin 2) (Fin 2) ℕ) : + (Matrix.fromBlocks A (0 : Matrix (Fin 2) (Fin 0) ℕ) 0 1).permanent = A.permanent := by + rw [Matrix.permanent_fromBlocks_zero, Matrix.permanent_one, mul_one] + +example : ((!![2, 3; 5, 7] : Matrix (Fin 2) (Fin 2) ℕ).submatrix + (Equiv.swap 0 1) (Equiv.refl _)).permanent = 29 := by + rw [Matrix.permanent_submatrix_equiv_equiv, Matrix.permanent_succ_row_zero, Fin.sum_univ_two] + decide + +end ComplexityTests.PermanentFormulas From de5703cd3c6a768ed5a4947ef0df4bd520ef8bae Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:53:50 -0400 Subject: [PATCH 2/2] doc(arithmetic): record permanent formula simulation and its scope --- ROADMAP.md | 5 ++++- references.bib | 12 ++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index fe1c32dcd3..ff0965e84e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -805,7 +805,10 @@ and credited. These remain coverage targets but are deferred from the active queue; their issues were closed as not planned, not as proved. -- The full VNP-completeness reduction for the permanent ([#321]). +- The full VNP-completeness reduction for the permanent ([#321]). Arithmetic formulas now + project to the permanent with dimension `Formula.size + 1` over every commutative semiring; + the conversion from VP witnesses to formulas and elimination of Boolean sums needed for + VNP-hardness remain open. - General auxiliary-input zero knowledge ([#324]); see the GMW theorem above. - Williams's square-root-space simulation ([#361]) and implicit Tree Evaluation ([#367]), now the frontier track [#888]. diff --git a/references.bib b/references.bib index 6012526f44..d12bd7db1f 100644 --- a/references.bib +++ b/references.bib @@ -3527,6 +3527,18 @@ @article{Ore1933 doi = {10.1090/S0002-9947-1933-1501703-0} } +@inproceedings{OrzelSrinivasanTavenasYehudayoff2025, + author = {Orzel, Ian and Srinivasan, Srikanth and Tavenas, S{\'e}bastien and Yehudayoff, Amir}, + title = {The Algebraic Cost of a Boolean Sum}, + booktitle = {45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, + series = {LIPIcs}, + volume = {360}, + pages = {47:1--47:13}, + year = {2025}, + doi = {10.4230/LIPIcs.FSTTCS.2025.47}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.47} +} + @article{Oum2005, author = {Oum, Sang-il}, title = {Rank-width and Vertex-minors},