The three charges bound the crossing signals

Let the wires out of a program over a finite field carry matMul n, and split the wires into S and its complement, crossed by w signals, and place the terminals matMulTermA, matMulTermB, matMulTermC as in Tripartite (Tripartite.place). Each charge is bounded through the kernels of blocks of one n × n matrix, two blocks per vertex.

• Charge R_I, fixing B = B₀ (pow_le_mul_prodI). On the inputs with second factor B₀ the product is linear, and its change δA ↦ δA B₀ is block diagonal over the rows i. The restricted rank-cut bound (card_pow_le_supportedKernel_of_trace) and the rowSet decomposition of the kernels give |F| ^ (n²) ≤ |F| ^ w ∏ i, |ker₁ i| |ker₂ i|, where ker₁ i and ker₂ i are left kernels of the blocks B₀[rowSet a i, (rowSet c i)ᶜ] and B₀[(rowSet a i)ᶜ, rowSet c i].
• Charge R_K, fixing A = A₀ (pow_le_mul_prodK): symmetrically, over the columns k.
• Charge R_J, the Hessian (pow_le_mul_prodJ). The combination ∑ i k, Λ i k C i k is the quadratic form of bilinForm Λ, so the cross block of H = M + Mᵀ between the inputs in S and outside S has rank at most w (blockRank_add_transpose_le_of_sum). Its kernel is block diagonal over the inner index j, which gives |F| ^ |X_T| ≤ |F| ^ w ∏ j, |ker₁ j| |ker₂ j| with |X_T| the inputs outside S.

At a vertex with a and c placed terminals of its two kinds, a totally regular matrix makes the two kernels miss min (a, n - c) + min (n - a, c) = minority n (a + c) dimensions (prodI_mul_pow_le and its siblings), so each charge is at most w (chargeI_le_of_totallyRegular, ...). For a uniformly random matrix each kernel has average size at most twice the ideal one (sum_card_supportedKernel_mul_pow_le), so by averaging some matrix loses at most 4 n (exists_prodI_mul_pow_le, ...), and each charge is at most w + 4 n over every finite field (chargeI_le_add, ...).

Placing the terminals

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

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

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

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

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

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

Arithmetic of the per-vertex bounds

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.minority_add_eq {n a c : ℕ} (ha : a ≤ n) (hc : c ≤ n) : Tripartite.minority n (a + c) = min a (n - c) + min (n - a) c

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.prod_mul_pow_le {n q : ℕ} (K₁ K₂ p₁ p₂ m₁ m₂ : Fin n → ℕ) (h₁ : ∀ (v : Fin n), K₁ v * q ^ m₁ v ≤ q ^ p₁ v) (h₂ : ∀ (v : Fin n), K₂ v * q ^ m₂ v ≤ q ^ p₂ v) : (∏ v : Fin n, K₁ v * K₂ v) * q ^ ∑ v : Fin n, (m₁ v + m₂ v) ≤ q ^ ∑ v : Fin n, (p₁ v + p₂ v)

Multiplying the per-vertex bounds.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.exists_prod_mul_pow_le {n : ℕ} {X : Type u_1} [Fintype X] [Nonempty X] {q : ℕ} (hq : 1 < q) (K₁ K₂ : Fin n → X → ℕ) (hK₁ : ∀ (v : Fin n) (x : X), 0 < K₁ v x) (hK₂ : ∀ (v : Fin n) (x : X), 0 < K₂ v x) (p₁ p₂ m₁ m₂ : Fin n → ℕ) (hm₁ : ∀ (v : Fin n), m₁ v ≤ p₁ v) (hm₂ : ∀ (v : Fin n), m₂ v ≤ p₂ v) (h₁ : ∀ (v : Fin n), (∑ x : X, K₁ v x) * q ^ m₁ v ≤ 2 * Fintype.card X * q ^ p₁ v) (h₂ : ∀ (v : Fin n), (∑ x : X, K₂ v x) * q ^ m₂ v ≤ 2 * Fintype.card X * q ^ p₂ v) : ∃ (x : X), (∏ v : Fin n, K₁ v x * K₂ v x) * q ^ ∑ v : Fin n, (m₁ v + m₂ v) ≤ q ^ (∑ v : Fin n, (p₁ v + p₂ v) + 4 * n)

Averaging the per-vertex bounds. If the two families of kernels at each vertex average at most twice their ideal sizes, some choice loses at most 4 n in the exponent.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.le_add_of_pow_le {q E w R L X : ℕ} (hq : 1 < q) (h₁ : q ^ E ≤ q ^ w * X) (h₂ : X * q ^ R ≤ q ^ (E + L)) : R ≤ w + L

Comparing exponents. If q ^ E ≤ q ^ w X and X q ^ R ≤ q ^ (E + L), then R ≤ w + L.

Charge identities

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_compl_eq {n : ℕ} {X : Finset (Fin n)} : Xᶜ.card = n - X.card

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_le_n {n : ℕ} (X : Finset (Fin n)) : X.card ≤ n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_min_eq_chargeI {n : ℕ} (a c : Finset (Fin n × Fin n)) : ∑ i : Fin n, (min (Tripartite.rowSet a i).card (Tripartite.rowSet c i)ᶜ.card + min (Tripartite.rowSet a i)ᶜ.card (Tripartite.rowSet c i).card) = Tripartite.chargeI a c

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_min_eq_chargeK {n : ℕ} (b c : Finset (Fin n × Fin n)) : ∑ k : Fin n, (min (Tripartite.colSet b k).card (Tripartite.colSet c k)ᶜ.card + min (Tripartite.colSet b k)ᶜ.card (Tripartite.colSet c k).card) = Tripartite.chargeK b c

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_min_eq_chargeJ {n : ℕ} (a b : Finset (Fin n × Fin n)) : ∑ j : Fin n, (min (Tripartite.colSet a j)ᶜ.card (Tripartite.rowSet b j).card + min (Tripartite.rowSet b j)ᶜ.card (Tripartite.colSet a j).card) = Tripartite.chargeJ a b

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_card_add_card_compl {n : ℕ} (X : Fin n → Finset (Fin n)) : ∑ v : Fin n, ((X v).card + (X v)ᶜ.card) = n * n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_eq_sum_ite {α : Type u_1} [Fintype α] [DecidableEq α] (X : Finset α) : X.card = ∑ x : α, if x ∈ X then 1 else 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_compl_inputsIn {n s : ℕ} (S : Finset (Wire (n * n + n * n) s)) : (SingleCut.inputsIn S)ᶜ.card = ∑ j : Fin n, ((Tripartite.colSet (Tripartite.place (matMulTermA n s) S) j)ᶜ.card + (Tripartite.rowSet (Tripartite.place (matMulTermB n s) S) j)ᶜ.card)

The inputs outside S, counted at the vertices of J.

Kernel products

noncomputable def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.prodI {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (B₀ : Matrix (Fin n) (Fin n) F) (S : Finset (Wire (n * n + n * n) s)) (out : Fin (n * n) → Wire (n * n + n * n) s) : ℕ

The kernels of the rows of δA ↦ δA B₀ at the split S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.prodK {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (A₀ : Matrix (Fin n) (Fin n) F) (S : Finset (Wire (n * n + n * n) s)) (out : Fin (n * n) → Wire (n * n + n * n) s) : ℕ

The kernels of the columns of δB ↦ A₀ δB at the split S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.prodJ {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Λ : Matrix (Fin n) (Fin n) F) (S : Finset (Wire (n * n + n * n) s)) : ℕ

The kernels of the blocks of the Hessian of ∑ Λ i k C i k at the split S.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_supportedKernel_shiftLeft_le {n : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (B₀ : Matrix (Fin n) (Fin n) F) (P : Finset (Fin (n * n + n * n))) (hP : P ⊆ leftCoords n) (Q : Finset (Fin (n * n))) : (supportedKernel (shiftLeft B₀) P Q).card ≤ ∏ i : Fin n, (supportedKernel (fun (u : Fin n → F) => Matrix.vecMul u B₀) {j : Fin n | matMulLeft n i j ∈ P} {k : Fin n | matMulOutput n i k ∈ Q}).card

Row decomposition of the kernels with B fixed.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_supportedKernel_shiftRight_le {n : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (A₀ : Matrix (Fin n) (Fin n) F) (P : Finset (Fin (n * n + n * n))) (hP : P ⊆ rightCoords n) (Q : Finset (Fin (n * n))) : (supportedKernel (shiftRight A₀) P Q).card ≤ ∏ k : Fin n, (supportedKernel (fun (u : Fin n → F) => A₀.mulVec u) {j : Fin n | matMulRight n j k ∈ P} {i : Fin n | matMulOutput n i k ∈ Q}).card

Column decomposition of the kernels with A fixed.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.pow_le_mul_prodI {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p : Program σ (n * n + n * n) s} {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) (S : Finset (Wire (n * n + n * n) s)) (B₀ : Matrix (Fin n) (Fin n) F) : Fintype.card F ^ (n * n) ≤ Fintype.card F ^ ((SingleCut.forward p S).card + (SingleCut.backward p S).card) * prodI B₀ S out

The bound behind R_I. Fixing the second factor to B₀, |F| ^ (n²) ≤ |F| ^ w · prodI B₀ S.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.pow_le_mul_prodK {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p : Program σ (n * n + n * n) s} {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) (S : Finset (Wire (n * n + n * n) s)) (A₀ : Matrix (Fin n) (Fin n) F) : Fintype.card F ^ (n * n) ≤ Fintype.card F ^ ((SingleCut.forward p S).card + (SingleCut.backward p S).card) * prodK A₀ S out

The bound behind R_K. Fixing the first factor to A₀, |F| ^ (n²) ≤ |F| ^ w · prodK A₀ S.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_ker_le_prodJ {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Λ : Matrix (Fin n) (Fin n) F) (S : Finset (Wire (n * n + n * n) s)) : {v : ↥(SingleCut.inputsIn S)ᶜ → F | v ∈ ((bilinForm Λ + (bilinForm Λ).transpose).submatrix (fun (x : ↥(SingleCut.inputsIn S)) => ↑x) fun (y : ↥(SingleCut.inputsIn S)ᶜ) => ↑y).mulVecLin.ker}.card ≤ prodJ Λ S

Kernels of the Hessian block. The kernel of the cross block of H = M + Mᵀ between the inputs in S and outside S embeds in the product of the kernels at the vertices j.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.pow_le_mul_prodJ {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p : Program σ (n * n + n * n) s} {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) (S : Finset (Wire (n * n + n * n) s)) (Λ : Matrix (Fin n) (Fin n) F) : Fintype.card F ^ (SingleCut.inputsIn S)ᶜ.card ≤ Fintype.card F ^ ((SingleCut.forward p S).card + (SingleCut.backward p S).card) * prodJ Λ S

The bound behind R_J. For every Λ, with X_T the inputs outside S, |F| ^ |X_T| ≤ |F| ^ w · prodJ Λ S.

The charges

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.prodI_mul_pow_le {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {M : Matrix (Fin n) (Fin n) F} (hM : TotallyRegular M) (S : Finset (Wire (n * n + n * n) s)) (out : Fin (n * n) → Wire (n * n + n * n) s) : prodI M S out * Fintype.card F ^ Tripartite.chargeI (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermC out) S) ≤ Fintype.card F ^ (n * n)

Totally regular rows. If M is totally regular, prodI M S · |F| ^ R_I ≤ |F| ^ (n²).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.prodK_mul_pow_le {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {M : Matrix (Fin n) (Fin n) F} (hM : TotallyRegular M) (S : Finset (Wire (n * n + n * n) s)) (out : Fin (n * n) → Wire (n * n + n * n) s) : prodK M S out * Fintype.card F ^ Tripartite.chargeK (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ Fintype.card F ^ (n * n)

Totally regular columns. If M is totally regular, prodK M S · |F| ^ R_K ≤ |F| ^ (n²).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.prodJ_mul_pow_le {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {Λ : Matrix (Fin n) (Fin n) F} (hΛ : TotallyRegular Λ) (S : Finset (Wire (n * n + n * n) s)) : prodJ Λ S * Fintype.card F ^ Tripartite.chargeJ (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) ≤ Fintype.card F ^ (SingleCut.inputsIn S)ᶜ.card

A totally regular Hessian. If Λ is totally regular, prodJ Λ S · |F| ^ R_J ≤ |F| ^ |X_T|.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.exists_prodI_mul_pow_le {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Finset (Wire (n * n + n * n) s)) (out : Fin (n * n) → Wire (n * n + n * n) s) : ∃ (B₀ : Matrix (Fin n) (Fin n) F), prodI B₀ S out * Fintype.card F ^ Tripartite.chargeI (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermC out) S) ≤ Fintype.card F ^ (n * n + 4 * n)

Uniform rows. Some B₀ has prodI B₀ S · |F| ^ R_I ≤ |F| ^ (n² + 4 n).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.exists_prodK_mul_pow_le {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Finset (Wire (n * n + n * n) s)) (out : Fin (n * n) → Wire (n * n + n * n) s) : ∃ (A₀ : Matrix (Fin n) (Fin n) F), prodK A₀ S out * Fintype.card F ^ Tripartite.chargeK (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ Fintype.card F ^ (n * n + 4 * n)

Uniform columns. Some A₀ has prodK A₀ S · |F| ^ R_K ≤ |F| ^ (n² + 4 n).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.exists_prodJ_mul_pow_le {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Finset (Wire (n * n + n * n) s)) : ∃ (Λ : Matrix (Fin n) (Fin n) F), prodJ Λ S * Fintype.card F ^ Tripartite.chargeJ (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) ≤ Fintype.card F ^ ((SingleCut.inputsIn S)ᶜ.card + 4 * n)

A uniform Hessian. Some Λ has prodJ Λ S · |F| ^ R_J ≤ |F| ^ (|X_T| + 4 n).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.charges_le_of_totallyRegular {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p : Program σ (n * n + n * n) s} {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) {M : Matrix (Fin n) (Fin n) F} (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 ∧ 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, with a totally regular matrix. If F has a totally regular n × n matrix, each charge of every split is at most the number of crossing signals.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.charges_le_add {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p : Program σ (n * n + n * n) s} {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) (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 + 4 * n ∧ Tripartite.chargeJ (Tripartite.place (matMulTermA n s) S) (Tripartite.place (matMulTermB n s) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card + 4 * n ∧ Tripartite.chargeK (Tripartite.place (matMulTermB n s) S) (Tripartite.place (matMulTermC out) S) ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card + 4 * n

The three charges over every finite field. Each charge of every split is at most the number of crossing signals plus 4 n.