Totally regular linear realizations over arbitrary fields

A local linear realization on the original circuit wires supplies the rank bound at every cut. The graph layout then gives the same gate lower bound over finite and infinite fields. There is no restriction on the coefficients of the local linear combinations, and no extra gate is charged for forming the certificate.

theorem Algebraic.Cutwidth.MultiOutput.Linear.Realization.sub_one_le_of_totallyRegular {σ : Signature} {F : Type u_1} [Field F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {n s : ℕ} {p : Program σ n s} (r : Realization p F) (fan : p.FanInAtMost 2) (out : Fin n → Wire n s) {M : Matrix (Fin n) (Fin n) F} (regular : TotallyRegular M) (rows : ∀ (i : Fin n), r.value (out i) = M i) : ↑n - 1 ≤ (A + η) * max (↑s - ↑n) 0 + 3 * Real.logb 2 (↑n + 3 * ↑s) + C

The finite layout bound for a local linear realization of a totally regular map.

theorem Algebraic.Cutwidth.MultiOutput.Linear.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] (M : Matrix (Fin n) (Fin n) F), TotallyRegular M → ∀ (σ : Signature) (c : Circuit σ n n), c.FanInAtMost 2 → ∀ (r : Realization c.program F), (∀ (i : Fin n), r.value (c.outputs i) = M i) → (1 + 1 / A - ε) * ↑n < ↑c.size

The asymptotic transfer is uniform over fields, signatures, and local coefficients.

theorem Algebraic.Cutwidth.MultiOutput.Linear.eventually_lt_size_gaussian {ε : ℝ} (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 → ∀ (r : Realization c.program F), (∀ (i : Fin n), r.value (c.outputs i) = M i) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

The Gaussian coefficient for totally regular linear realizations over any field.