Exponentially small correlation with quadratic forms

Circuits of fan-in at most two over any basis on Bool, with at most c n gates of positive arity, have correlation 2^{-Ω(n)} with a nonconstructively chosen family of bilinear forms xᵀ R y over 𝔽₂, for every c < c* = 1 + 1/(2A) ≈ 2.78125. Here A = 2p ≈ 0.2807 is the Gaussian layout coefficient of the frontier method (Cslib.Circuits.Frontier.layoutBound_gaussian), and c* = (1 + L)/2 for the coefficient L = 1 + 1/A ≈ 4.5625 of the worst-case frontier lower bound (Cslib.Circuits.Frontier.circuitLowerBound_gaussian). Correlation is measured in the terms of the average-case frontier lower bound: correlation S T = 2 · agreement S T - 1 (Cslib.Circuits.Frontier.correlation_eq_two_mul_agreement_sub_one), so a correlation of absolute value at most ε is an agreement of at most 1/2 + ε/2. The circuit model and the gate count (Cslib.Circuits.Circuit.innerSize) are those of Cslib.Circuits.Frontier.AverageCaseBound. The best previously published average-case bounds for the full binary basis are 2.5 n, for an explicit affine extractor Chen–Kabanets, and 2.6 n, for non-explicit quadratic extractors Golovnev–Kulikov–Smal–Tamaki. Because the family here is chosen nonconstructively, the comparable bound is the non-explicit one; nothing here improves on the explicit 2.5 n.

The argument

For a quadratic form f over 𝔽₂ and a cut X of the coordinates, Lindsey's lemma bounds the signed sum of (-1)^f over every rectangle R for X by √(|R| 2^{n - ρ(X)}), where the cut rank ρ(X) is the rank of the block of the polar matrix with rows X and columns Xᶜ (Cslib.Circuits.Frontier.sq_signedCount_quadForm_rectangle_mul_le). Partition the inputs into K rectangle classes for one cut on which the circuit is constant; Cauchy–Schwarz over the classes gives correlation² ≤ K · 2^{-ρ(X)} (Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le). Two partitions apply:

• if the circuit leaves the inputs D unread, its two output classes are rectangles for D;
• along a layout of the graph of the circuit, the inputs with a given output and a given state of the read-once branching program of its constraint network, at the layer where exactly ⌊n/2⌋ inputs have been read, form 2 · 2^w rectangle classes for a layout of width w.

If every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - τ n, balancing the two at θ n unread inputs, with θ = (1/2 - A (c - 1))/(1 + A), gives the rate (c* - c)/(2L) - τ/2 (Cslib.Circuits.Frontier.eventually_abs_correlation_quadForm_le), and (c* - c)/(2L) for a sublinear deficiency (eventually_abs_correlation_quadForm_le_gaussian).

A nonconstructively chosen family

A matrix is submatrix-robust with deficiency t when every square block with k rows has rank at least k - t. Counting spanning sets of columns shows that for t = 2 ⌊√m⌋ + 1 such an m × m matrix over 𝔽₂ exists (Matrix.exists_submatrixRobust). The family hardForm n = xᵀ R y uses a fixed such matrix R = robustMatrix ⌊n/2⌋ between the first ⌊n/2⌋ coordinates x and the next ⌊n/2⌋ coordinates y. The matrix is chosen nonconstructively by Classical.choose; no efficient construction is supplied. Its bisection cut rank is at least ⌊n/2⌋ - O(√n) (half_le_cutRank_hardMatrix).

Remark, not formalized. Taking instead the lexicographically first robust matrix makes the family computable in E^NP: whether some robust matrix extends a given prefix is one NP query of length 2^{O(n)} (guess the matrix and check its fewer than 4^{n/2} pairs of row and column sets), so the matrix is found bit by bit in time 2^{O(n)}. Nothing in this file states or proves this uniformity.

Main definitions

• Cslib.Circuits.Frontier.robustMatrix k: a fixed submatrix-robust k × k matrix over 𝔽₂.
• Cslib.Circuits.Frontier.hardForm n: a nonconstructively chosen family of bilinear forms xᵀ R y.

Main results

• Cslib.Circuits.Frontier.eventually_abs_correlation_quadForm_le_gaussian: correlation 2^{-γ n} below c n gates for every family of quadratic forms whose bisection cut rank is ⌊n/2⌋ - o(n), for every γ < (c* - c)/(2L).
• Cslib.Circuits.Frontier.half_le_cutRank_hardMatrix: the bisection cut rank of the chosen family.
• Cslib.Circuits.Frontier.eventually_abs_correlation_hardForm_le: the headline bound for the chosen family.
• Cslib.Circuits.Frontier.exists_eventually_abs_correlation_hardForm_le_of_lt: below c n gates, for any c < c*, a fixed rate γ > 0.
• Cslib.Circuits.Frontier.exists_eventually_abs_correlation_hardForm_le: below 2.77 n gates, correlation 2^{-γ n} for a fixed γ > 0.

References

• R. Chen, V. Kabanets, Correlation bounds and #SAT algorithms for small linear-size circuits
• A. Golovnev, A. S. Kulikov, A. V. Smal, S. Tamaki, Circuit size lower bounds and #SAT upper bounds through a general framework
• S. Jukna, Extremal Combinatorics, Ch. 14

The Gaussian rate

theorem Cslib.Circuits.Frontier.gaussian_rate_eq (c : ℝ) : (1 + 1 / (2 * (2 * Gaussian.gaussianCoefficient)) - c) / (2 * (1 + 1 / (2 * Gaussian.gaussianCoefficient))) = (1 + Real.pi / (6 * Real.arccos ((1 + 2 * √2) / 4)) - c) / (2 * (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4))))

The threshold and the rate of the Gaussian layout coefficient A = 2p in closed form: c* = 1 + π / (6 arccos ((1 + 2√2)/4)) and L = 1 + π / (3 arccos ((1 + 2√2)/4)).

theorem Cslib.Circuits.Frontier.correlationThreshold_ge : 139 / 50 ≤ 1 + Real.pi / (6 * Real.arccos ((1 + 2 * √2) / 4))

The threshold is above 2.78: c* = 1 + π / (6 arccos ((1 + 2√2)/4)) ≥ 139/50, since c* = (1 + L)/2 and L ≥ 114/25 (Gaussian.circuitCoefficient_ge_456).

theorem Cslib.Circuits.Frontier.eventually_abs_correlation_quadForm_le_gaussian {c γ : ℝ} (hc : 1 / 2 ≤ c) (hγ : γ < (1 + Real.pi / (6 * Real.arccos ((1 + 2 * √2) / 4)) - c) / (2 * (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4))))) (Q : (n : ℕ) → Matrix (Fin n) (Fin n) (ZMod 2)) (e : ℕ → ℝ) (he : e =o[Filter.atTop] fun (n : ℕ) => ↑n) (hQ : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑((Q n + (Q n).transpose).cutRank U) + e n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Signature) (I : Interpretation σ Bool) (Acc : Set Bool) (C : Circuit σ n 1), C.FanInAtMost 2 → ↑C.innerSize ≤ c * ↑n → |correlation {x : Fin n → Bool | BitString.quadForm (Q n) x = true} {x : Fin n → Bool | C.eval I x 0 ∈ Acc}| ≤ 2 ^ (-γ * ↑n)

Exponentially small correlation below 2.78 n gates. If every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - o(n) in Q_n + Q_nᵀ, then for every c ≥ 1/2 and every γ < (c* - c)/(2L), with c* = 1 + π / (6 arccos ((1 + 2√2)/4)) ≈ 2.78125 and L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625, for all large n every circuit of fan-in at most two, over any basis on Bool and accepting any set of values, with at most c n gates of positive arity has correlation at most 2^{-γ n} in absolute value with the quadratic form of Q_n.

A nonconstructively chosen family

def Cslib.Circuits.Frontier.leftHalf (n : ℕ) (a : Fin (n / 2)) : Fin n

The coordinate of an input of length n holding the entry a of its left half x: the left half is the first ⌊n/2⌋ coordinates.

def Cslib.Circuits.Frontier.rightHalf (n : ℕ) (b : Fin (n / 2)) : Fin n

The coordinate of an input of length n holding the entry b of its right half y: the right half is the next ⌊n/2⌋ coordinates. For odd n the last coordinate is in neither half.

theorem Cslib.Circuits.Frontier.leftHalf_injective (n : ℕ) : Function.Injective (leftHalf n)

theorem Cslib.Circuits.Frontier.rightHalf_injective (n : ℕ) : Function.Injective (rightHalf n)

theorem Cslib.Circuits.Frontier.disjoint_range_leftHalf_rightHalf (n : ℕ) : Disjoint (Set.range (leftHalf n)) (Set.range (rightHalf n))

The two halves are disjoint.

noncomputable def Cslib.Circuits.Frontier.robustMatrix (k : ℕ) : Matrix (Fin k) (Fin k) (ZMod 2)

A fixed submatrix-robust k × k matrix over 𝔽₂ with deficiency 2 ⌊√k⌋ + 1, chosen once and for all by Classical.choose from Matrix.exists_submatrixRobust.

theorem Cslib.Circuits.Frontier.robustMatrix_submatrixRobust (k : ℕ) : (robustMatrix k).SubmatrixRobust (2 * k.sqrt + 1)

noncomputable def Cslib.Circuits.Frontier.hardMatrix (n : ℕ) : Matrix (Fin n) (Fin n) (ZMod 2)

The matrix of the chosen family: robustMatrix ⌊n/2⌋ in the block whose rows are the left half and whose columns are the right half, and zeros elsewhere.

noncomputable def Cslib.Circuits.Frontier.hardForm (n : ℕ) : (Fin n → Bool) → Bool

The nonconstructively chosen family: on inputs of length n, the quadratic form of hardMatrix n, which is the bilinear form xᵀ R y of R = robustMatrix ⌊n/2⌋ between the left half x and the right half y (hardForm_apply). The matrix R is chosen by Classical.choose.

theorem Cslib.Circuits.Frontier.hardForm_apply (n : ℕ) (x : Fin n → Bool) : hardForm n x = decide (((fun (a : Fin (n / 2)) => BitString.bitVal (ZMod 2) (x (leftHalf n a))) ⬝ᵥ (robustMatrix (n / 2)).mulVec fun (b : Fin (n / 2)) => BitString.bitVal (ZMod 2) (x (rightHalf n b))) = 1)

The chosen family is the bilinear form xᵀ R y of R = robustMatrix ⌊n/2⌋.

theorem Cslib.Circuits.Frontier.half_le_cutRank_hardMatrix (n : ℕ) {U : Set (Fin n)} (hU : U.ncard = n / 2) : n / 2 ≤ (hardMatrix n + (hardMatrix n).transpose).cutRank U + (2 * (2 * (n / 2).sqrt + 1) + 1)

Bisection cut rank of the chosen family. Every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - (2 (2 ⌊√⌊n/2⌋⌋ + 1) + 1) in the polar matrix of hardMatrix n.

theorem Cslib.Circuits.Frontier.isLittleO_hardDeficiency : (fun (n : ℕ) => ↑(2 * (2 * (n / 2).sqrt + 1) + 1)) =o[Filter.atTop] fun (n : ℕ) => ↑n

The deficiency 2 (2 ⌊√⌊n/2⌋⌋ + 1) + 1 of the chosen family is sublinear.

theorem Cslib.Circuits.Frontier.half_le_cutRank_hardMatrix_add (n : ℕ) (U : Set (Fin n)) (hU : U.ncard = n / 2) : ↑(n / 2) ≤ ↑((hardMatrix n + (hardMatrix n).transpose).cutRank U) + ↑(2 * (2 * (n / 2).sqrt + 1) + 1)

The bisection hypothesis for the chosen family, in the form used by the asymptotic bounds.

theorem Cslib.Circuits.Frontier.eventually_abs_correlation_hardForm_le {c γ : ℝ} (hc : 1 / 2 ≤ c) (hγ : γ < (1 + Real.pi / (6 * Real.arccos ((1 + 2 * √2) / 4)) - c) / (2 * (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4))))) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Signature) (I : Interpretation σ Bool) (Acc : Set Bool) (C : Circuit σ n 1), C.FanInAtMost 2 → ↑C.innerSize ≤ c * ↑n → |correlation {x : Fin n → Bool | hardForm n x = true} {x : Fin n → Bool | C.eval I x 0 ∈ Acc}| ≤ 2 ^ (-γ * ↑n)

Exponentially small correlation with the chosen family below 2.78 n gates. For every c ≥ 1/2 and every γ < (c* - c)/(2L), with c* = 1 + π / (6 arccos ((1 + 2√2)/4)) ≈ 2.78125 and L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625, for all large n every circuit of fan-in at most two, over any basis on Bool and accepting any set of values, with at most c n gates of positive arity has correlation at most 2^{-γ n} in absolute value with hardForm n.

theorem Cslib.Circuits.Frontier.exists_eventually_abs_correlation_hardForm_le_of_lt {c : ℝ} (hc : c < 1 + Real.pi / (6 * Real.arccos ((1 + 2 * √2) / 4))) : ∃ (γ : ℝ), 0 < γ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Signature) (I : Interpretation σ Bool) (Acc : Set Bool) (C : Circuit σ n 1), C.FanInAtMost 2 → ↑C.innerSize ≤ c * ↑n → |correlation {x : Fin n → Bool | hardForm n x = true} {x : Fin n → Bool | C.eval I x 0 ∈ Acc}| ≤ 2 ^ (-γ * ↑n)

Every coefficient below the threshold. For every c < c*, where c* = 1 + π / (6 arccos ((1 + 2√2)/4)) ≈ 2.78125, some fixed γ > 0 bounds, for all large n, the correlation of every circuit of fan-in at most two, over any basis on Bool and accepting any set of values, with at most c n gates of positive arity, with hardForm n by 2^{-γ n}.

theorem Cslib.Circuits.Frontier.exists_eventually_abs_correlation_hardForm_le : ∃ (γ : ℝ), 0 < γ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Signature) (I : Interpretation σ Bool) (Acc : Set Bool) (C : Circuit σ n 1), C.FanInAtMost 2 → ↑C.innerSize ≤ 277 / 100 * ↑n → |correlation {x : Fin n → Bool | hardForm n x = true} {x : Fin n → Bool | C.eval I x 0 ∈ Acc}| ≤ 2 ^ (-γ * ↑n)

Below 2.77 n gates. Some fixed γ > 0 bounds, for all large n, the correlation of every circuit of fan-in at most two, over any basis on Bool and accepting any set of values, with at most 2.77 n gates of positive arity, with hardForm n by 2^{-γ n}.