Lower bounds for linear maps

The frontier method applies to circuits with many outputs. Here the demand comes from linear algebra instead of from counting rectangles.

Let a circuit over a field F compute x ↦ M x for an N × N matrix M, and compile it into a network that accepts every value at every output. Cut the network along a set P of vertices: P reads the inputs X and holds the outputs Y. If the runs on two inputs agree on the cut, then splicing them (Frontier.Compiler.trace_out_of_cut) shows that the outputs in Y do not see the inputs outside X, and the outputs outside Y do not see the inputs in X. When M is totally regular and |X| + |Y| = N, both blocks M[Y, X^c] and M[Y^c, X] are square and nonsingular, so the input is determined by the values on the cut (Frontier.exists_injective_cut). Every layout passes through such a P, since |X| + |Y| grows by at most one per vertex, from 0 to 2 N.

How many values can a cut of k edges carry? A circuit has linear capacity (Frontier.LinearCapacity) when k wires never determine more than k coordinates of the input. This holds

• over a finite field, for every basis: k wires take at most |F| ^ k values (Frontier.linearCapacity_of_finite);
• over any field, for the affine basis: the values of k wires are an affine function of the input (Frontier.linearCapacity_affine);
• over an infinite field, for polynomial operations, after linearizing the circuit (Frontier.exists_affine_circuit).

It fails over infinite fields for arbitrary operations: a bijection F × F → F lets one wire carry everything.

So every layout of the graph of the circuit has a frontier of at least N edges: the demand is exactly N. The graph has cycle rank at most (r - 1) s + 1 - N for s inner gates of fan-in r, and the comparison of demand and supply gives the same coefficient as for decision problems.

Main theorem (Frontier.lowerBound_linear). Under LayoutBound (r + 1) A, for every ε > 0 and all large N, every circuit of fan-in at most r with linear capacity computing a totally regular map F^N → F^N has s inner gates with (r - 1) s > (1 + 1/A - ε) N, uniformly in the field. Constants are free.

Main results

• Frontier.exists_injective_cut: some frontier of every layout determines the input.
• Frontier.lowerBound_linear: the lower bound, for circuits with linear capacity.
• Frontier.lowerBound_linear_finite, Frontier.lowerBound_linear_affine, Frontier.lowerBound_linear_polynomial: over finite fields with any basis, over any field with the affine basis, and over infinite fields with polynomial operations.

Linear capacity

def Complexity.Frontier.LinearCapacity {F : Type u} {σ : Cslib.Circuits.Signature} {N m : ℕ} (I : Cslib.Circuits.Interpretation σ F) (c : Cslib.Circuits.Circuit σ N m) : Prop

A circuit has linear capacity when its wires carry at most one element of the field each: whenever the values of k wires determine the input, N ≤ k.

Equations

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

theorem Complexity.Frontier.linearCapacity_of_finite {F : Type u} [Field F] {σ : Cslib.Circuits.Signature} {N m : ℕ} [Finite F] (I : Cslib.Circuits.Interpretation σ F) (c : Cslib.Circuits.Circuit σ N m) : LinearCapacity I c

Over a finite field every circuit has linear capacity: k wires take at most |F| ^ k values.

theorem Complexity.Frontier.linearCapacity_affine {F : Type u} [Field F] {N m : ℕ} (c : Cslib.Circuits.Circuit (affineSignature F) N m) : LinearCapacity (affineInterpretation F) c

Circuits over the affine basis have linear capacity: the values of k wires are an affine function of the input, which is injective only if N ≤ k.

Every layout has a frontier that determines the input

theorem Complexity.Frontier.exists_eq_of_le_succ {a : ℕ → ℕ} (h0 : a 0 = 0) {m T : ℕ} : m ≤ a T → (∀ t < T, a (t + 1) ≤ a t + 1) → ∃ t ≤ T, a t = m

A discrete intermediate value theorem. A sequence of naturals that starts at 0 and grows by at most one per step takes every value up to its final one.

@[reducible, inline]

noncomputable abbrev Complexity.Frontier.functionNetwork {F : Type u} {σ : Cslib.Circuits.Signature} {N : ℕ} (I : Cslib.Circuits.Interpretation σ F) (c : Cslib.Circuits.Circuit σ N N) : Network F (Fin N) (Compiler.Vertex c.program c.outputs) (Compiler.Edge c.program c.outputs)

The network of a circuit computing a function: every value is accepted at every output.

Equations

• Complexity.Frontier.functionNetwork I c = Complexity.Frontier.Compiler.network c.program c.outputs I fun (x : Fin N) => Set.univ

theorem Complexity.Frontier.trace_outputs {F : Type u} [Field F] {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ F} {N : ℕ} {M : Matrix (Fin N) (Fin N) F} {c : Cslib.Circuits.Circuit σ N N} (hc : c.Computes I fun (x : Fin N → F) => M.mulVec x) (x : Fin N → F) (o : Fin N) : c.program.trace I x (c.outputs o) = M.mulVec x o

theorem Complexity.Frontier.upstream_of_totallyRegular {F : Type u} [Field F] {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ F} {N : ℕ} {M : Matrix (Fin N) (Fin N) F} {c : Cslib.Circuits.Circuit σ N N} (hM : TotallyRegular M) (hc : c.Computes I fun (x : Fin N → F) => M.mulVec x) (o i : Fin N) : c.program.Upstream (c.outputs o) (Cslib.Circuits.Wire.input i)

Every output of a totally regular map depends on every input, so every input is upstream of every output.

theorem Complexity.Frontier.mem_readIn_functionNetwork {F : Type u} [Field F] {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ F} {N : ℕ} {M : Matrix (Fin N) (Fin N) F} {c : Cslib.Circuits.Circuit σ N N} (hM : TotallyRegular M) (hc : c.Computes I fun (x : Fin N → F) => M.mulVec x) (P : Set (Compiler.Vertex c.program c.outputs)) (i : Fin N) : i ∈ (functionNetwork I c).readIn P ↔ Compiler.Vertex.signal ⟨Cslib.Circuits.Wire.input i, ⋯⟩ ∈ P

In the network of a circuit for a totally regular map, an input is read in P exactly when its vertex lies in P.

theorem Complexity.Frontier.exists_injective_cut {F : Type u} [Field F] {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ F} {N : ℕ} {M : Matrix (Fin N) (Fin N) F} {c : Cslib.Circuits.Circuit σ N N} (hM : TotallyRegular M) (hc : c.Computes I fun (x : Fin N → F) => M.mulVec x) (π : Layout (Compiler.Vertex c.program c.outputs)) : ∃ (t : ℕ), Function.Injective fun (x : Fin N → F) (e : ↑((functionNetwork I c).cut (π.initial t))) => c.program.trace I x ↑(↑e).signal

Some frontier of every layout determines the input. For a circuit computing a totally regular map, every layout of its network has a time at which the values on the frontier determine the input.

theorem Complexity.Frontier.exists_graph_of_totallyRegular {F : Type u} [Field F] {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ F} {N : ℕ} {M : Matrix (Fin N) (Fin N) F} {c : Cslib.Circuits.Circuit σ N N} (hN : 1 ≤ N) {r : ℕ} (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hM : TotallyRegular M) (hc : c.Computes I fun (x : Fin N → F) => M.mulVec x) (hcap : LinearCapacity I c) : ∃ (V : Type) (E : Type) (_ : Finite V) (_ : Finite E) (G : Multigraph V E), G.Connected ∧ G.Loopless ∧ G.MaxDegreeLE (r + 1) ∧ Nat.card V ≤ 2 * r * c.innerSize + 3 * N ∧ G.cycleRank + N ≤ (r - 1) * c.innerSize + 1 ∧ ∀ (π : Layout V), ∃ (t : ℕ), N ≤ (G.cut (π.initial t)).ncard

The graph of a circuit for a totally regular map. A circuit with s inner gates of fan-in at most r ≥ 2 and linear capacity, computing a totally regular map F^N → F^N with N ≥ 1, yields a connected, loopless multigraph of maximum degree r + 1 with at most 2 r s + 3 N vertices and cycle rank at most (r - 1) s + 1 - N, every layout of which has a frontier of at least N edges.

The lower bound

theorem Complexity.Frontier.lowerBound_linear {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ F) (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit σ N N), TotallyRegular M → c.FanInAtMost r → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → LinearCapacity I c → (1 + 1 / A - ε) * ↑N < (↑r - 1) * ↑c.innerSize

The frontier lower bound for linear maps. Let r ≥ 2 and assume the layout hypothesis for maximum degree r + 1 with coefficient A > 0. For every ε > 0 and all large N, every circuit of fan-in at most r with linear capacity, over any field and any basis, that computes x ↦ M x for a totally regular N × N matrix M, has s inner gates with (r - 1) s > (1 + 1/A - ε) N.

theorem Complexity.Frontier.lowerBound_linear_finite {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Finite F] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ F) (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit σ N N), TotallyRegular M → c.FanInAtMost r → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → (1 + 1 / A - ε) * ↑N < (↑r - 1) * ↑c.innerSize

Linear maps over finite fields, over any basis.

theorem Complexity.Frontier.lowerBound_linear_affine {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit (affineSignature F) N N), TotallyRegular M → c.FanInAtMost r → (c.Computes (affineInterpretation F) fun (x : Fin N → F) => M.mulVec x) → (1 + 1 / A - ε) * ↑N < (↑r - 1) * ↑c.innerSize

Linear maps over any field, over the affine basis.

theorem Complexity.Frontier.lowerBound_linear_polynomial {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Infinite F] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ F), IsPolynomial I → ∀ (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit σ N N), TotallyRegular M → c.FanInAtMost r → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → (1 + 1 / A - ε) * ↑N < (↑r - 1) * ↑c.innerSize

Linear maps over infinite fields, over any basis of polynomial operations: the coefficients and degrees of the operations are arbitrary.