The lower bound with a ledger

Main theorem (Frontier.lowerBound_ledger). Fix r ≥ 2 and assume the layout hypothesis LayoutBound (r + 1) A. Let S_n ⊆ U^n be dense K_n-rectangle-free sets with log K_n = o(n), as in Frontier.lowerBound, and let β(n) = o(n). For every ε > 0 and all large n, every circuit deciding S_n whose gates have fan-in at most r, except for special gates of any fan-in that have a ledger in a monoid M with log |M| ≤ β(n), has (r - 1) s > (1 + 1/A - ε) n for its number s of ordinary inner gates. Constants and special gates are free; the ledger contributes only to the sublinear error.

So the coefficient of the frontier method survives a sublinear amount of unbounded fan-in. For instance, k gates computing AND, OR, parity, or counts modulo a fixed m of any number of arguments have a ledger with log |M| = O(k) (Frontier.exists_ledger_of_aggregates), so k = o(n) such gates are allowed.

Proof. Erase the special gates and lay out the network of the erased program, one connected component after another (Frontier.LayoutBound.exists_layout_componentwise). Sweep the circuit along this layout with the ledger in the messages (Frontier.Ledger.sweep). At each step the transitions are bounded both by the width of the frontier and by the number of inputs of the component being processed. The frontier counting lemma then finds a component W that reads almost all n inputs and whose layout is wide, up to 2 log |M| and the usual error terms (Frontier.Ledger.exists_ncard_le). The cycle rank of W is at most (r - 1) s + 1 minus the number of inputs it reads (Frontier.Compiler.cycleRankOn_add_ncard_readIn_le), so W alone has the demand and the supply of a connected graph, and the comparison of demand and supply finishes the proof.

theorem Complexity.Frontier.Ledger.card_vtx_pos {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {special : ℕ → Prop} : 0 < Nat.card (Vtx c special)

The erased program has an output vertex, so its network has a vertex.

theorem Complexity.Frontier.Ledger.card_live_le {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {special : ℕ → Prop} : Nat.card { w : Cslib.Circuits.Wire n c.size // Live c special w } ≤ n + (erase special c.program).innerGates.card

The live wires are the inputs and the inner gates of the erased program.

theorem Complexity.Frontier.Ledger.card_innerGates_erase_le {σ : Cslib.Circuits.Signature} {n : ℕ} {special : ℕ → Prop} {s : ℕ} (p : Cslib.Circuits.Program σ n s) : (erase special p).innerGates.card ≤ p.innerGates.card

Erasing the special gates leaves only inner gates of the circuit as inner gates.

theorem Complexity.Frontier.Ledger.exists_ncard_le {U : Type u} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_1} [CommMonoid M] (L : Ledger c.program I special M) [Finite U] [Nonempty U] [Finite M] {Acc : Set U} {K : ℕ} (hfree : RectangleFree {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc} K) (hK : K ≤ {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc}.ncard) (π : Layout (Vtx c special)) (W : (t : ℕ) → t < Nat.card (Vtx c special) → Set (Vtx c special)) (hW : ∀ (t : ℕ) (ht : t < Nat.card (Vtx c special)), (L.fnet 1).cut (W t ht) = ∅) (hv : ∀ (t : ℕ) (ht : t < Nat.card (Vtx c special)), (Equiv.symm π) ⟨t, ht⟩ ∈ W t ht) (hC : ∀ (t : ℕ) (ht : t < Nat.card (Vtx c special)), (L.fnet 1).frontier π t ∪ (L.fnet 1).frontier π (t + 1) ⊆ (L.fnet 1).touching (W t ht)) : ∃ (t : ℕ) (ht : t < Nat.card (Vtx c special)), {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc}.ncard ≤ (K - 1) ^ 2 * (Nat.card (Vtx c special) + 1) * Nat.card M ^ 3 * Nat.card U ^ min (((L.fnet 1).frontier π t ∪ (L.fnet 1).frontier π (t + 1)).ncard + ((L.fnet 1).readAt ((Equiv.symm π) ⟨t, ht⟩)).ncard) ((L.fnet 1).readIn (W t ht)).ncard

Counting along a componentwise layout. If the vertex processed at each step lies in a closed set containing both frontiers of the step, then some step t bounds the size of the set decided by the circuit by (K - 1)^2 (|V| + 1) |M|^3 q^m, where m is the smaller of the width of the step and the number of inputs read in its closed set.

theorem Complexity.Frontier.lowerBound_ledger {U : Type u} [Finite U] [Nontrivial U] {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (S : (n : ℕ) → Set (Fin n → U)) (K : ℕ → ℕ) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {β : ℕ → ℝ} (hβ : β =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) (M : Type) [inst : CommMonoid M] [Finite M], (∀ (g : Fin c.size), ¬special ↑g → σ.Arity (c.program.lines g).op ≤ r) → ∀ (a : Ledger c.program I special M), Real.log ↑(Nat.card M) ≤ β n → Decides c I Acc (S n) → (1 + 1 / A - ε) * ↑n < (↑r - 1) * ↑(erase special c.program).innerGates.card

The frontier lower bound with a ledger. Let r ≥ 2 and assume the layout hypothesis for maximum degree r + 1 with coefficient A > 0. Let S_n ⊆ U^n be dense K_n-rectangle-free sets with log K_n = o(n), and let β(n) = o(n). Then for every ε > 0 and all large n, every circuit deciding S_n, over any basis on U, whose gates have fan-in at most r except for special gates of any fan-in with a ledger in a monoid M with log |M| ≤ β(n), has s ordinary inner gates with (r - 1) s > (1 + 1/A - ε) n. These are the inner gates of the erased program.

theorem Complexity.Frontier.lowerBound_aggregate {U : Type u} [Finite U] [Nontrivial U] {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (S : (n : ℕ) → Set (Fin n → U)) (K : ℕ → ℕ) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {β : ℕ → ℝ} (hβ : β =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) (T : Type) [inst : CommMonoid T] [Finite T], (∀ (g : Fin c.size), ¬special ↑g → σ.Arity (c.program.lines g).op ≤ r) → (∀ (g : Fin c.size), special ↑g → Aggregates (I (c.program.lines g).op) T) → ↑(Nat.card { g : Fin c.size // special ↑g }) * Real.log ↑(Nat.card T) ≤ β n → Decides c I Acc (S n) → (1 + 1 / A - ε) * ↑n < (↑r - 1) * ↑(erase special c.program).innerGates.card

Aggregate gates. Under the hypotheses of Frontier.lowerBound, let β(n) = o(n). For every ε > 0 and all large n, every circuit deciding S_n whose gates have fan-in at most r, except for k special gates of any fan-in that aggregate in a finite commutative monoid T, with k log |T| ≤ β(n), has s ordinary inner gates with (r - 1) s > (1 + 1/A - ε) n. For instance, the special gates may compute AND, OR, parity, or counts modulo a fixed m.