The rank-cut bound

Split the wires of a multi-output circuit into S and its complement T, with forward signals A = forward c.program S and backward signals B = backward c.program S. Let X_S and X_T be the inputs placed in S and in T, and Y_S and Y_T the outputs whose wires lie in S and in T (outputsIn); an output carried by an input wire is placed with that wire.

The rank-cut bound (blockRank_add_blockRank_le). If a circuit with values in a finite field F, with any gates, computes the linear map x ↦ M x, then for every split rank M[Y_T, X_S] + rank M[Y_S, X_T] ≤ |A| + |B|.

The proof uses the product fibres of SingleCut. The inputs with a fixed boundary key form a product L × R of left and right parts. On such a fibre the outputs carried in T depend only on the right part, so the left parts lie in a coset of the kernel of M[Y_T, X_S] and number at most |F| ^ (|X_S| - rank M[Y_T, X_S]); symmetrically for the right parts. Since there are at most |F| ^ (|A| + |B|) keys, |F| ^ n ≤ |F| ^ (|A| + |B|) |F| ^ (n - r₁ - r₂).

The counting step holds for every function and every finite value type (card_pow_le_of_fibres): if every left fibre (inputs varying only on X_S and keeping the outputs in Y_T) has at most DT elements and every right fibre at most DS, then |U| ^ n ≤ |U| ^ (|A| + |B|) · DT · DS.

The general fibre bound

theorem Algebraic.Cutwidth.MultiOutput.card_pow_inputsIn_le_of_leftFibre_of_trace {σ : Signature} {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] [Nonempty 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 : ℕ} (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 for a program. If the wires out of a program carry f and 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.card_pow_compl_inputsIn_le_of_rightFibre_of_trace {σ : Signature} {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] [Nonempty 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)) {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 for a program. 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.card_pow_le_of_fibres_of_trace {σ : 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 fibre bound for a program. If the wires out of a program carry f, every left fibre has at most DT elements and every right fibre at most DS, then |U| ^ n ≤ |U| ^ (|A| + |B|) · DT · DS.

theorem Algebraic.Cutwidth.MultiOutput.card_pow_inputsIn_le_of_leftFibre {σ : Signature} {n m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] [Nonempty U] {c : Circuit σ n m} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} (hc : c.Computes I f) (S : Finset (Wire n c.size)) {DT : ℕ} (hT : ∀ (x : Fin n → U), (leftFibre c.outputs f S x).card ≤ DT) : Fintype.card U ^ (SingleCut.inputsIn S).card ≤ Fintype.card U ^ (SingleCut.forward c.program S).card * DT

The forward fibre bound. If a circuit computes f and every left fibre of a split has at most DT elements, then |U| ^ |X_S| ≤ |U| ^ |A| · DT.

theorem Algebraic.Cutwidth.MultiOutput.card_pow_compl_inputsIn_le_of_rightFibre {σ : Signature} {n m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] [Nonempty U] {c : Circuit σ n m} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} (hc : c.Computes I f) (S : Finset (Wire n c.size)) {DS : ℕ} (hS : ∀ (x : Fin n → U), (rightFibre c.outputs f S x).card ≤ DS) : Fintype.card U ^ (SingleCut.inputsIn S)ᶜ.card ≤ Fintype.card U ^ (SingleCut.backward c.program S).card * DS

The backward fibre bound. Symmetrically, if every right fibre of a split has at most DS elements, then |U| ^ |X_T| ≤ |U| ^ |B| · DS.

theorem Algebraic.Cutwidth.MultiOutput.card_pow_le_of_fibres {σ : Signature} {n m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] {c : Circuit σ n m} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} (hc : c.Computes I f) (S : Finset (Wire n c.size)) {DT DS : ℕ} (hT : ∀ (x : Fin n → U), (leftFibre c.outputs f S x).card ≤ DT) (hS : ∀ (x : Fin n → U), (rightFibre c.outputs f S x).card ≤ DS) : Fintype.card U ^ n ≤ Fintype.card U ^ ((SingleCut.forward c.program S).card + (SingleCut.backward c.program S).card) * (DT * DS)

The fibre bound. If a circuit computes f, every left fibre of a split 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.card_leftFibre_le {n s m : ℕ} {F : Type u_1} [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 have at most |F| ^ (|X_S| - rank M[Y_T, X_S]) elements.

theorem Algebraic.Cutwidth.MultiOutput.card_rightFibre_le {n s m : ℕ} {F : Type u_1} [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 have at most |F| ^ (|X_T| - rank M[Y_S, X_T]) elements.

theorem Algebraic.Cutwidth.MultiOutput.blockRank_le_forward_of_trace {σ : Signature} {n s m : ℕ} {F : Type u_1} [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 of a program carry the linear map x ↦ M x, every split S has rank M[Y_T, X_S] ≤ |A|, where A = forward p S.

theorem Algebraic.Cutwidth.MultiOutput.blockRank_le_backward_of_trace {σ : Signature} {n s m : ℕ} {F : Type u_1} [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, every split S has rank M[Y_S, X_T] ≤ |B|, where B = backward p S.

theorem Algebraic.Cutwidth.MultiOutput.blockRank_add_blockRank_le_of_trace {σ : Signature} {n s m : ℕ} {F : Type u_1} [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 of a program carry the linear map x ↦ M x, every split S has rank M[Y_T, X_S] + rank M[Y_S, X_T] ≤ |A| + |B|.

theorem Algebraic.Cutwidth.MultiOutput.blockRank_le_forward {σ : Signature} {n m : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {c : Circuit σ n m} {I : Interpretation σ F} {M : Matrix (Fin m) (Fin n) F} (hc : c.Computes I fun (x : Fin n → F) => M.mulVec x) (S : Finset (Wire n c.size)) : blockRank M (outputsIn c.outputs S)ᶜ (SingleCut.inputsIn S) ≤ (SingleCut.forward c.program S).card

The forward rank-cut bound. If a circuit with values in a finite field, over any signature, computes the linear map x ↦ M x, then every set S of its wires has rank M[Y_T, X_S] ≤ |A|, where A = forward c.program S.

theorem Algebraic.Cutwidth.MultiOutput.blockRank_le_backward {σ : Signature} {n m : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {c : Circuit σ n m} {I : Interpretation σ F} {M : Matrix (Fin m) (Fin n) F} (hc : c.Computes I fun (x : Fin n → F) => M.mulVec x) (S : Finset (Wire n c.size)) : blockRank M (outputsIn c.outputs S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.backward c.program S).card

The backward rank-cut bound. Symmetrically, every set S of its wires has rank M[Y_S, X_T] ≤ |B|, where B = backward c.program S.

theorem Algebraic.Cutwidth.MultiOutput.blockRank_add_blockRank_le {σ : Signature} {n m : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {c : Circuit σ n m} {I : Interpretation σ F} {M : Matrix (Fin m) (Fin n) F} (hc : c.Computes I fun (x : Fin n → F) => M.mulVec x) (S : Finset (Wire n c.size)) : blockRank M (outputsIn c.outputs S)ᶜ (SingleCut.inputsIn S) + blockRank M (outputsIn c.outputs S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward c.program S).card + (SingleCut.backward c.program S).card

The rank-cut bound. If a circuit with values in a finite field, over any signature, computes the linear map x ↦ M x, then every set S of its wires has rank M[Y_T, X_S] + rank M[Y_S, X_T] ≤ |A| + |B|, where X_S and X_T are the inputs in S and outside S, Y_S and Y_T the outputs whose wires lie in S and outside S, and A and B the forward and backward signals of S.