Proofs for the rank-cut bound

Fix a split S of the wires and the boundary key of an input x₀. Mixing an input with the same key into x₀ on the coordinates outside S keeps every output carried outside S (SingleCut.trace_mix), so the left parts of the fibre embed into the left fibre of x₀ (card_leftParts_le); symmetrically for the right parts. As the fibres of the key are products of their left and right parts (SingleCut.card_filter_boundaryKey_eq), summing over the keys gives |U| ^ n ≤ |U| ^ (|A| + |B|) · DT · DS (card_pow_le_of_fibres).

For a linear map x ↦ M x, the differences between a left fibre and its base point lie in the kernel of the block M[Y_T, X_S], so a left fibre has at most |F| ^ (|X_S| - r₁) elements (card_leftFibre_le), and the exponents compare to r₁ + r₂ ≤ |A| + |B|.

The general fibre bound

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_leftParts_le {σ : Signature} {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (out : Fin m → Wire n s) (f : (Fin n → U) → Fin m → U) (hf : ∀ (x : Fin n → U) (i : Fin m), p.trace I x (out i) = f x i) (S : Finset (Wire n s)) (x₀ : Fin n → U) : (SingleCut.leftParts p I S Finset.univ (SingleCut.boundaryKey p I S x₀)).card ≤ (leftFibre out f S x₀).card

The left parts of a fibre embed into the left fibre of any of its members.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_rightParts_le {σ : Signature} {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (out : Fin m → Wire n s) (f : (Fin n → U) → Fin m → U) (hf : ∀ (x : Fin n → U) (i : Fin m), p.trace I x (out i) = f x i) (S : Finset (Wire n s)) (x₀ : Fin n → U) : (SingleCut.rightParts p I S Finset.univ (SingleCut.boundaryKey p I S x₀)).card ≤ (rightFibre out f S x₀).card

The right parts of a fibre embed into the right fibre of any of its members.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_pow_inputsIn_le_of_leftFibre {σ : Signature} {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (out : Fin m → Wire n s) (f : (Fin n → U) → Fin m → U) (hf : ∀ (x : Fin n → U) (i : Fin m), p.trace I x (out i) = f x i) (S : Finset (Wire n s)) [Nonempty U] {DT : ℕ} (hT : ∀ (x : Fin n → U), (leftFibre out f S x).card ≤ DT) : Fintype.card U ^ (SingleCut.inputsIn S).card ≤ Fintype.card U ^ (SingleCut.forward p S).card * DT

The forward fibre bound. If every left fibre has at most DT elements, then |U| ^ |X_S| ≤ |U| ^ |A| · DT, using only the forward signals A = forward p S.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_pow_compl_inputsIn_le_of_rightFibre {σ : Signature} {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (out : Fin m → Wire n s) (f : (Fin n → U) → Fin m → U) (hf : ∀ (x : Fin n → U) (i : Fin m), p.trace I x (out i) = f x i) (S : Finset (Wire n s)) [Nonempty U] {DS : ℕ} (hS : ∀ (x : Fin n → U), (rightFibre out f S x).card ≤ DS) : Fintype.card U ^ (SingleCut.inputsIn S)ᶜ.card ≤ Fintype.card U ^ (SingleCut.backward p S).card * DS

The backward fibre bound. Symmetrically, if every right fibre has at most DS elements, then |U| ^ |X_T| ≤ |U| ^ |B| · DS, using only the backward signals B = backward p S.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_pow_le_of_fibres {σ : Signature} {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (out : Fin m → Wire n s) (f : (Fin n → U) → Fin m → U) (hf : ∀ (x : Fin n → U) (i : Fin m), p.trace I x (out i) = f x i) (S : Finset (Wire n s)) {DT DS : ℕ} (hT : ∀ (x : Fin n → U), (leftFibre out f S x).card ≤ DT) (hS : ∀ (x : Fin n → U), (rightFibre out f S x).card ≤ DS) : Fintype.card U ^ n ≤ Fintype.card U ^ ((SingleCut.forward p S).card + (SingleCut.backward p S).card) * (DT * DS)

The general fibre bound. If every left fibre has at most DT elements and every right fibre at most DS, then |U| ^ n ≤ |U| ^ (|A| + |B|) · DT · DS.

Linear maps

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_filter_mem_ker {F : Type u_2} [Field F] [Fintype F] {ι κ : Type} [Fintype ι] [DecidableEq ι] (B : Matrix κ ι F) [DecidablePred fun (x : ι → F) => x ∈ B.mulVecLin.ker] : {v : ι → F | v ∈ B.mulVecLin.ker}.card = Fintype.card F ^ (Fintype.card ι - B.rank)

The kernel of a matrix over a finite field has |F| ^ (width - rank) elements.

theorem Algebraic.Cutwidth.MultiOutput.Internal.sum_subtype_eq_sum {n : ℕ} {F : Type u_2} [Field F] {X : Finset (Fin n)} (g : Fin n → F) (hg : ∀ j ∉ X, g j = 0) : ∑ j : ↥X, g ↑j = ∑ j : Fin n, g j

Sums over the coordinates of a subset, with zero terms outside it, are full sums.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_leftFibre_le {n s m : ℕ} {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (out : Fin m → Wire n s) (M : Matrix (Fin m) (Fin n) F) (S : Finset (Wire n s)) (x : Fin n → F) : (leftFibre out (fun (x : Fin n → F) => M.mulVec x) S x).card ≤ Fintype.card F ^ ((SingleCut.inputsIn S).card - blockRank M (outputsIn out S)ᶜ (SingleCut.inputsIn S))

Left fibres of a linear map. The inputs that differ from x only on the coordinates in S and keep the outputs carried outside S differ from x by a kernel vector of the block M[Y_T, X_S]; there are at most |F| ^ (|X_S| - rank M[Y_T, X_S]) of them.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_rightFibre_le {n s m : ℕ} {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (out : Fin m → Wire n s) (M : Matrix (Fin m) (Fin n) F) (S : Finset (Wire n s)) (x : Fin n → F) : (rightFibre out (fun (x : Fin n → F) => M.mulVec x) S x).card ≤ Fintype.card F ^ ((SingleCut.inputsIn S)ᶜ.card - blockRank M (outputsIn out S) (SingleCut.inputsIn S)ᶜ)

Right fibres of a linear map. Symmetrically, there are at most |F| ^ (n - |X_S| - rank M[Y_S, X_T]) inputs differing from x only outside S and keeping the outputs carried in S.

theorem Algebraic.Cutwidth.MultiOutput.Internal.blockRank_le_forward {σ : Signature} {n s m : ℕ} {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (p : Program σ n s) (I : Interpretation σ F) (out : Fin m → Wire n s) (M : Matrix (Fin m) (Fin n) F) (hf : ∀ (x : Fin n → F) (i : Fin m), p.trace I x (out i) = M.mulVec x i) (S : Finset (Wire n s)) : blockRank M (outputsIn out S)ᶜ (SingleCut.inputsIn S) ≤ (SingleCut.forward p S).card

The forward rank-cut bound for a program. If the wires out carry the linear map x ↦ M x, then for every split S, rank M[Y_T, X_S] ≤ |A|, where A = forward p S.

theorem Algebraic.Cutwidth.MultiOutput.Internal.blockRank_le_backward {σ : Signature} {n s m : ℕ} {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (p : Program σ n s) (I : Interpretation σ F) (out : Fin m → Wire n s) (M : Matrix (Fin m) (Fin n) F) (hf : ∀ (x : Fin n → F) (i : Fin m), p.trace I x (out i) = M.mulVec x i) (S : Finset (Wire n s)) : blockRank M (outputsIn out S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.backward p S).card

The backward rank-cut bound for a program. Symmetrically, if the wires out carry the linear map x ↦ M x, then for every split S, rank M[Y_S, X_T] ≤ |B|, where B = backward p S.

theorem Algebraic.Cutwidth.MultiOutput.Internal.blockRank_add_blockRank_le {σ : Signature} {n s m : ℕ} {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (p : Program σ n s) (I : Interpretation σ F) (out : Fin m → Wire n s) (M : Matrix (Fin m) (Fin n) F) (hf : ∀ (x : Fin n → F) (i : Fin m), p.trace I x (out i) = M.mulVec x i) (S : Finset (Wire n s)) : blockRank M (outputsIn out S)ᶜ (SingleCut.inputsIn S) + blockRank M (outputsIn out S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card

The rank-cut bound for a program. If the wires out carry the linear map x ↦ M x, then for every split S, rank M[Y_T, X_S] + rank M[Y_S, X_T] ≤ |A| + |B|.