The terminal graph of matrix multiplication: definitions

The 3 n² terminals of n × n matrix multiplication C = A B, the inputs A i j and B j k and the outputs C i k, are the edges of the complete tripartite graph on three copies I, J, K of Fin n: A i j joins i ∈ I to j ∈ J, B j k joins j ∈ J to k ∈ K, and C i k joins i ∈ I to k ∈ K. Every vertex has degree 2 n.

A split of the wires of a circuit places some terminals on its side S. We record the placed terminals of each kind as a set of index pairs: a holds the pairs (i, j) with A i j placed, b the pairs (j, k) with B j k placed, and c the pairs (i, k) with C i k placed.

• rowSet a i and colSet a j: the second coordinates paired with i, and the first coordinates paired with j.
• degI a c i, degJ a b j, degK b c k: the number of placed terminals at a vertex.
• minority n d = min d (2 n - d): the smaller of the numbers of terminals at a vertex of degree 2 n on the two sides, when d of them are placed.
• chargeI a c, chargeJ a b, chargeK b c: the sums of minority over the vertices of I, J and K. For matrix multiplication they are lower bounds for ranks of three linear maps read off the split: fixing B (chargeI), fixing A (chargeK), and the cross block of the Hessian of ∑ Λ i k C i k (chargeJ).
• heavyI a c, heavyJ a b, heavyK b c: the heavy vertices, with at least n placed terminals; heavyCount a b c counts them.
• excessI a c i, deficitI a c i: the excess deg - n and deficit n - deg of a vertex of I relative to the threshold n.
• colSetIn a R j and complColSetIn a R j: the rows i ∈ R with A i j placed, resp. unplaced.
• probeIJ a b c I₀ and twoSubsetProbeIJ a b c I₀ I₁: exploratory sums mixing the I and J charges along subsets of I. They are combinatorial quantities only; no rank-cut theorem relates them to the signals crossing a split.
• mixedPairs X Y: the pairs (x, y) with exactly one of x ∈ X and y ∈ Y.
• lightHeavy a b c: the number of terminals with exactly one heavy endpoint.
• place t S: the index pairs whose terminal wire t p lies in a set of wires S.

def Algebraic.Cutwidth.MultiOutput.Tripartite.rowSet {n : ℕ} (a : Finset (Fin n × Fin n)) (i : Fin n) : Finset (Fin n)

Row i of a set of index pairs: the second coordinates paired with i.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.rowSet a i = {j : Fin n | (i, j) ∈ a}

def Algebraic.Cutwidth.MultiOutput.Tripartite.colSet {n : ℕ} (a : Finset (Fin n × Fin n)) (j : Fin n) : Finset (Fin n)

Column j of a set of index pairs: the first coordinates paired with j.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.colSet a j = {i : Fin n | (i, j) ∈ a}

def Algebraic.Cutwidth.MultiOutput.Tripartite.degI {n : ℕ} (a c : Finset (Fin n × Fin n)) (i : Fin n) : ℕ

The placed terminals at the vertex i ∈ I: the entries A i j and C i k.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.degI a c i = (Algebraic.Cutwidth.MultiOutput.Tripartite.rowSet a i).card + (Algebraic.Cutwidth.MultiOutput.Tripartite.rowSet c i).card

def Algebraic.Cutwidth.MultiOutput.Tripartite.degJ {n : ℕ} (a b : Finset (Fin n × Fin n)) (j : Fin n) : ℕ

The placed terminals at the vertex j ∈ J: the entries A i j and B j k.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.degJ a b j = (Algebraic.Cutwidth.MultiOutput.Tripartite.colSet a j).card + (Algebraic.Cutwidth.MultiOutput.Tripartite.rowSet b j).card

def Algebraic.Cutwidth.MultiOutput.Tripartite.degK {n : ℕ} (b c : Finset (Fin n × Fin n)) (k : Fin n) : ℕ

The placed terminals at the vertex k ∈ K: the entries B j k and C i k.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.degK b c k = (Algebraic.Cutwidth.MultiOutput.Tripartite.colSet b k).card + (Algebraic.Cutwidth.MultiOutput.Tripartite.colSet c k).card

def Algebraic.Cutwidth.MultiOutput.Tripartite.minority (n d : ℕ) : ℕ

The smaller side at a vertex of degree 2 n with d placed terminals.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.minority n d = min d (2 * n - d)

def Algebraic.Cutwidth.MultiOutput.Tripartite.chargeI {n : ℕ} (a c : Finset (Fin n × Fin n)) : ℕ

The charge of the vertices of I.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.chargeI a c = ∑ i : Fin n, Algebraic.Cutwidth.MultiOutput.Tripartite.minority n (Algebraic.Cutwidth.MultiOutput.Tripartite.degI a c i)

def Algebraic.Cutwidth.MultiOutput.Tripartite.chargeJ {n : ℕ} (a b : Finset (Fin n × Fin n)) : ℕ

The charge of the vertices of J.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.chargeJ a b = ∑ j : Fin n, Algebraic.Cutwidth.MultiOutput.Tripartite.minority n (Algebraic.Cutwidth.MultiOutput.Tripartite.degJ a b j)

def Algebraic.Cutwidth.MultiOutput.Tripartite.chargeK {n : ℕ} (b c : Finset (Fin n × Fin n)) : ℕ

The charge of the vertices of K.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.chargeK b c = ∑ k : Fin n, Algebraic.Cutwidth.MultiOutput.Tripartite.minority n (Algebraic.Cutwidth.MultiOutput.Tripartite.degK b c k)

def Algebraic.Cutwidth.MultiOutput.Tripartite.heavyI {n : ℕ} (a c : Finset (Fin n × Fin n)) : Finset (Fin n)

The heavy vertices of I: at least n placed terminals.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.heavyI a c = {i : Fin n | n ≤ Algebraic.Cutwidth.MultiOutput.Tripartite.degI a c i}

def Algebraic.Cutwidth.MultiOutput.Tripartite.heavyJ {n : ℕ} (a b : Finset (Fin n × Fin n)) : Finset (Fin n)

The heavy vertices of J.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.heavyJ a b = {j : Fin n | n ≤ Algebraic.Cutwidth.MultiOutput.Tripartite.degJ a b j}

def Algebraic.Cutwidth.MultiOutput.Tripartite.heavyK {n : ℕ} (b c : Finset (Fin n × Fin n)) : Finset (Fin n)

The heavy vertices of K.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.heavyK b c = {k : Fin n | n ≤ Algebraic.Cutwidth.MultiOutput.Tripartite.degK b c k}

def Algebraic.Cutwidth.MultiOutput.Tripartite.heavyCount {n : ℕ} (a b c : Finset (Fin n × Fin n)) : ℕ

The number of heavy vertices.

Equations

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

def Algebraic.Cutwidth.MultiOutput.Tripartite.excessI {n : ℕ} (a c : Finset (Fin n × Fin n)) (i : Fin n) : ℕ

The excess degI a c i - n of i ∈ I over the threshold n (zero unless i is heavy).

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.excessI a c i = Algebraic.Cutwidth.MultiOutput.Tripartite.degI a c i - n

def Algebraic.Cutwidth.MultiOutput.Tripartite.deficitI {n : ℕ} (a c : Finset (Fin n × Fin n)) (i : Fin n) : ℕ

The deficit n - degI a c i of i ∈ I below the threshold n (zero if i is heavy).

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.deficitI a c i = n - Algebraic.Cutwidth.MultiOutput.Tripartite.degI a c i

def Algebraic.Cutwidth.MultiOutput.Tripartite.colSetIn {n : ℕ} (a : Finset (Fin n × Fin n)) (R : Finset (Fin n)) (j : Fin n) : Finset (Fin n)

The first coordinates in R paired with j in a: the placed terminals A i j with i ∈ R.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.colSetIn a R j = {x ∈ Algebraic.Cutwidth.MultiOutput.Tripartite.colSet a j | x ∈ R}

def Algebraic.Cutwidth.MultiOutput.Tripartite.complColSetIn {n : ℕ} (a : Finset (Fin n × Fin n)) (R : Finset (Fin n)) (j : Fin n) : Finset (Fin n)

The first coordinates in R not paired with j in a: the unplaced terminals A i j with i ∈ R.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.complColSetIn a R j = {x ∈ R | x ∉ Algebraic.Cutwidth.MultiOutput.Tripartite.colSet a j}

def Algebraic.Cutwidth.MultiOutput.Tripartite.probeIJ {n : ℕ} (a b c : Finset (Fin n × Fin n)) (I₀ : Finset (Fin n)) : ℕ

An exploratory probe mixing the I and J charges along a subset I₀ of I: the I-charge minority n (degI a c i) of the rows i ∈ I₀, plus, at each j ∈ J, the two summands of minority n (degJ a b j) = min x (n - y) + min (n - x) y (minority_add_eq, with x = (colSet a j).card, y = (rowSet b j).card) with the A-terminals restricted to the rows of I₀ᶜ. It interpolates between chargeJ (I₀ = ∅) and chargeI (I₀ = univ).

This is a combinatorial quantity only: no theorem bounds the number of signals crossing a split below by it.

Equations

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

def Algebraic.Cutwidth.MultiOutput.Tripartite.twoSubsetProbeIJ {n : ℕ} (a b c : Finset (Fin n × Fin n)) (I₀ I₁ : Finset (Fin n)) : ℕ

A two-subset variant of probeIJ. At i ∈ I, minority n (degI a c i) is the sum of min r (n - s) and min (n - r) s (minority_add_eq, with r = (rowSet a i).card, s = (rowSet c i).card); here the first summand is counted over I₀ and the second over I₁. At each j ∈ J, the two summands of minority n (degJ a b j) are counted with the A-terminals restricted to the rows of I₀ᶜ and of I₁ᶜ respectively. As for probeIJ, the arguments are the rows charged on the I side, and twoSubsetProbeIJ a b c I₀ I₀ = probeIJ a b c I₀.

This is a combinatorial quantity only: no theorem bounds the number of signals crossing a split below by it.

Equations

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

def Algebraic.Cutwidth.MultiOutput.Tripartite.mixedPairs {n : ℕ} (X Y : Finset (Fin n)) : Finset (Fin n × Fin n)

The pairs (x, y) with exactly one of x ∈ X and y ∈ Y.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.mixedPairs X Y = {p : Fin n × Fin n | ¬(p.1 ∈ X ↔ p.2 ∈ Y)}

def Algebraic.Cutwidth.MultiOutput.Tripartite.lightHeavy {n : ℕ} (a b c : Finset (Fin n × Fin n)) : ℕ

The number of terminals with exactly one heavy endpoint.

Equations

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

def Algebraic.Cutwidth.MultiOutput.Tripartite.place {n N s : ℕ} (t : Fin n × Fin n → Wire N s) (S : Finset (Wire N s)) : Finset (Fin n × Fin n)

The index pairs whose terminal wire lies in S.

Equations

• Algebraic.Cutwidth.MultiOutput.Tripartite.place t S = {p : Fin n × Fin n | t p ∈ S}