Proofs for the terminal graph of matrix multiplication #
- Charging (
lightHeavy_le_charge). A terminal with a light endpointuand a heavy endpointvis charged touif it is placed and tovotherwise. At a light vertex the minority is the number of placed terminals, at a heavy vertex the number of unplaced ones (le_minority), so every vertex pays for the terminals charged to it. Each terminal type is handled bysum_ite_add_sum_ite_eq_card_mixedPairs. - Counting (
card_mixedPairs,three_mul_sq_le_two_mul_lightHeavy). Withx,y,zheavy vertices in the three parts andh = x + y + z, the light–heavy terminals number2 n h - 2 (x y + y z + z x) ≥ 2 n h - 2 h² / 3, which is at least3 n² / 2 - 3 / 2when3 n ≤ 2 h ≤ 3 n + 3. - Threshold (
heavyCount_le_add_two,exists_threshold). The degrees sum to twice the number of placed terminals, so placing one more terminal raises the heavy count by at most two. Along a ranking of the wires, the heavy count of the prefixes thus climbs from0to3 nin steps of at most two, and the first prefix with at least⌈3 n/2⌉heavy vertices ends at a terminal and has at most⌈3 n/2⌉ + 1. - Exploratory probes (
twoSubsetProbeIJ_add_eq,card_mixedPairs_le_twoSubsetProbeIJ,sum_light_heavy_le_probeIJ). Splitting each minority into its two summands (minority_add_eq) and double counting theA-terminals by rows and by columns (sum_card_colSetIn,sum_card_complColSetIn) gives the bookkeeping identitytwoSubsetProbeIJ + (shortfalls) = n². These are combinatorial facts only; nothing here relates the probes to the signals crossing a split.
The minority function #
A vertex pays for its charged terminals. A vertex with placed neighbours m₁ in one part
and m₂ in the other is charged, when light, its placed terminals whose other endpoint is heavy
(in h₁, h₂), and when heavy, its unplaced terminals whose other endpoint is light.
Counting the light–heavy terminals #
The two endpoints of a terminal type pay exactly once. For a set a of index pairs and
heavy sets X and Y, the charges paid by the first coordinates and by the second coordinates
add up to the number of mixed pairs.
The light–heavy count near the threshold. If the heavy vertices number h with
3 n ≤ 2 h ≤ 3 n + 3, then 3 n² ≤ 2 P + 3 for the number P of light–heavy terminals.
The charging inequality. Near the threshold, 3 n² ≤ 2 (R_I + R_J + R_K) + 3.
Placing one more terminal #
Placing one more terminal adds at most two heavy vertices. The degrees sum to twice the number of placed terminals.
The threshold prefix #
A prefix gains at most one terminal per rank.
The threshold prefix. Along an injective ranking of the wires, if the 3 n² terminals lie
on distinct wires, some prefix ending at a terminal has h heavy vertices with
3 n ≤ 2 h ≤ 3 n + 3.
Exploratory probes mixing the I and J charges #
At a vertex of degree 2 n whose terminals split into two groups of n, with x and y
placed, the minority is min x (n - y) + min (n - x) y.
The two J-summands of twoSubsetProbeIJ at j fall short of the restricted counts x and
x' of A-terminals by x + y - n and x' - y.
The single-subset case of min_colSetIn_add_min_complColSetIn_add_eq: the two J-summands
restricted to the rows of R and their shortfalls add up to R.card.