The size bounds for matrix multiplication

• The finite bound (sq_sub_le_of_charges). Suppose every split has total charge at most three times its crossing signals plus 3 L. Along the ranking of MultiOutput.exists_rank, the threshold prefix of Tripartite.exists_threshold ends at a terminal and satisfies 3 n² ≤ 2 (R_I + R_J + R_K) + 3 (Tripartite.three_mul_sq_le_two_mul_charge), so it is crossed by at least (n² - 2 L - 1)/2 signals. It is charged to the component holding all terminals (mem_component_of_trace), which has 2 n² inputs and at most s gates. With a totally regular matrix L = 0 (half_sq_le_of_totallyRegular); over every finite field L = 4 n (sq_sub_le); for polynomial gates over any field K, evaluating over K(t) with the generic Hankel matrix gives L = 0 (half_sq_le_of_formallyComputes).
• The asymptotic bound (eventually_lt_size_of_orderingBound_matMul, eventually_lt_size_of_orderingBound_matMul_polynomial). Assume at most (2 + 1/(2A) - ε) n² gates and choose η = A² ε; the cycle term is then at most (1/2 - A ε/2) n², while the loss 4 n and the logarithmic term are o(n²).

The finite bound

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sq_sub_le_of_charges {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) (p : Program σ (n * n + n * n) s) (hp : p.FanInAtMost 2) (I : Interpretation σ F) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) (L : ℕ) (hcharge : ∀ (S : Finset (Wire (n * n + n * n) s)), Tripartite.chargeI (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermC out) S) + Tripartite.chargeJ (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) + Tripartite.chargeK (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ 3 * ((SingleCut.forward p S).card + (SingleCut.backward p S).card) + 3 * L) : (↑n ^ 2 - 2 * ↑L - 1) / 2 ≤ (A + η) * max (↑s - 2 * ↑n ^ 2) 0 + 3 * Real.logb 2 (2 * ↑n ^ 2 + 3 * ↑s) + C

The finite bound from the charges. If every split of a fan-in-two program whose wires out carry matMul n has total charge at most three times its crossing signals plus 3 L, then (n² - 2 L - 1)/2 ≤ (A + η) (s - 2 n²)⁺ + 3 log₂ (2 n² + 3 s) + C.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.half_sq_le_of_totallyRegular {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {M : Matrix (Fin n) (Fin n) F} (hM : TotallyRegular M) (p : Program σ (n * n + n * n) s) (hp : p.FanInAtMost 2) (I : Interpretation σ F) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) : (↑n ^ 2 - 1) / 2 ≤ (A + η) * max (↑s - 2 * ↑n ^ 2) 0 + 3 * Real.logb 2 (2 * ↑n ^ 2 + 3 * ↑s) + C

The finite bound with a totally regular matrix. A fan-in-two program over a finite field with a totally regular n × n matrix, whose wires out carry matMul n, has (n² - 1)/2 ≤ (A + η) (s - 2 n²)⁺ + 3 log₂ (2 n² + 3 s) + C.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sq_sub_le {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) (p : Program σ (n * n + n * n) s) (hp : p.FanInAtMost 2) (I : Interpretation σ F) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) : (↑n ^ 2 - 8 * ↑n - 1) / 2 ≤ (A + η) * max (↑s - 2 * ↑n ^ 2) 0 + 3 * Real.logb 2 (2 * ↑n ^ 2 + 3 * ↑s) + C

The finite bound over every finite field. A fan-in-two program over any finite field whose wires out carry matMul n has (n² - 8 n - 1)/2 ≤ (A + η) (s - 2 n²)⁺ + 3 log₂ (2 n² + 3 s) + C.

Polynomial gates over arbitrary fields

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.aeval_matMul_X {n : ℕ} {K : Type u_1} {R : Type u_2} [CommSemiring K] [CommSemiring R] [Algebra K R] (z : Fin (n * n + n * n) → R) (o : Fin (n * n)) : (MvPolynomial.aeval z) (matMul n MvPolynomial.X o) = matMul n z o

Evaluating the formal matrix product at a point of an algebra gives the matrix product.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.eval_matMul_X {n : ℕ} {K : Type u_1} [CommSemiring K] (z : Fin (n * n + n * n) → K) (o : Fin (n * n)) : (MvPolynomial.eval z) (matMul n MvPolynomial.X o) = matMul n z o

Evaluating the formal matrix product at a point gives the matrix product.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMul_nonconstant {n : ℕ} {K : Type u_1} [Field K] (o : Fin (n * n)) : ∃ (x : Fin (n * n + n * n) → K) (y : Fin (n * n + n * n) → K), matMul n x o ≠ matMul n y o

Every output entry of matrix multiplication is a nonconstant function.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.finrank_add_sum_min_le {n : ℕ} {L : Type u_1} [Field L] {ι : Type u_2} [Fintype ι] {N : ℕ} (U : Submodule L (Fin N → L)) (coord : ι → Fin n → Fin N) (hinj : ∀ u ∈ U, (∀ (t : ι) (j : Fin n), u (coord t j) = 0) → u = 0) (M : ι → Matrix (Fin n) (Fin n) L) (hM : ∀ (t : ι), TotallyRegular (M t)) (P Q : ι → Finset (Fin n)) (hsupp : ∀ u ∈ U, ∀ (t : ι), ∀ j ∉ P t, u (coord t j) = 0) (hker : ∀ u ∈ U, ∀ (t : ι), ∀ k ∈ Q t, (M t).mulVec (fun (j : Fin n) => u (coord t j)) k = 0) : Module.finrank L ↥U + ∑ t : ι, min (P t).card (Q t).card ≤ ∑ t : ι, (P t).card

Subspace decomposition across totally regular blocks.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.jacobian_matMulInput_zero_right {σ : Signature} {n s : ℕ} {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) (M : Matrix (Fin n) (Fin n) L) {v : Fin (n * n + n * n) → L} (hv : ∀ x ∉ leftCoords n, v x = 0) (i k : Fin n) : (Taylor.jacobian (Taylor.wirePolynomial P p) (matMulInput 0 M)).mulVec v (out (matMulOutput n i k)) = M.transpose.mulVec (fun (j : Fin n) => v (matMulLeft n i j)) k

At A = 0, B = M, the Jacobian of formal matrix multiplication sends a direction v supported on A to C i k = ∑ j, v (A i j) M j k.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.jacobian_matMulInput_zero_left {σ : Signature} {n s : ℕ} {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) (M : Matrix (Fin n) (Fin n) L) {v : Fin (n * n + n * n) → L} (hv : ∀ x ∉ rightCoords n, v x = 0) (i k : Fin n) : (Taylor.jacobian (Taylor.wirePolynomial P p) (matMulInput M 0)).mulVec v (out (matMulOutput n i k)) = M.mulVec (fun (j : Fin n) => v (matMulRight n j k)) i

At A = M, B = 0, the Jacobian of formal matrix multiplication sends a direction v supported on B to C i k = ∑ j, M i j v (B j k).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.dotProduct_hessian_matMulOutput {σ : Signature} {n s : ℕ} {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) (v u : Fin (n * n + n * n) → L) (i k : Fin n) : v ⬝ᵥ (Taylor.hessian (Taylor.wirePolynomial P p (out (matMulOutput n i k))) 0).mulVec u = ∑ j : Fin n, (v (matMulLeft n i j) * u (matMulRight n j k) + u (matMulLeft n i j) * v (matMulRight n j k))

The Hessian of the output C i k of formal matrix multiplication, as a bilinear form.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.dotProduct_bilinForm_add_transpose {n : ℕ} {L : Type u_2} [Field L] (M : Matrix (Fin n) (Fin n) L) (v u : Fin (n * n + n * n) → L) : v ⬝ᵥ (bilinForm M + (bilinForm M).transpose).mulVec u = ∑ i : Fin n, ∑ k : Fin n, M i k * ∑ j : Fin n, (v (matMulLeft n i j) * u (matMulRight n j k) + u (matMulLeft n i j) * v (matMulRight n j k))

The symmetrized bilinear form of M is the M-weighted sum of the output Hessian forms.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.chargeI_le_of_formallyComputes_of_totallyRegular {σ : Signature} {n s : ℕ} {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) {M : Matrix (Fin n) (Fin n) L} (hM : TotallyRegular M) (S : Finset (Wire (n * n + n * n) s)) : Tripartite.chargeI (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermC out) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card

The charge R_I for polynomial gates. With a totally regular matrix M over an extension field, R_I is at most the number of forward and backward signals.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.chargeK_le_of_formallyComputes_of_totallyRegular {σ : Signature} {n s : ℕ} {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) {M : Matrix (Fin n) (Fin n) L} (hM : TotallyRegular M) (S : Finset (Wire (n * n + n * n) s)) : Tripartite.chargeK (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card

The charge R_K for polynomial gates. With a totally regular matrix M over an extension field, R_K is at most the number of forward and backward signals.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.chargeJ_le_of_formallyComputes_of_totallyRegular {σ : Signature} {n s : ℕ} {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) {M : Matrix (Fin n) (Fin n) L} (hM : TotallyRegular M) (S : Finset (Wire (n * n + n * n) s)) : Tripartite.chargeJ (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card

The charge R_J for polynomial gates. With a totally regular matrix M over an extension field, R_J is at most the number of forward and backward signals, by the Hessian cut bound.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.charges_le_of_formallyComputes {σ : Signature} {n s : ℕ} {K : Type u_1} [Field K] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) (S : Finset (Wire (n * n + n * n) s)) : Tripartite.chargeI (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermC out) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card ∧ Tripartite.chargeJ (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card ∧ Tripartite.chargeK (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card

The three charges for polynomial gates over any field.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.half_sq_le_of_formallyComputes {σ : Signature} {n s : ℕ} {K : Type u_1} [Field K] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ (n * n + n * n) s) (out : Fin (n * n) → Wire (n * n + n * n) s) {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) (hp : p.FanInAtMost 2) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMul n MvPolynomial.X o) : (↑n ^ 2 - 1) / 2 ≤ (A + η) * max (↑s - 2 * ↑n ^ 2) 0 + 3 * Real.logb 2 (2 * ↑n ^ 2 + 3 * ↑s) + C

The finite bound for polynomial gates over any field.

Asymptotics

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.eventually_lt_of_sq_sub_le {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : ℕ), (∀ (η C : ℝ), 0 ≤ A + η → Multigraph.OrderingBound A η C → (↑n ^ 2 - 8 * ↑n - 1) / 2 ≤ (A + η) * max (↑s - 2 * ↑n ^ 2) 0 + 3 * Real.logb 2 (2 * ↑n ^ 2 + 3 * ↑s) + C) → (2 + 1 / (2 * A) - ε) * ↑n ^ 2 < ↑s

The asymptotic bound from the finite inequality.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.eventually_lt_size_of_orderingBound_matMul {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Fintype F] (σ : Signature) (I : Interpretation σ F) (c : Circuit σ (n * n + n * n) (n * n)), c.FanInAtMost 2 → c.Computes I (matMul n) → (2 + 1 / (2 * A) - ε) * ↑n ^ 2 < ↑c.size

The asymptotic bound for matrix multiplication with a general ordering coefficient.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.eventually_lt_size_of_orderingBound_matMul_polynomial {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (K : Type u) [inst : Field K] (σ : Signature) (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (c : Circuit σ (n * n + n * n) (n * n)), c.FanInAtMost 2 → Taylor.FormallyComputes P c (matMul n MvPolynomial.X) → (2 + 1 / (2 * A) - ε) * ↑n ^ 2 < ↑c.size

The asymptotic bound for polynomial gates over any field with a general ordering coefficient.