Multi-output cuts: definitions

The single-cut infrastructure (SingleCut) splits the wires of a straight-line program into a set S and its complement and counts the forward and backward signals crossing the split. This file collects the notions used to apply it to programs with several outputs.

• Linked p u v: one of the wires u, v is a gate reading the other. These are the edges of the undirected wire graph.
• component p w: the wires joined to w by a path of linked wires.
• gatesIn S: the gates whose wires lie in S (the inputs are SingleCut.inputsIn S).
• prefixUpTo rank w and prefixBelow rank t: the prefixes of a ranking of the wires.
• outputsIn out S: the output indices whose wires lie in S.
• leftFibre out f S x and rightFibre out f S x: the inputs that differ from x only on the coordinates placed in S (respectively outside S) and keep every output carried outside S (respectively in S).
• blockRank M Y X: the rank of the block of a matrix with rows Y and columns X.
• TotallyRegular M: every square submatrix of M is nonsingular.
• cauchy x y: the Cauchy matrix (1 / (x i - y j)), and cauchyZMod q N, its instance over ZMod q with nodes x i = i and y j = N + j.

The wire graph

def Algebraic.Cutwidth.MultiOutput.Linked {σ : Signature} {n s : ℕ} (p : Program σ n s) (u v : Wire n s) : Prop

Two wires are linked when one of them is a gate reading the other.

Equations

• Algebraic.Cutwidth.MultiOutput.Linked p u v = ((∃ (g : Fin s), u = Cslib.Circuits.Wire.gate g ∧ p.Reads g v) ∨ ∃ (g : Fin s), v = Cslib.Circuits.Wire.gate g ∧ p.Reads g u)

noncomputable def Algebraic.Cutwidth.MultiOutput.component {σ : Signature} {n s : ℕ} (p : Program σ n s) (w : Wire n s) : Finset (Wire n s)

The connected component of a wire in the wire graph: the wires joined to it by a path of linked wires.

Equations

• Algebraic.Cutwidth.MultiOutput.component p w = {v : Cslib.Circuits.Wire n s | Relation.ReflTransGen (Algebraic.Cutwidth.MultiOutput.Linked p) w v}

def Algebraic.Cutwidth.MultiOutput.gatesIn {n s : ℕ} (S : Finset (Wire n s)) : Finset (Fin s)

The gates whose wires lie in S.

Equations

• Algebraic.Cutwidth.MultiOutput.gatesIn S = {g : Fin s | Cslib.Circuits.Wire.gate g ∈ S}

Prefixes of a ranking

def Algebraic.Cutwidth.MultiOutput.prefixUpTo {n s : ℕ} (rank : Wire n s → ℕ) (w : Wire n s) : Finset (Wire n s)

The wires ranked at most as high as w.

Equations

• Algebraic.Cutwidth.MultiOutput.prefixUpTo rank w = {v : Cslib.Circuits.Wire n s | rank v ≤ rank w}

def Algebraic.Cutwidth.MultiOutput.prefixBelow {n s : ℕ} (rank : Wire n s → ℕ) (t : ℕ) : Finset (Wire n s)

The wires ranked below t.

Equations

• Algebraic.Cutwidth.MultiOutput.prefixBelow rank t = {v : Cslib.Circuits.Wire n s | rank v < t}

Outputs and fibres

def Algebraic.Cutwidth.MultiOutput.outputsIn {n s m : ℕ} (out : Fin m → Wire n s) (S : Finset (Wire n s)) : Finset (Fin m)

The output indices whose wires lie in S.

Equations

• Algebraic.Cutwidth.MultiOutput.outputsIn out S = {i : Fin m | out i ∈ S}

def Algebraic.Cutwidth.MultiOutput.leftFibre {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (out : Fin m → Wire n s) (f : (Fin n → U) → Fin m → U) (S : Finset (Wire n s)) (x : Fin n → U) : Finset (Fin n → U)

The inputs that agree with x on every coordinate placed outside S and on which f takes the values it takes at x on every output whose wire lies outside S.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.MultiOutput.rightFibre {n s m : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (out : Fin m → Wire n s) (f : (Fin n → U) → Fin m → U) (S : Finset (Wire n s)) (x : Fin n → U) : Finset (Fin n → U)

The inputs that agree with x on every coordinate placed in S and on which f takes the values it takes at x on every output whose wire lies in S.

Equations

• One or more equations did not get rendered due to their size.

Matrices

noncomputable def Algebraic.Cutwidth.MultiOutput.blockRank {n m : ℕ} {F : Type u_1} [Field F] (M : Matrix (Fin m) (Fin n) F) (Y : Finset (Fin m)) (X : Finset (Fin n)) : ℕ

The rank of the block of M with rows in Y and columns in X.

Equations

• Algebraic.Cutwidth.MultiOutput.blockRank M Y X = (M.submatrix (fun (i : ↥Y) => ↑i) fun (j : ↥X) => ↑j).rank

def Algebraic.Cutwidth.MultiOutput.TotallyRegular {n m : ℕ} {F : Type u_1} [Field F] (M : Matrix (Fin m) (Fin n) F) : Prop

A matrix is totally regular when every square submatrix is nonsingular: for every k and all injective choices of k rows and k columns, the determinant is nonzero.

Equations

• Algebraic.Cutwidth.MultiOutput.TotallyRegular M = ∀ (k : ℕ) (r : Fin k → Fin m) (c : Fin k → Fin n), Function.Injective r → Function.Injective c → (M.submatrix r c).det ≠ 0

def Algebraic.Cutwidth.MultiOutput.cauchy {n m : ℕ} {F : Type u_1} [Field F] (x : Fin m → F) (y : Fin n → F) : Matrix (Fin m) (Fin n) F

The Cauchy matrix with entries 1 / (x i - y j).

Equations

• Algebraic.Cutwidth.MultiOutput.cauchy x y = Matrix.of fun (i : Fin m) (j : Fin n) => (x i - y j)⁻¹

def Algebraic.Cutwidth.MultiOutput.cauchyZMod (q N : ℕ) : Matrix (Fin N) (Fin N) (ZMod q)

The N × N Cauchy matrix over ZMod q with nodes x i = i and y j = N + j. For a prime q ≥ 2 N the nodes are distinct, so it is totally regular.

Equations

• Algebraic.Cutwidth.MultiOutput.cauchyZMod q N = Matrix.of fun (i j : Fin N) => (↑↑i - ↑(N + ↑j))⁻¹