Monotone circuits for Boolean matrix product

The Boolean product of an I × K matrix x and a K × J matrix y has entries z i j = ⋁ k, x i k ∧ y k j. Every circuit over the binary AND/OR basis (AndOr.signature, which has neither negations nor constants) computing it has at least I * J * K AND gates (Pratt 1975; Paterson 1975; Mehlhorn--Galil 1976; see Wegener, The Complexity of Boolean Functions, Theorem 6.8.1). AND gates are counted by AndOr.andCost, which charges one per AND gate and nothing per OR gate; every gate of the program is counted, used or not. The schoolbook circuit attains the bound.

Main results

• mul_mul_le_andCost: the bound for any injective placement of the entries of x and y among the circuit inputs and any placement of the outputs.
• cube_le_andCost: for two n × n matrices in a fixed row-major layout, at least n ^ 3 AND gates.

The proof is in Complexitylib.Algebraic.LowerBound.Monotone.MatrixProduct.Internal.

theorem Algebraic.Monotone.MatrixProduct.mul_mul_le_andCost {N M I J K : ℕ} (x : Fin I → Fin K → Fin N) (y : Fin K → Fin J → Fin N) (distinct : Function.Injective (Sum.elim (Function.uncurry x) (Function.uncurry y))) (z : Fin I → Fin J → Fin M) (circuit : Circuit AndOr.signature N M) (computes : ∀ (a : Fin N → Bool) (i : Fin I) (j : Fin J), circuit.eval AndOr.boolInterpretation a (z i j) = decide (∃ (k : Fin K), a (x i k) = true ∧ a (y k j) = true)) : I * J * K ≤ circuit.cost AndOr.andCost

Monotone Boolean matrix product. Place entry (i, k) of an I × K matrix at input x i k and entry (k, j) of a K × J matrix at input y k j, all at distinct inputs. An AND/OR circuit whose output z i j computes ⋁ k, x i k ∧ y k j for every i and j has at least I * J * K AND gates.

def Algebraic.Monotone.MatrixProduct.leftEntry (n : ℕ) (i k : Fin n) : Fin (n * n + n * n)

The input carrying entry (i, k) of the left n × n matrix: the first n * n inputs, in row-major order.

Equations

• Algebraic.Monotone.MatrixProduct.leftEntry n i k = Fin.castAdd (n * n) (finProdFinEquiv (i, k))

def Algebraic.Monotone.MatrixProduct.rightEntry (n : ℕ) (k j : Fin n) : Fin (n * n + n * n)

The input carrying entry (k, j) of the right n × n matrix: the last n * n inputs, in row-major order.

Equations

• Algebraic.Monotone.MatrixProduct.rightEntry n k j = Fin.natAdd (n * n) (finProdFinEquiv (k, j))

def Algebraic.Monotone.MatrixProduct.productEntry (n : ℕ) (i j : Fin n) : Fin (n * n)

The output carrying entry (i, j) of the product, in row-major order.

Equations

• Algebraic.Monotone.MatrixProduct.productEntry n i j = finProdFinEquiv (i, j)

theorem Algebraic.Monotone.MatrixProduct.entry_injective (n : ℕ) : Function.Injective (Sum.elim (Function.uncurry (leftEntry n)) (Function.uncurry (rightEntry n)))

The row-major layout puts the entries of both matrices at distinct inputs.

theorem Algebraic.Monotone.MatrixProduct.cube_le_andCost (n : ℕ) (circuit : Circuit AndOr.signature (n * n + n * n) (n * n)) (computes : ∀ (a : Fin (n * n + n * n) → Bool) (i j : Fin n), circuit.eval AndOr.boolInterpretation a (productEntry n i j) = decide (∃ (k : Fin n), a (leftEntry n i k) = true ∧ a (rightEntry n k j) = true)) : n ^ 3 ≤ circuit.cost AndOr.andCost

Monotone Boolean matrix product, square case. An AND/OR circuit computing the Boolean product of two n × n matrices has at least n ^ 3 AND gates.