Documentation

Complexity.Computability.Circuit.Arithmetic.Determinant

The determinant is in VP #

The generic matrix genericMatrix K n is the n × n matrix whose entries are the n * n variables, in row-major order, and the determinant family detFamily K consists of its determinants. Over every commutative ring K the determinant family is in VP K [Val79a]: exists_circuit_det gives, for every n, an arithmetic circuit with at most 3 * n ^ 4 + 4 gates computing the generic determinant as a formal polynomial.

The circuit runs Bird's division-free algorithm [Bir11], whose correctness is Mathlib's BirdDet development; Cslib.Circuits.Rational.DeterminantAlgorithm executes the same algorithm on integer matrices. Bird's algorithm, like Berkowitz's [Ber84], uses only additions, multiplications and integer constants, so no field or characteristic hypothesis is needed. It runs n - 1 stages. Each stage multiplies the previous matrix, with its diagonal replaced by negated suffix sums and its lower triangle cleared, by the input matrix; each of its n ^ 2 entries costs at most 3 * n + 3 gates. Common subexpressions are not shared across entries, which a sharper count would exploit. Only the gate count is certified; the circuits are 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.

Main definitions #

Main results #

References #

Bird's algorithm over a commutative ring #

source
theorem Cslib.Circuits.Arithmetic.det_eq_birdDetSpec {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) :
A.det = BirdDet.Spec.birdDet A

Bird's algorithm in matrix form computes the determinant over every commutative ring [Bir11]. The shared bridge restates Mathlib's private matrix-specification theorem.

The generic matrix and the determinant family #

source
noncomputable def Cslib.Circuits.Arithmetic.genericMatrix (K : Type u) [CommSemiring K] (n : ℕ) :
Matrix (Fin n) (Fin n) (MvPolynomial (Fin (n * n)) K)

The generic n × n matrix over K: entry (i, j) is the variable n * i + j of MvPolynomial (Fin (n * n)) K.

Instances For
    source
    noncomputable def Cslib.Circuits.Arithmetic.detFamily (K : Type u) [CommRing K] :
    PolynomialFamily K

    The determinant family over K: its n-th member is the determinant of the generic n × n matrix, a polynomial in n * n variables.

    Instances For
      source
      theorem Cslib.Circuits.Arithmetic.totalDegree_det_genericMatrix_le {K : Type u} [CommRing K] (n : ℕ) :
      (genericMatrix K n).det.totalDegree ≤ n

      The generic determinant has total degree at most n.

      The permanent family #

      source
      noncomputable def Cslib.Circuits.Arithmetic.permFamily (K : Type u) [CommSemiring K] :
      PolynomialFamily K

      The permanent family over K: its n-th member is the permanent of the generic n × n matrix, a polynomial in n * n variables.

      Instances For
        source
        theorem Cslib.Circuits.Arithmetic.totalDegree_permanent_genericMatrix_le {K : Type u} [CommRing K] (n : ℕ) :
        (genericMatrix K n).permanent.totalDegree ≤ n

        The generic permanent has total degree at most n.

        source
        theorem Cslib.Circuits.Arithmetic.isPFamily_permFamily {K : Type u} [CommRing K] :
        (permFamily K).IsPFamily

        The permanent family over K is a p-family (vars n = n ^ 2 and totalDegree ≤ n).

        Bird's algorithm as an arithmetic circuit #

        source
        theorem Cslib.Circuits.Arithmetic.exists_circuit_det {K : Type u} [CommRing K] (n : ℕ) :
        ∃ (c : Circuit (arithSignature K) (n * n) 1), c.polynomial 0 = (genericMatrix K n).det ∧ c.size ≤ 3 * n ^ 4 + 4

        The determinant has small circuits [Bir11]: the generic n × n determinant is computed by an arithmetic circuit with at most 3 * n ^ 4 + 4 gates, over every commutative ring K.

        source
        theorem Cslib.Circuits.Arithmetic.exists_circuit_det_eval {K : Type u} [CommRing K] (n : ℕ) :
        ∃ (c : Circuit (arithSignature K) (n * n) 1), c.size ≤ 3 * n ^ 4 + 4 ∧ ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Algebra K R] (A : Matrix (Fin n) (Fin n) R), c.eval (arithInterpretationWith K ⇑(algebraMap K R)) (fun (k : Fin (n * n)) => A (finProdFinEquiv.symm k).1 (finProdFinEquiv.symm k).2) 0 = A.det

        The circuits of exists_circuit_det are universal: the same circuit evaluates the determinant of every n × n matrix over every commutative K-algebra, its entries supplied in row-major order.

        source
        theorem Cslib.Circuits.Arithmetic.detFamily_mem_VP {K : Type u} [CommRing K] :
        detFamily K ∈ VP K

        The determinant is in VP [Val79a]: over every commutative ring, the family of generic determinants has n * n variables, degree at most n and arithmetic circuits with at most 3 * n ^ 4 + 4 gates.