Light–heavy accounting with the Jacobian charges

Let a split place the terminals a, b, c (MatMul.Tripartite.Defs), with heavy vertices H_I, H_J, H_K of sizes x, y, z. As in MatMul.Tripartite, a terminal with one light and one heavy endpoint is charged to its light endpoint if it is placed and to its heavy endpoint otherwise; A_I, A_J, B_J, B_K count the charged A and B terminals by the part of the endpoint they are charged to, and C is the number of light–heavy C terminals.

• The Hessian charge (sum_ite_add_sum_ite_le_chargeJ): A_J + B_J ≤ R_J.
• The row Jacobian charge (card_mixedPairs_add_le_jacobianChargeI): C + B_K ≤ L_I + z (n - x - y)⁺ + (n - z) (x + y - n)⁺, where L_I = jacobianChargeI a b c. At a heavy row i the forward term is the number of unplaced C i k, at a light row the backward term is the number of placed C i k; these are the C terminals charged to i together with the placed light–light and unplaced heavy–heavy ones (rowTerm_eq). At a column k the two terms pay for the C terminals charged to k, and for the B terminals charged to k up to the light–light and heavy–heavy C terminals at k and an overshoot (colTerm_le). The two counts of the light–light and heavy–heavy C terminals agree (sum_ite_inter_eq), so they cancel.
• The column Jacobian charge (card_mixedPairs_add_le_jacobianChargeK): the mirror image C + A_I ≤ L_K + x (n - y - z)⁺ + (n - x) (y + z - n)⁺, obtained by transposing the terminal graph (swapPairs).
• Near the threshold (fifteen_mul_sq_le_of_threshold, fifteen_mul_sq_le). If 3 n ≤ 2 (x + y + z) ≤ 3 n + 3, the total P + C - corr of these bounds, with P the number of light–heavy terminals and corr the two overshoot terms, is at least (15 n² - 6 n - 9)/8, so 15 n² ≤ 8 (R_J + L_I + L_K) + 6 n + 9. With x = n/2 + u, z = n/2 + w and δ = x + y + z - 3 n/2, the total is 2 n² + φ(u) + φ(w) with φ(u) = u² - δ u - (n/2) |u - δ| ≥ -(n/2 + δ)²/4.

Sets of pairs

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

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

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.card_inter_add_card_inter_compl {n : ℕ} (s T : Finset (Fin n)) : (s ∩ T).card + (s ∩ Tᶜ).card = s.card

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.rowSet_compl {n : ℕ} (s : Finset (Fin n × Fin n)) (i : Fin n) : Tripartite.rowSet sᶜ i = (Tripartite.rowSet s i)ᶜ

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.colSet_compl {n : ℕ} (s : Finset (Fin n × Fin n)) (j : Fin n) : Tripartite.colSet sᶜ j = (Tripartite.colSet s j)ᶜ

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_ite_mem {n : ℕ} (Y : Finset (Fin n)) (α β : ℕ) : (∑ k : Fin n, if k ∈ Y then α else β) = Y.card * α + (n - Y.card) * β

A sum of a two-valued function over the vertices.

The row charge

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.rowTerm_eq {n : ℕ} (a c : Finset (Fin n × Fin n)) (HK : Finset (Fin n)) (i : Fin n) : ((if i ∈ Tripartite.heavyI a c then min (Tripartite.rowSet c i)ᶜ.card (Tripartite.rowSet a i).card else 0) + if i ∈ (Tripartite.heavyI a c)ᶜ then min (Tripartite.rowSet c i).card (Tripartite.rowSet a i)ᶜ.card else 0) = (if i ∈ Tripartite.heavyI a c then ((Tripartite.rowSet c i)ᶜ ∩ HKᶜ).card else (Tripartite.rowSet c i ∩ HK).card) + if i ∈ Tripartite.heavyI a c then ((Tripartite.rowSet c i)ᶜ ∩ HK).card else (Tripartite.rowSet c i ∩ HKᶜ).card

A row pays for its C terminals. At a heavy row the forward term counts the unplaced C i k, at a light row the backward term counts the placed ones; split by the column k.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.colTerm_le {n : ℕ} (b c : Finset (Fin n × Fin n)) (HI HJ : Finset (Fin n)) (k : Fin n) : ((if k ∈ Tripartite.heavyK b c then ((Tripartite.colSet c k)ᶜ ∩ HIᶜ).card else (Tripartite.colSet c k ∩ HI).card) + if k ∈ Tripartite.heavyK b c then ((Tripartite.colSet b k)ᶜ ∩ HJᶜ).card else (Tripartite.colSet b k ∩ HJ).card) ≤ min ((Tripartite.colSet c k)ᶜ \ HI).card (Tripartite.colSet b k).card + min (Tripartite.colSet c k \ HIᶜ).card (Tripartite.colSet b k)ᶜ.card + ((if k ∈ Tripartite.heavyK b c then ((Tripartite.colSet c k)ᶜ ∩ HI).card else (Tripartite.colSet c k ∩ HIᶜ).card) + if k ∈ Tripartite.heavyK b c then n - (HI.card + HJ.card) else HI.card + HJ.card - n)

A column pays for its charged terminals. At a column k, the two Jacobian terms pay for the C terminals charged to k and for the B terminals charged to k, up to the heavy–heavy (at a heavy column) or light–light (at a light column) C terminals at k and an overshoot (n - x - y)⁺ or (x + y - n)⁺.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_ite_inter_eq {n : ℕ} (c : Finset (Fin n × Fin n)) (X Y : Finset (Fin n)) : (∑ i : Fin n, if i ∈ X then ((Tripartite.rowSet c i)ᶜ ∩ Y).card else (Tripartite.rowSet c i ∩ Yᶜ).card) = ∑ k : Fin n, if k ∈ Y then ((Tripartite.colSet c k)ᶜ ∩ X).card else (Tripartite.colSet c k ∩ Xᶜ).card

The light–light and heavy–heavy C terminals, counted at their rows and at their columns.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.card_mixedPairs_add_le_jacobianChargeI {n : ℕ} (a b c : Finset (Fin n × Fin n)) (HJ : Finset (Fin n)) : ((Tripartite.mixedPairs (Tripartite.heavyI a c) (Tripartite.heavyK b c)).card + ∑ k : Fin n, if k ∈ Tripartite.heavyK b c then ((Tripartite.colSet b k)ᶜ ∩ HJᶜ).card else (Tripartite.colSet b k ∩ HJ).card) ≤ Tripartite.jacobianChargeI a b c + (Tripartite.heavyK b c).card * (n - ((Tripartite.heavyI a c).card + HJ.card)) + (n - (Tripartite.heavyK b c).card) * ((Tripartite.heavyI a c).card + HJ.card - n)

The row Jacobian charge. The light–heavy C terminals and the B terminals charged to their K endpoints number at most L_I + z (n - x - y)⁺ + (n - z) (x + y - n)⁺, for any set HJ of size y in place of the heavy vertices of J.

Transposing the terminal graph

def Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.swapPairs {n : ℕ} (s : Finset (Fin n × Fin n)) : Finset (Fin n × Fin n)

The transposed set of pairs.

Equations

• Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.swapPairs s = Finset.map (Equiv.prodComm (Fin n) (Fin n)).toEmbedding s

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.mem_swapPairs {n : ℕ} {s : Finset (Fin n × Fin n)} {q : Fin n × Fin n} : q ∈ swapPairs s ↔ q.swap ∈ s

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.rowSet_swapPairs {n : ℕ} (s : Finset (Fin n × Fin n)) (k : Fin n) : Tripartite.rowSet (swapPairs s) k = Tripartite.colSet s k

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.colSet_swapPairs {n : ℕ} (s : Finset (Fin n × Fin n)) (i : Fin n) : Tripartite.colSet (swapPairs s) i = Tripartite.rowSet s i

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.swapPairs_compl {n : ℕ} (s : Finset (Fin n × Fin n)) : swapPairs sᶜ = (swapPairs s)ᶜ

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.heavyI_swapPairs {n : ℕ} (b c : Finset (Fin n × Fin n)) : Tripartite.heavyI (swapPairs b) (swapPairs c) = Tripartite.heavyK b c

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.heavyK_swapPairs {n : ℕ} (a c : Finset (Fin n × Fin n)) : Tripartite.heavyK (swapPairs a) (swapPairs c) = Tripartite.heavyI a c

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.heavyJ_swapPairs {n : ℕ} (a b : Finset (Fin n × Fin n)) : Tripartite.heavyJ (swapPairs b) (swapPairs a) = Tripartite.heavyJ a b

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobianRows_swapPairs {n : ℕ} (cY aX bX : Finset (Fin n × Fin n)) (H : Finset (Fin n)) : Tripartite.jacobianRows (swapPairs cY) (swapPairs bX) (swapPairs aX) H = Tripartite.jacobianCols cY aX bX H

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobianChargeI_swapPairs {n : ℕ} (a b c : Finset (Fin n × Fin n)) : Tripartite.jacobianChargeI (swapPairs b) (swapPairs a) (swapPairs c) = Tripartite.jacobianChargeK a b c

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.card_mixedPairs_add_le_jacobianChargeK {n : ℕ} (a b c : Finset (Fin n × Fin n)) (HJ : Finset (Fin n)) : ((Tripartite.mixedPairs (Tripartite.heavyK b c) (Tripartite.heavyI a c)).card + ∑ i : Fin n, if i ∈ Tripartite.heavyI a c then ((Tripartite.rowSet a i)ᶜ ∩ HJᶜ).card else (Tripartite.rowSet a i ∩ HJ).card) ≤ Tripartite.jacobianChargeK a b c + (Tripartite.heavyI a c).card * (n - ((Tripartite.heavyK b c).card + HJ.card)) + (n - (Tripartite.heavyI a c).card) * ((Tripartite.heavyK b c).card + HJ.card - n)

The column Jacobian charge. The light–heavy C terminals and the A terminals charged to their I endpoints number at most L_K + x (n - y - z)⁺ + (n - x) (y + z - n)⁺.

The Hessian charge

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_ite_add_sum_ite_le_chargeJ {n : ℕ} (a b c : Finset (Fin n × Fin n)) : ((∑ j : Fin n, if j ∈ Tripartite.heavyJ a b then ((Tripartite.colSet a j)ᶜ ∩ (Tripartite.heavyI a c)ᶜ).card else (Tripartite.colSet a j ∩ Tripartite.heavyI a c).card) + ∑ j : Fin n, if j ∈ Tripartite.heavyJ a b then ((Tripartite.rowSet b j)ᶜ ∩ (Tripartite.heavyK b c)ᶜ).card else (Tripartite.rowSet b j ∩ Tripartite.heavyK b c).card) ≤ Tripartite.chargeJ a b

The Hessian charge pays for the terminals charged to J.

Near the threshold

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.fifteen_mul_sq_le_of_threshold {n x y z : ℕ} (hx : x ≤ n) (hy : y ≤ n) (hz : z ≤ n) (hlo : 3 * n ≤ 2 * (x + y + z)) (hhi : 2 * (x + y + z) ≤ 3 * n + 3) : 15 * n ^ 2 + 8 * (z * (n - (x + y)) + (n - z) * (x + y - n) + (x * (n - (z + y)) + (n - x) * (z + y - n))) ≤ 8 * (x * (n - y) + (n - x) * y + (y * (n - z) + (n - y) * z) + (x * (n - z) + (n - x) * z) + (z * (n - x) + (n - z) * x)) + 6 * n + 9

The arithmetic of the threshold. If 3 n ≤ 2 (x + y + z) ≤ 3 n + 3, the light–heavy terminals, plus the light–heavy C terminals once more, minus the two overshoot corrections, number at least (15 n² - 6 n - 9)/8.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.fifteen_mul_sq_le {n : ℕ} (a b c : Finset (Fin n × Fin n)) (hlo : 3 * n ≤ 2 * Tripartite.heavyCount a b c) (hhi : 2 * Tripartite.heavyCount a b c ≤ 3 * n + 3) : 15 * n ^ 2 ≤ 8 * (Tripartite.chargeJ a b + Tripartite.jacobianChargeI a b c + Tripartite.jacobianChargeK a b c) + 6 * n + 9

The charging inequality with the Jacobian charges. Near the threshold, 15 n² ≤ 8 (R_J + L_I + L_K) + 6 n + 9.