The frontier lower bound for linear maps #
The frontier method applies to circuits with many outputs. For a circuit computing a linear map, 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 cut its graph
(Cslib.Circuits.Frontier.Compiler.graph) 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, splicing them
(Cslib.Circuits.Frontier.Compiler.eval_splice) 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ᶜ] and M[Yᶜ, X] are square and nonsingular,
so the values on the cut determine the input. Every layout passes through such a P, since
|X| + |Y| grows by at most one per vertex, from 0 to 2 N
(Cslib.Circuits.Frontier.Compiler.exists_injective_frontier), by a discrete intermediate value
theorem (Nat.exists_eq_of_forall_le_add_one).
How many values can a cut of k edges carry? A circuit has linear capacity
(Cslib.Circuits.Circuit.LinearCapacity) when the values of k wires never determine more than
k coordinates of the input. This holds
- over a finite alphabet, for every basis:
kwires take at most|F| ^ kvalues (Cslib.Circuits.Circuit.linearCapacity_of_finite); - over any field, for the affine basis: the values of
kwires are an affine function of the input (Cslib.Circuits.Circuit.linearCapacity_affine); - over an infinite field, for polynomial operations, after linearizing the circuit
(
Cslib.Circuits.Circuit.Computes.exists_affine).
It fails over infinite fields for arbitrary operations: an injection F × F → F lets one wire
carry two coordinates.
So every layout of the graph of the circuit has a frontier of at least N edges: the demand is
exactly N. For s inner gates of fan-in at most r the graph has cycle rank at most
(r - 1) s + 1 - N, and the comparison of demand and supply (eventually_lt_of_demand) gives
the coefficient of the frontier lower bound for decision problems.
Main theorem (eventually_lt_mul_innerSize_of_isTotallyRegular). 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 definitions #
Cslib.Circuits.Circuit.LinearCapacity: wires carry at most one coordinate each.
Main results #
Cslib.Circuits.Frontier.Compiler.exists_injective_frontier: some frontier of every layout determines the input.Cslib.Circuits.Frontier.exists_graph_of_isTotallyRegular: the reduction theorem for linear maps.Cslib.Circuits.Frontier.eventually_lt_mul_innerSize_of_isTotallyRegular: the lower bound, for circuits with linear capacity;..._finite,..._affineand..._isPolynomialspecialize it to finite fields with any basis, to any field with the affine basis, and to infinite fields with polynomial operations.
References #
Linear capacity #
A circuit has linear capacity under an interpretation when its wires carry at most one
symbol each: whenever the values of a set W of wires determine the input, n ≤ |W|.
Instances For
Over a finite alphabet every circuit has linear capacity: k wires take at most |U| ^ k
values.
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.
The graph of a circuit for a totally regular map #
Every output of a totally regular map depends on every input, so in the graph of a circuit computing it the vertex of every input is joined to every output vertex.
The graph of a circuit computing a totally regular map with at least one input is connected.
A circuit computing a totally regular map reads all of its inputs.
Some frontier of every layout determines the input. For a circuit computing a totally regular map, every layout of its graph has a time at which the values of the circuit on the frontier determine the input.
Every layout is wide. Every layout of the graph of a circuit with linear capacity
computing a totally regular map F^N → F^N has width at least N.
The lower bound #
The reduction theorem for linear maps. 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 width at least N.
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.
The frontier lower bound for linear maps over finite fields, for every basis. Under the
hypotheses of eventually_lt_mul_innerSize_of_isTotallyRegular, for every ε > 0 and all large
N, every circuit of fan-in at most r over a finite field F, over 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.
The frontier lower bound for linear maps over the affine basis, over every field.
The frontier lower bound for linear maps over infinite fields, for every basis of polynomial operations: their coefficients and degrees are arbitrary.