Finite correlation bounds for circuits

Two partitions of the inputs of a circuit into rectangle classes:

• by the output alone, if the circuit ignores the inputs in D: each output class is a rectangle for the cut D;
• by the output and the values on the frontier of a layout of the compiled constraint network at time t: by the separator lemma each class is a rectangle for the cut X of the inputs read before time t, and there are at most 2 · 2^w classes for a layout of width w.

With a bisection hypothesis on the cut ranks, the inputs read before some time number exactly ⌊n/2⌋, since reads grow one at a time.

theorem Complexity.Correlation.readIn_insert_subset {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Frontier.Network U ι V E) (v : V) (L : Set V) : N.readIn (insert v L) ⊆ N.readIn L ∪ N.readAt v

The inputs read by a set with one more vertex.

theorem Complexity.Correlation.exists_ncard_readIn_eq {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Frontier.Network U ι V E) [Finite ι] (π : Frontier.Layout V) (hm : ∀ (v : V), (N.readAt v).ncard ≤ 1) {k : ℕ} (hk : k ≤ N.read.ncard) : ∃ t ≤ Nat.card V, (N.readIn (π.initial t)).ncard = k

Reads grow one at a time. If each vertex reads at most one input, some initial segment of every layout reads exactly k inputs, for every k up to the number read.

theorem Complexity.Correlation.accepted_constraintNetwork_eval {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) (b : Bool) : (Frontier.constraintNetwork I {b} c).accepted = {x : Fin n → Bool | c.eval I x 0 = b}

theorem Complexity.Correlation.read_constraintNetwork {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) (b : Bool) : (Frontier.constraintNetwork I {b} c).read = (Frontier.constraintNetwork I {true} c).read

theorem Complexity.Correlation.sq_corr_mul_le_of_unread {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) {D : Set (Fin n)} (hD : D ⊆ (Frontier.constraintNetwork I {true} c).readᶜ) : ((2 * Frontier.agreement (quadForm Q) fun (x : Fin n → Bool) => c.eval I x 0) - 1) ^ 2 * 2 ^ cutRank Q D ≤ 2

Unread inputs. If a circuit does not read the inputs in D, its two output classes are rectangles for the cut D.

theorem Complexity.Correlation.sq_corr_mul_le_of_layout {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) (π : Frontier.Layout (Frontier.Compiler.Vertex c.program c.outputs)) {t : ℕ} (ht : t ≤ Nat.card (Frontier.Compiler.Vertex c.program c.outputs)) : ((2 * Frontier.agreement (quadForm Q) fun (x : Fin n → Bool) => c.eval I x 0) - 1) ^ 2 * 2 ^ cutRank Q ((Frontier.constraintNetwork I {true} c).readIn (π.initial t)) ≤ 2 * 2 ^ ((Frontier.constraintNetwork I {true} c).frontier π t).ncard

Frontier classes. Along a layout of the compiled network, the inputs with a given output and given values on the frontier at time t form a rectangle for the cut of the inputs read before time t.

theorem Complexity.Correlation.ncard_le_cutRank_add_of_bisection {n : ℕ} (Q : Matrix (Fin n) (Fin n) (ZMod 2)) {e : ℝ} (hQ : ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑(cutRank Q U) + e) {D : Set (Fin n)} (hD : D.ncard ≤ n / 2) : ↑D.ncard ≤ ↑(cutRank Q D) + e

Small sets have large cut rank. If every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - e, then every set D of at most ⌊n/2⌋ coordinates has cut rank at least |D| - e.

theorem Complexity.Correlation.le_rpow_of_mul_two_pow_le {y : ℝ} {ρ m : ℕ} {r : ℝ} (hy : y * 2 ^ ρ ≤ 2 * 2 ^ m) (hr : r ≤ ↑ρ) : y ≤ 2 ^ (1 + ↑m - r)

A bound y · 2^ρ ≤ 2 · 2^m with ρ ≥ r gives y ≤ 2^(1 + m - r) in real exponents.

theorem Complexity.Correlation.sq_corr_le_of_unread {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) {e : ℝ} (hQ : ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑(cutRank Q U) + e) {k : ℕ} (hk : k ≤ n / 2) (hkd : k ≤ (Frontier.constraintNetwork I {true} c).readᶜ.ncard) : ((2 * Frontier.agreement (quadForm Q) fun (x : Fin n → Bool) => c.eval I x 0) - 1) ^ 2 ≤ 2 ^ (1 + e - ↑k)

Theorem (unread inputs, finite). Under the bisection hypothesis, a circuit that leaves at least k ≤ ⌊n/2⌋ inputs unread has squared correlation at most 2^(1 + e - k).

theorem Complexity.Correlation.sq_corr_le_of_layout {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) {e : ℝ} (hQ : ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑(cutRank Q U) + e) (π : Frontier.Layout (Frontier.Compiler.Vertex c.program c.outputs)) {w : ℕ} (hw : ∀ (t : ℕ), ((Frontier.constraintNetwork I {true} c).frontier π t).ncard ≤ w) (hread : n / 2 ≤ (Frontier.constraintNetwork I {true} c).read.ncard) : ((2 * Frontier.agreement (quadForm Q) fun (x : Fin n → Bool) => c.eval I x 0) - 1) ^ 2 ≤ 2 ^ (1 + ↑w + e - ↑(n / 2))

Theorem (frontier, finite). Under the bisection hypothesis, if a circuit reads at least ⌊n/2⌋ inputs and its compiled network has a layout with every frontier of at most w edges, its squared correlation is at most 2^(1 + w + e - ⌊n/2⌋).