From small circuits to wide graphs

This file combines the three ingredients of the frontier method for a single input length:

• compiling a circuit into a constraint network (Frontier.Compiler),
• the frontier counting lemma for networks (Frontier.Network.ncard_accepted_le), and
• the support lemma for rectangle-free sets (Frontier.RectangleFree.pow_ncard_compl_lt).

The reduction theorem (Frontier.exists_graph_of_decides). Let c be a circuit with s inner gates (gates of positive arity; constants are free) of fan-in at most r ≥ 2, over any basis on a finite alphabet U with q ≥ 2 symbols, that decides a K-rectangle-free set S ⊆ U^n with |S| ≥ q K^2. Then there is a connected, loopless multigraph G of maximum degree r + 1 with at most 2 r s + 3 vertices and cycle rank

β₁(G) ≤ (r - 1) s - n + log_q K + 1,

every layout of which has width at least

log_q |S| - 3 log_q K - log_q (|V(G)| + 1) - (r + 2).

For fan-in two the graph is subcubic, β₁(G) ≤ s - n + log_q K + 1, and the width is at least log_q |S| - 3 log_q K - log_q (|V(G)| + 1) - 4.

The graph is the constraint graph of c. The cycle rank bound is the count of the compiler, together with the support lemma, which says that c reads all but log_q K of its inputs. The width bound is the frontier counting lemma, in which the unread inputs contribute at most K transitions, again by the support lemma.

For a dense set, log_q |S| ≈ n; so a small circuit gives a graph whose cycle rank is about (r - 1) s - n but whose layouts all have width about n.

def Complexity.Frontier.Decides {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} (c : Cslib.Circuits.Circuit σ n 1) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (S : Set (Fin n → U)) : Prop

A circuit with one output decides a set of inputs S, accepting the values in Acc, when an input lies in S exactly if the output of the circuit lies in Acc.

Equations

• Complexity.Frontier.Decides c I Acc S = ∀ (x : Fin n → U), x ∈ S ↔ c.eval I x 0 ∈ Acc

theorem Complexity.Frontier.Decides.of_computes {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ Bool} {f : (Fin n → Bool) → Bool} (h : c.Computes I (Cslib.Circuits.single f)) : Decides c I {true} {x : Fin n → Bool | f x = true}

A circuit computing a Boolean function decides the set of inputs it maps to true.

theorem Complexity.Frontier.RectangleFree.pos {U : Type u_1} {ι : Type u_2} {S : Set (ι → U)} {K : ℕ} (h : RectangleFree S K) : 0 < K

A rectangle-free set has a positive threshold.

@[reducible, inline]

noncomputable abbrev Complexity.Frontier.constraintNetwork {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1) : Network U (Fin n) (Compiler.Vertex c.program c.outputs) (Compiler.Edge c.program c.outputs)

The constraint network of a one-output circuit.

Equations

• Complexity.Frontier.constraintNetwork I Acc c = Complexity.Frontier.Compiler.network c.program c.outputs I fun (x : Fin 1) => Acc

theorem Complexity.Frontier.accepted_constraintNetwork {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {I : Cslib.Circuits.Interpretation σ U} {Acc : Set U} {c : Cslib.Circuits.Circuit σ n 1} {S : Set (Fin n → U)} (hS : Decides c I Acc S) : (constraintNetwork I Acc c).accepted = S

theorem Complexity.Frontier.Network.logb_ncard_accepted_le {U : Type u_1} {n : ℕ} {V : Type u_2} {E : Type u_3} [Finite E] [Finite U] [Nontrivial U] (N : Network U (Fin n) V E) {K d m w : ℕ} (hfree : RectangleFree N.accepted K) (hbig : Nat.card U * K ^ 2 ≤ N.accepted.ncard) (π : Layout V) (hw : ∀ (t : ℕ), (N.cut (π.initial t)).ncard ≤ w) (hd : N.MaxDegreeLE d) (hm : ∀ (v : V), (N.readAt v).ncard ≤ m) : Real.logb ↑(Nat.card U) ↑N.accepted.ncard ≤ ↑w + (↑d + ↑m) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card V) + 1)

Frontier demand for any network. Rectangle-freeness pays for unread inputs; no uniqueness of satisfying assignments is needed.

theorem Complexity.Frontier.pow_ncard_unread_lt {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} [Finite U] [Nontrivial U] {I : Cslib.Circuits.Interpretation σ U} {Acc : Set U} {c : Cslib.Circuits.Circuit σ n 1} {S : Set (Fin n → U)} {K : ℕ} (hS : Decides c I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) : Nat.card U ^ (constraintNetwork I Acc c).readᶜ.ncard < K

The support lemma, for circuits. A circuit deciding a large rectangle-free set reads all but fewer than log_q K of its inputs.

theorem Complexity.Frontier.cycleRank_le {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} [Finite U] [Nontrivial U] {I : Cslib.Circuits.Interpretation σ U} {Acc : Set U} {c : Cslib.Circuits.Circuit σ n 1} {S : Set (Fin n → U)} {K r : ℕ} (hfan : c.FanInAtMost r) (hS : Decides c I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) : ↑(constraintNetwork I Acc c).cycleRank ≤ ↑((r - 1) * c.innerSize) - ↑n + Real.logb ↑(Nat.card U) ↑K + 1

The cycle rank of the constraint graph is at most (r - 1) s - n + log_q K + 1 for fan-in at most r, where s counts the inner gates.

theorem Complexity.Frontier.logb_ncard_le {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} [Finite U] [Nontrivial U] {I : Cslib.Circuits.Interpretation σ U} {Acc : Set U} {c : Cslib.Circuits.Circuit σ n 1} {S : Set (Fin n → U)} {K r : ℕ} (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hS : Decides c I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) (π : Layout (Compiler.Vertex c.program c.outputs)) {w : ℕ} (hw : ∀ (t : ℕ), ((constraintNetwork I Acc c).cut (π.initial t)).ncard ≤ w) : Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑w + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card (Compiler.Vertex c.program c.outputs)) + 1)

Every layout of the constraint graph is wide. For fan-in at most r ≥ 2, if all frontiers of a layout have at most w edges, then log_q |S| ≤ w + (r + 2) + 3 log_q K + log_q (|V| + 1).

theorem Complexity.Frontier.exists_graph_of_decides {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} [Finite U] [Nontrivial U] {I : Cslib.Circuits.Interpretation σ U} {Acc : Set U} {c : Cslib.Circuits.Circuit σ n 1} {S : Set (Fin n → U)} {K r : ℕ} (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hS : Decides c I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) : ∃ (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 ∧ ↑G.cycleRank ≤ ↑((r - 1) * c.innerSize) - ↑n + Real.logb ↑(Nat.card U) ↑K + 1 ∧ ∀ (π : Layout V) (w : ℕ), (∀ (t : ℕ), (G.cut (π.initial t)).ncard ≤ w) → Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑w + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card V) + 1)

The reduction theorem. A circuit with s inner gates of fan-in at most r ≥ 2, over any basis on U, deciding a K-rectangle-free set S ⊆ U^n with |S| ≥ q K^2, yields a connected, loopless multigraph of maximum degree r + 1 with at most 2 r s + 3 vertices and cycle rank at most (r - 1) s - n + log_q K + 1, every layout of which has width at least log_q |S| - 3 log_q K - log_q (|V| + 1) - (r + 2).