Proofs for arithmetic matrix multiplication

Let a program with polynomial gates over a field K carry the polynomials matMulPolynomial K n on its output wires out.

• The cut bounds (chargeJ_le_of_formal, jacobianChargeI_le_of_formal, jacobianChargeK_le_of_formal). Every split S, crossed by w signals, has R_J, L_I, L_K ≤ w. Over K(t) the Hankel matrix M = (t ^ ((i + j)²)) is totally regular (totallyRegular_genericHankel). The Hessian consequence of the Taylor cut lemma, for the combination ∑ M i k C i k, bounds R_J (chargeJ_le_blockRank_hessian); its Jacobian consequence at the point A = B = M bounds the forward and the backward block together, so L_I and L_K (jacobianRows_le_blockRank, jacobianCols_le_blockRank).
• One component (mem_component_of_formal). The component of the output C 0 0 is crossed by no signal, so both Jacobian blocks vanish at the point A = B = 1 (all ones), where the output C i k has derivative one in every A i j and every B j k. So C i k, A i j and B j k lie together in or out of the component, which spreads to every terminal.
• The finite bound (fifteen_mul_sq_sub_le). At the threshold prefix of Tripartite.exists_threshold, 15 n² ≤ 8 (R_J + L_I + L_K) + 6 n + 9 ≤ 24 w + 6 n + 9 (fifteen_mul_sq_le), and the prefix is charged to the component of all 2 n² inputs.
• The asymptotic bound (eventually_lt_of_le). Assume at most (2 + 5/(8 A) - ε) n² gates and choose η = A² ε/2; the cycle term is then at most (5/8 - A ε/2) n², while the linear loss and the logarithmic term are o(n²).

Evaluating the polynomials

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.aeval_matMulPolynomial {n : ℕ} {K : Type u_1} {A : Type u_2} [CommSemiring K] [CommSemiring A] [Algebra K A] (z : Fin (n * n + n * n) → A) (o : Fin (n * n)) : (MvPolynomial.aeval z) (matMulPolynomial K n o) = matMul n z o

Over every commutative algebra, the polynomials evaluate to the product.

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

The polynomials evaluate to the product.

The cut bounds

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.mem_placeA {n s : ℕ} {S : Finset (Wire (n * n + n * n) s)} {i j : Fin n} : (i, j) ∈ Tripartite.place (matMulTermA n s) S ↔ matMulLeft n i j ∈ SingleCut.inputsIn S

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.mem_placeB {n s : ℕ} {S : Finset (Wire (n * n + n * n) s)} {j k : Fin n} : (j, k) ∈ Tripartite.place (matMulTermB n s) S ↔ matMulRight n j k ∈ SingleCut.inputsIn S

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.mem_placeC {n s : ℕ} {out : Fin (n * n) → Wire (n * n + n * n) s} {S : Finset (Wire (n * n + n * n) s)} {i k : Fin n} : (i, k) ∈ Tripartite.place (matMulTermC out) S ↔ matMulOutput n i k ∈ outputsIn out S

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.trace_eq_matMul {n : ℕ} {σ : Signature} {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) = matMulPolynomial K n o) (z : Fin (n * n + n * n) → K) (o : Fin (n * n)) : p.trace (Taylor.algebraInterpretation P K) z (out o) = matMul n z o

A program formally computing the polynomials computes the product over its coefficient field.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.chargeJ_le_of_formal {n : ℕ} {σ : Signature} {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) = matMulPolynomial K n o) (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 Hessian charge.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobianChargeI_le_of_formal {n : ℕ} {σ : Signature} {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) = matMulPolynomial K n o) (S : Finset (Wire (n * n + n * n) s)) : Tripartite.jacobianChargeI (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card

The row Jacobian charge.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobianChargeK_le_of_formal {n : ℕ} {σ : Signature} {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) = matMulPolynomial K n o) (S : Finset (Wire (n * n + n * n) s)) : Tripartite.jacobianChargeK (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card

The column Jacobian charge.

One component

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.one_le_blockRank {L : Type u_1} [Field L] {m N : ℕ} {M : Matrix (Fin m) (Fin N) L} {Y : Finset (Fin m)} {X : Finset (Fin N)} {y : Fin m} {x : Fin N} (hy : y ∈ Y) (hx : x ∈ X) (h : M y x ≠ 0) : 1 ≤ blockRank M Y X

A block with a nonzero entry has positive rank.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.mem_component_of_formal {n : ℕ} {σ : Signature} {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} (hn : 0 < n) (hf : ∀ (o : Fin (n * n)), Taylor.wirePolynomial P p (out o) = matMulPolynomial K n o) : (∀ (x : Fin (n * n + n * n)), Wire.input x ∈ component p (out (matMulOutput n ⟨0, hn⟩ ⟨0, hn⟩))) ∧ ∀ (o : Fin (n * n)), out o ∈ component p (out (matMulOutput n ⟨0, hn⟩ ⟨0, hn⟩))

All terminals lie in one component. If the wires out of a program with polynomial gates carry the polynomials of matrix multiplication and n ≥ 1, the component of the output C 0 0 contains every input and every output.

The finite bound

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

The finite bound. A fan-in-two program with polynomial gates over a field, whose wires out carry the polynomials of matrix multiplication, has (15 n² - 6 n - 9)/24 ≤ (A + η) (s - 2 n²)⁺ + 3 log₂ (2 n² + 3 s) + C.

Asymptotics

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.eventually_lt_of_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 → (15 * ↑n ^ 2 - 6 * ↑n - 9) / 24 ≤ (A + η) * max (↑s - 2 * ↑n ^ 2) 0 + 3 * Real.logb 2 (2 * ↑n ^ 2 + 3 * ↑s) + C) → (2 + 5 / (8 * A) - ε) * ↑n ^ 2 < ↑s

The asymptotic bound. If the graph-ordering hypothesis holds with coefficient A > 0 for every positive slack, then for every ε > 0 and all large n, every size s satisfying the finite bound for every ordering has s > (2 + 5/(8 A) - ε) n².