Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.AverageCase

The average-case (4 - ε) n bound #

A circuit with at most (4 - ε) n gates agrees with a (K, ν)-balanced function on at most (1/2 + 3ν) 2ⁿ + 2^{(1 - ε/24) n} inputs, for K polynomial and n large, under the graph-ordering hypothesis.

This does not follow from the worst-case cut-counting lemma: an input whose past set is still small at a vertex lies in a thin rectangle, on which a balanced function is unconstrained. Instead the proof uses the direction of the wiring graph. At a cut, the forward-crossing bits are determined by the inputs read so far and the backward-crossing bits (trace_eq_of_agree_backward), and symmetrically for the future. This caps the number of cut assignments a fixed past or future can see, so the thin mass at a prefix L is at most (K - 1)(2^{n - a(L)} + 2^{n - c(L)}) with a(L) = |past L| - |forward cut| and c(L) = n - |past L| - |backward cut|. Along the vertex order a grows from 0 to the number of inputs read in steps of at most four, and a + c = n - |cut|, so a prefix with both a and c linear exists whenever the cutwidth is below (1 - Ω(ε)) n.

Circuits reading few inputs are handled separately: on every subcube fixing the read inputs the circuit is constant, and a balanced function is close to one half on a rectangle refining that subcube.

The attribution of the underlying compiler is as in FourN.

The wiring network has unique, direction-determined assignments #

Balanced functions on subcubes #

theorem Algebraic.Cutwidth.card_accepting_bounds_of_balanced {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} {ν : ℝ} (hbal : Balanced f K ν) {u : ℕ} (hu : u ≤ n) (hK₁ : K ≤ 2 ^ u) (hK₂ : K ≤ 2 ^ (n - u)) :
(1 / 2 - ν) * 2 ^ n ≤ ↑(accepting f).card ∧ ↑(accepting f).card ≤ (1 / 2 + ν) * 2 ^ n

The whole cube split at u coordinates is a rectangle with sides 2^u and 2^(n-u), so a balanced function accepts within ν of half of all inputs once both exceed K.

theorem Algebraic.Cutwidth.card_agree_le_of_dependsOnlyOn {n : ℕ} {g f : Cslib.BooleanFunction n} {K : ℕ} {ν : ℝ} (hbal : Balanced f K ν) {R : Finset (Fin n)} (hg : DependsOnlyOn g R) (hR : R.card + 2 * Nat.clog 2 K ≤ n) :
↑{x : Cslib.BitString n | g x = f x}.card ≤ (1 / 2 + ν) * 2 ^ n

Few inputs read. If g depends only on R and at least 2 ⌈log₂ K⌉ coordinates lie outside R, then g agrees with a (K, ν)-balanced f on at most (1/2 + ν) 2ⁿ inputs: on each subcube fixing R, g is constant, and refining the subcube by ⌈log₂ K⌉ free coordinates gives a rectangle on which f is balanced.

A good prefix of the vertex order #

theorem Algebraic.Cutwidth.Network.card_past_upto_le {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [LinearOrder V] (v : V) (hv : ∀ j ∈ N.read, ∀ j' ∈ N.read, N.portVertex j = v → N.portVertex j' = v → j = j') :
(N.past (upto v)).card ≤ (N.past (below v)).card + 1

Processing one vertex adds to the past at most one variable when no two variables are read at the same vertex.

theorem Algebraic.Cutwidth.Network.fwdCut_below_subset {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] [LinearOrder V] (v : V) :
N.fwdCut (below v) ⊆ N.fwdCut (upto v) ∪ N.edgesAt v

Processing one vertex removes from the forward cut only its incident edges.

theorem Algebraic.Cutwidth.Network.card_fwdCut_below_le {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] [LinearOrder V] (v : V) :
(N.fwdCut (below v)).card ≤ (N.fwdCut (upto v)).card + N.degree v

Processing one vertex drops the forward cut by at most its degree.

theorem Algebraic.Cutwidth.exists_good_prefix {V : Type} [Fintype V] [LinearOrder V] [Nonempty V] (P F : Finset V → ℕ) (t : ℕ) (hP0 : P ∅ = 0) (huniv : t + F Finset.univ ≤ P Finset.univ) (hstepP : ∀ (v : V), P (Network.upto v) ≤ P (Network.below v) + 1) (hstepF : ∀ (v : V), F (Network.below v) ≤ F (Network.upto v) + 3) :
∃ (L : Finset V), IsLowerSet ↑L ∧ t + F L ≤ P L ∧ P L < F L + t + 4

A good prefix. For quantities P and F on the prefixes of a finite linear order with P ∅ = 0, t + F univ ≤ P univ, P growing by at most one and F dropping by at most three per vertex, some prefix L has t ≤ P L - F L < t + 4.

theorem Algebraic.Cutwidth.Wiring.card_past_upto_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) [LinearOrder (Vertex p out)] (v : Vertex p out) :

A vertex of the wiring graph reads at most one variable.

Assembly #

theorem Algebraic.Cutwidth.card_agree_eq {n : ℕ} (g f : Cslib.BooleanFunction n) :
↑{x : Cslib.BitString n | g x = f x}.card = 2 ^ n - ↑(accepting g).card - ↑(accepting f).card + 2 * ↑(accepting g ∩ accepting f).card

Agreement counted through the accepting sets.

theorem Algebraic.Cutwidth.thin_mass_le {ε η C : ℝ} (hε : 0 < ε) (hε4 : ε ≤ 4) (hη : 0 ≤ η) (hη1 : η ≤ ε / 36) (hC : 0 ≤ C) {n : ℕ} (hn : 2 ≤ n) {K c : ℕ} (hK : K ≤ n ^ c) (hlog : (2 * ↑c + 3) * Real.logb 2 ↑n + (C + 24) < ε * ↑n / 24) {s n' : ℕ} (hs : ↑s ≤ (4 - ε) * ↑n) (hn'le : n' ≤ n) (hread : n - n' < 2 * Nat.clog 2 K) {Vb : ℝ} (hVpos : 0 < Vb) (hVb : Vb ≤ 16 * ↑n) {t : ℕ} (ht : ε * ↑n / 12 ≤ ↑t) (ht' : ↑t < ε * ↑n / 12 + 1) {P F B : ℕ} (hP : P ≤ n) (hgood₁ : t + F ≤ P) (hgood₂ : P < F + t + 4) (hcut : ↑(F + B) ≤ (1 / 3 + η) * max (↑s - ↑n') 0 + 3 * Real.logb 2 Vb + C) :
2 * (↑(K - 1) * (2 ^ (n - P + F) + 2 ^ (P + B))) ≤ 2 ^ ((1 - ε / 24) * ↑n)

The numeric core of the average case. At a good prefix, twice the thin-rectangle mass of the one-sided count is at most 2 ^ ((1 - ε/24) n), once n satisfies an explicit logarithmic condition.

theorem Algebraic.Cutwidth.card_agree_le_of_bounds {ε η C : ℝ} (hε : 0 < ε) (hε4 : ε ≤ 4) (hη : 0 ≤ η) (hη1 : η ≤ ε / 36) (hC : 0 ≤ C) (order : Multigraph.OrderingBound η C) {n : ℕ} (hn : 2 ≤ n) {f : Cslib.BooleanFunction n} {K c : ℕ} (hK : K ≤ n ^ c) {ν : ℝ} (hν : 0 ≤ ν) (hbal : Balanced f K ν) (hlog : (2 * ↑c + 3) * Real.logb 2 ↑n + (C + 24) < ε * ↑n / 24) (circuit : Circuit Binary.signature n 1) (hs : ↑circuit.size ≤ (4 - ε) * ↑n) :
↑{x : Fin n → Bool | circuit.eval Binary.interpretation x 0 = f x}.card ≤ (1 / 2 + 3 * ν) * 2 ^ n + 2 ^ ((1 - ε / 24) * ↑n)

The fixed-n average-case bound. With the graph-ordering hypothesis for slack η ≤ ε/36, a circuit with at most (4 - ε) n binary gates agrees with a (K, ν)-balanced function, K ≤ n ^ c, on at most (1/2 + 3ν) 2ⁿ + 2 ^ ((1 - ε/24) n) inputs, once n satisfies an explicit logarithmic condition.

theorem Algebraic.Cutwidth.eventually_card_agree_le (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound η C) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) {ν : ℝ} (hν : 0 ≤ ν) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hbal : ∀ᶠ (n : ℕ) in Filter.atTop, Balanced (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) :
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), ↑circuit.size ≤ (4 - ε) * ↑n → ↑{x : Fin n → Bool | circuit.eval Binary.interpretation x 0 = f n x}.card ≤ (1 / 2 + 3 * ν) * 2 ^ n + 2 ^ ((1 - ε / 24) * ↑n)

Theorem (average case). Assume the graph-ordering lemma for every slack η > 0 and a family f n that is (K n, ν)-balanced with K n ≤ n ^ c for all large n. Then for every ε > 0 and all sufficiently large n, every binary circuit with at most (4 - ε) n gates agrees with f n on at most (1/2 + 3ν) 2ⁿ + 2 ^ ((1 - ε/24) n) inputs.

theorem Algebraic.Cutwidth.eventually_card_agree_le_of_pathwidthBound (pathwidth : ∀ (ξ : ℝ), 0 < ξ → ∃ (N₀ : ℕ), PathwidthBound ξ N₀) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) {ν : ℝ} (hν : 0 ≤ ν) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hbal : ∀ᶠ (n : ℕ) in Filter.atTop, Balanced (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) :
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), ↑circuit.size ≤ (4 - ε) * ↑n → ↑{x : Fin n → Bool | circuit.eval Binary.interpretation x 0 = f n x}.card ≤ (1 / 2 + 3 * ν) * 2 ^ n + 2 ^ ((1 - ε / 24) * ↑n)

The average case from the pathwidth hypothesis.