Proofs for totally regular linear maps

• Every block of a totally regular matrix has rank at least the smaller of its dimensions (min_card_le_blockRank): it contains a nonsingular square block of that size.
• A circuit computing a totally regular map has distinct output wires (outputs_injective): two outputs on one wire would give two equal rows, hence a singular 2 × 2 block.
• All inputs and outputs lie in one component of the wire graph: the component of an output is closed, so it is crossed by no signal, and the rank-cut bound forces every input and every output into it.
• Along the ranking of MultiOutput.exists_rank, the number of inputs and outputs in a prefix grows by at most two per wire, so some prefix ending at an input or output holds N or N + 1 of them. For that prefix the two blocks have ranks summing to at least N - 1, and the prefix is charged to the component holding all inputs, which gives N - 1 ≤ (A + η) (s - N)⁺ + 3 log₂ (N + 3 s) + C (sub_one_le_of_totallyRegular).
• For a rectangular m × N totally regular matrix with 2 ≤ N ≤ m, the m output wires are still distinct (outputs_injective_rect), so peeling the last gate and at most one output wire seated on it m - N times leaves a program with s - (m - N) gates computing an N × N totally regular row-submatrix (exists_square_of_totallyRegular_rect). This gives the rectangular finite bound N - 1 ≤ (A + η) (s - m)⁺ + 3 log₂ (N + 3 s) + C (sub_one_le_of_totallyRegular_rect) and the asymptotic lower bound m + (1 / A - ε) N < s (eventually_lt_size_of_orderingBound_rect).
• Cauchy matrices are totally regular (totallyRegular_cauchy): a kernel vector v of a square Cauchy matrix makes the interpolant through (y j, v j / w j), with w the barycentric weights, vanish at every x i; it has degree below the number of nodes, so it is zero, and then v = 0.

Blocks of totally regular matrices

theorem Algebraic.Cutwidth.MultiOutput.Internal.min_card_le_blockRank {F : Type u_1} [Field F] {m n : ℕ} {M : Matrix (Fin m) (Fin n) F} (hM : TotallyRegular M) (Y : Finset (Fin m)) (X : Finset (Fin n)) : min Y.card X.card ≤ blockRank M Y X

Every block of a totally regular matrix has rank at least the smaller of its dimensions.

theorem Algebraic.Cutwidth.MultiOutput.Internal.outputs_injective {σ : Signature} {F : Type u_1} [Field F] {n s N : ℕ} {M : Matrix (Fin N) (Fin N) F} (hM : TotallyRegular M) (p : Program σ n s) (I : Interpretation σ F) (out : Fin N → Wire n s) {f : (Fin n → F) → Fin N → F} (hf : ∀ (x : Fin n → F) (i : Fin N), p.trace I x (out i) = f x i) (hfM : ∀ (i i' : Fin N), (∀ (x : Fin n → F), f x i = f x i') → ∀ (j : Fin N), M i j = M i' j) : Function.Injective out

A circuit computing a totally regular square map carries distinct outputs on distinct wires.

theorem Algebraic.Cutwidth.MultiOutput.Internal.TotallyRegular.submatrix_rows {F : Type u_1} [Field F] {m m' n : ℕ} {M : Matrix (Fin m) (Fin n) F} (hM : TotallyRegular M) {r : Fin m' → Fin m} (hr : Function.Injective r) : TotallyRegular (M.submatrix r id)

Any injective selection of rows of a totally regular matrix is totally regular.

theorem Algebraic.Cutwidth.MultiOutput.Internal.outputs_injective_rect {σ : Signature} {F : Type u_1} [Field F] {m N s : ℕ} (hN : 2 ≤ N) {M : Matrix (Fin m) (Fin N) F} (hM : TotallyRegular M) (p : Program σ N s) (I : Interpretation σ F) (out : Fin m → Wire N s) (hf : ∀ (x : Fin N → F) (i : Fin m), p.trace I x (out i) = M.mulVec x i) : Function.Injective out

A circuit computing a totally regular map on N ≥ 2 inputs carries distinct outputs on distinct wires.

def Algebraic.Cutwidth.MultiOutput.Internal.unlast {n s : ℕ} (w : Wire n (s + 1)) (hw : w ≠ Wire.gate (Fin.last s)) : Wire n s

Every wire of p.gate line other than the last gate comes from p.

Equations

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

@[simp]

theorem Algebraic.Cutwidth.MultiOutput.Internal.castSucc_unlast {n s : ℕ} (w : Wire n (s + 1)) (hw : w ≠ Wire.gate (Fin.last s)) : (unlast w hw).castSucc = w

unlast inverts Wire.castSucc.

theorem Algebraic.Cutwidth.MultiOutput.Internal.trace_unlast {σ : Signature} {n s : ℕ} {U : Type u_2} (p : Program σ n s) (line : Line σ n s) (I : Interpretation σ U) (x : Fin n → U) (w : Wire n (s + 1)) (hw : w ≠ Wire.gate (Fin.last s)) : p.trace I x (unlast w hw) = (p.gate line).trace I x w

A wire of p.gate line other than the last gate carries the same value in p.

theorem Algebraic.Cutwidth.MultiOutput.Internal.exists_square_of_totallyRegular_rect {σ : Signature} {F : Type u_1} [Field F] {N m s : ℕ} (hN : 2 ≤ N) (hNm : N ≤ m) (p : Program σ N s) (hp : p.FanInAtMost 2) (I : Interpretation σ F) (out : Fin m → Wire N s) {M : Matrix (Fin m) (Fin N) F} (hM : TotallyRegular M) (hf : ∀ (x : Fin N → F) (i : Fin m), p.trace I x (out i) = M.mulVec x i) : ∃ (s' : ℕ) (p' : Program σ N s') (out' : Fin N → Wire N s') (M' : Matrix (Fin N) (Fin N) F), s' + (m - N) = s ∧ p'.FanInAtMost 2 ∧ TotallyRegular M' ∧ ∀ (x : Fin N → F) (i : Fin N), p'.trace I x (out' i) = M'.mulVec x i

Peeling m - N gates from a program computing a rectangular m × N totally regular map leaves a program with s - (m - N) gates computing an N × N totally regular submatrix.

A discrete intermediate value step

theorem Algebraic.Cutwidth.MultiOutput.Internal.exists_cross (g : ℕ → ℕ) (hzero : g 0 = 0) {h : ℕ} (hh : 1 ≤ h) (T : ℕ) (hT : h ≤ g T) : ∃ (t : ℕ), g t < h ∧ h ≤ g (t + 1)

A function from 0 that reaches h ≥ 1 crosses h at some step.

The finite bound

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_inputsIn_prefixBelow_succ_le {n s : ℕ} (rank : Wire n s → ℕ) (hrank : Function.Injective rank) (t : ℕ) : (SingleCut.inputsIn (prefixBelow rank (t + 1))).card ≤ (SingleCut.inputsIn (prefixBelow rank t)).card + 1

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_outputsIn_prefixBelow_succ_le {n s m : ℕ} (rank : Wire n s → ℕ) (hrank : Function.Injective rank) (out : Fin m → Wire n s) (hout : Function.Injective out) (t : ℕ) : (outputsIn out (prefixBelow rank (t + 1))).card ≤ (outputsIn out (prefixBelow rank t)).card + 1

theorem Algebraic.Cutwidth.MultiOutput.Internal.sub_one_le_of_rank_cuts {σ : Signature} {F : Type u_1} [Field F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {N s : ℕ} (p : Program σ N s) (hp : p.FanInAtMost 2) (out : Fin N → Wire N s) {M : Matrix (Fin N) (Fin N) F} (hM : TotallyRegular M) (hout : Function.Injective out) (cuts : ∀ (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) : ↑N - 1 ≤ (A + η) * max (↑s - ↑N) 0 + 3 * Real.logb 2 (↑N + 3 * ↑s) + C

The layout bound needs only distinct output wires and the rank inequality at each cut. No finiteness assumption on the coefficient field enters this graph argument.

theorem Algebraic.Cutwidth.MultiOutput.Internal.sub_one_le_of_totallyRegular {σ : Signature} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {N s : ℕ} (p : Program σ N s) (hp : p.FanInAtMost 2) (I : Interpretation σ F) (out : Fin N → Wire N s) {M : Matrix (Fin N) (Fin N) F} (hM : TotallyRegular M) (hf : ∀ (x : Fin N → F) (i : Fin N), p.trace I x (out i) = M.mulVec x i) : ↑N - 1 ≤ (A + η) * max (↑s - ↑N) 0 + 3 * Real.logb 2 (↑N + 3 * ↑s) + C

The finite bound for totally regular maps. A fan-in-two program over any signature whose wires out carry a totally regular linear map on N inputs has N - 1 ≤ (A + η) (s - N)⁺ + 3 log₂ (N + 3 s) + C.

theorem Algebraic.Cutwidth.MultiOutput.Internal.sub_one_le_of_totallyRegular_rect {σ : Signature} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {N m s : ℕ} (hNm : N ≤ m) (p : Program σ N s) (hp : p.FanInAtMost 2) (I : Interpretation σ F) (out : Fin m → Wire N s) {M : Matrix (Fin m) (Fin N) F} (hM : TotallyRegular M) (hf : ∀ (x : Fin N → F) (i : Fin m), p.trace I x (out i) = M.mulVec x i) : ↑N - 1 ≤ (A + η) * max (↑s - ↑m) 0 + 3 * Real.logb 2 (↑N + 3 * ↑s) + C

The finite bound for rectangular totally regular maps. A fan-in-two program over any signature whose wires out carry an m × N totally regular linear map with N ≤ m has N - 1 ≤ (A + η) (s - m)⁺ + 3 log₂ (N + 3 s) + C.

Asymptotics

theorem Algebraic.Cutwidth.MultiOutput.Internal.eventually_lt_size_of_rank_cuts {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (M : Matrix (Fin N) (Fin N) F), TotallyRegular M → ∀ (σ : Signature) (c : Circuit σ N N), c.FanInAtMost 2 → Function.Injective c.outputs → (∀ (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) → (1 + 1 / A - ε) * ↑N < ↑c.size

The asymptotic layout transfer is uniform over all fields satisfying the rank-cut bound.

theorem Algebraic.Cutwidth.MultiOutput.Internal.eventually_lt_size_of_orderingBound {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Fintype F] [DecidableEq F] (M : Matrix (Fin N) (Fin N) F), TotallyRegular M → ∀ (σ : Signature) (I : Interpretation σ F) (c : Circuit σ N N), c.FanInAtMost 2 → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → (1 + 1 / A - ε) * ↑N < ↑c.size

The asymptotic bound for totally regular maps with a general ordering coefficient.

theorem Algebraic.Cutwidth.MultiOutput.Internal.eventually_lt_size_of_orderingBound_rect {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ {m : ℕ}, N ≤ m → ∀ (F : Type u) [inst : Field F] [Fintype F] [DecidableEq F] (M : Matrix (Fin m) (Fin N) F), TotallyRegular M → ∀ (σ : Signature) (I : Interpretation σ F) (c : Circuit σ N m), c.FanInAtMost 2 → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → ↑m + (1 / A - ε) * ↑N < ↑c.size

The asymptotic bound for rectangular totally regular maps with a general ordering coefficient.

Cauchy matrices

theorem Algebraic.Cutwidth.MultiOutput.Internal.det_cauchy_ne_zero {F : Type u_1} [Field F] {k : ℕ} (x y : Fin k → F) (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i j : Fin k), x i ≠ y j) : (cauchy x y).det ≠ 0

Square Cauchy matrices are nonsingular.

theorem Algebraic.Cutwidth.MultiOutput.Internal.totallyRegular_cauchy {F : Type u_1} [Field F] {m n : ℕ} (x : Fin m → F) (y : Fin n → F) (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i : Fin m) (j : Fin n), x i ≠ y j) : TotallyRegular (cauchy x y)

Cauchy matrices are totally regular: with distinct nodes x i, distinct nodes y j and x i ≠ y j, every square submatrix is again a nonsingular Cauchy matrix.

theorem Algebraic.Cutwidth.MultiOutput.Internal.totallyRegular_cauchyZMod (q N : ℕ) [Fact (Nat.Prime q)] (hq : 2 * N ≤ q) : TotallyRegular (cauchyZMod q N)

The explicit Cauchy family is totally regular over ZMod q for a prime q ≥ 2 N.