The terminal graph of matrix multiplication #
The terminals of n × n matrix multiplication C = A B are the edges of the complete
tripartite graph on three copies I, J, K of Fin n (Tripartite.Defs): A i j joins
i and j, B j k joins j and k, C i k joins i and k. A split of the wires of a
circuit places d v of the 2 n terminals at each vertex v, and the minority
g (d) = min (d, 2 n - d) is the smaller of the two counts. The sums of g over I, J and
K are the charges R_I, R_J, R_K; for matrix multiplication they bound the ranks of the
linear maps obtained by fixing B (R_I), by fixing A (R_K), and the cross block of the
Hessian of a combination of the outputs (R_J), so each is at most the number of signals
crossing the split. This file proves the combinatorics, independently of circuits.
Charging (lightHeavy_le_charge). Call a vertex heavy when d v ≥ n. A terminal with a
light endpoint u and a heavy endpoint v is charged to u if it is placed, and to v
otherwise: at a light vertex g counts the placed terminals, at a heavy one the unplaced ones.
So the number P of light–heavy terminals is at most R_I + R_J + R_K.
Counting (card_mixedPairs, three_mul_sq_le_two_mul_lightHeavy). With x, y, z heavy
vertices in I, J, K and h = x + y + z, P = 2 n h - 2 (x y + y z + z x), which is at least
2 n h - 2 h² / 3. If 3 n ≤ 2 h ≤ 3 n + 3, this gives 3 n² ≤ 2 P + 3, so
3 n² ≤ 2 (R_I + R_J + R_K) + 3 (three_mul_sq_le_two_mul_charge): one of the three charges is
at least (n² - 1)/2.
The threshold prefix (exists_threshold). The degrees sum to twice the number of placed
terminals, so placing one more terminal adds at most two heavy vertices
(heavyCount_le_add_two). Along an injective ranking of the wires of a circuit whose 3 n²
terminals lie on distinct wires, the heavy count of the prefixes thus climbs from 0 to 3 n
in steps of at most two, and the first prefix with at least ⌈3 n/2⌉ heavy vertices ends at a
terminal and satisfies 3 n ≤ 2 h ≤ 3 n + 3.
Exploratory probes (probeIJ, twoSubsetProbeIJ). These are bookkeeping definitions for a
possible combined I/J charge, recorded with the identities that relate them to the existing
charges; they are not used by any lower bound. At i ∈ I the minority splits as
minority n (r + s) = min r (n - s) + min (n - r) s (minority_add_eq), with r and s the
placed A- and C-terminals at i; at j ∈ J it splits likewise, with the A- and
B-terminals at j. twoSubsetProbeIJ a b c I₀ I₁ counts the first I-summand over I₀, the
second over I₁, and the two J-summands with their A-terminals restricted to the rows of
I₀ᶜ and I₁ᶜ; probeIJ a b c I₀ is the case I₀ = I₁ (twoSubsetProbeIJ_self), and equals
chargeJ for I₀ = ∅ and chargeI for I₀ = univ (probeIJ_empty, probeIJ_univ). Each
summand min x (n - y) or min x y falls short of x by x + y - n or x - y, and the x
add up to the n² entries of A, giving twoSubsetProbeIJ + (shortfalls) = n²
(twoSubsetProbeIJ_add_eq). For I₀ = (heavyI a c)ᶜ, I₁ = heavyI a c the I-shortfalls
vanish (twoSubsetProbeIJ_compl_heavyI_add_eq), and the probe is at least the number of
light–heavy A-terminals (card_mixedPairs_le_twoSubsetProbeIJ).
No theorem in the library bounds the number of signals crossing a split below by probeIJ or
twoSubsetProbeIJ: their I- and J-summands come from ranks of different linear maps (a
Jacobian and a Hessian block), which are not known to add. In particular these probes do not
improve the matrix-multiplication bound.
The minority function #
Charging #
The light–heavy terminals near the threshold. If the heavy vertices number h with
3 n ≤ 2 h ≤ 3 n + 3, the light–heavy terminals number P with 3 n² ≤ 2 P + 3.
The charging inequality. If the heavy vertices number h with 3 n ≤ 2 h ≤ 3 n + 3,
then 3 n² ≤ 2 (R_I + R_J + R_K) + 3.
The threshold prefix #
The threshold prefix. Let the terminals tA, tB, tC of n × n matrix multiplication,
n ≥ 1, lie on distinct wires, and rank the wires injectively below T. Some prefix of the
ranking ends at a terminal, ranked t, and the wires ranked below t + 1 have h heavy
vertices with 3 n ≤ 2 h ≤ 3 n + 3.
Exploratory probes mixing the I and J charges #
At j ∈ J, with x = (colSetIn a I₀ᶜ j).card, x' = (complColSetIn a I₁ᶜ j).card and
y = (rowSet b j).card, the summands min x (n - y) and min x' y of twoSubsetProbeIJ fall
short of x and x' by x + y - n and x' - y.
The single-subset case of min_colSetIn_add_min_complColSetIn_add_eq: the two J-summands
at j restricted to the rows of R, plus their shortfalls, add up to R.card.
Bookkeeping identity for twoSubsetProbeIJ. The probe plus the shortfalls of its
summands (the excesses over I₀, the deficits over I₁, and the J-shortfalls of
min_colSetIn_add_min_complColSetIn_add_eq) is n².
The case I₀ = I₁ of twoSubsetProbeIJ_add_eq, for probeIJ.
The case I₀ = (heavyI a c)ᶜ, I₁ = heavyI a c of twoSubsetProbeIJ_add_eq, where the
excesses over the light rows and the deficits over the heavy rows vanish.
The A-terminals with exactly one heavy endpoint number at most
twoSubsetProbeIJ a b c (heavyI a c)ᶜ (heavyI a c): the charging of lightHeavy_le_charge,
restricted to the A-terminals, pays for each of them from one of the probe's summands.
probeIJ a b c (heavyI a c)ᶜ is at least the placed terminals at the light rows of I, plus,
at each j ∈ J, the A-terminals A i j with heavy i that are placed (for light j) or
unplaced (for heavy j).