Exponentially small correlation below (1 + 1/(2A)) n gates

Let every set of ⌊n/2⌋ coordinates have cut rank at least ⌊n/2⌋ - τ n in the polar matrix of a quadratic form S_n over 𝔽₂, and let subcubic graphs have layouts of width (A + o(1)) β₁ + o(|V|) (LayoutBound 3 A). Balance the two finite bounds of Cslib.Circuits.Frontier.sq_correlation_quadForm_le_of_unread and Cslib.Circuits.Frontier.sq_correlation_quadForm_le_of_layout at θ n unread inputs, where θ = (1/2 - A (c - 1)) / (1 + A):

• with at least θ n unread inputs, correlation² ≤ 2^{-(θ - τ) n + O(1)};
• with fewer, the graph of a circuit of fan-in two with at most c n inner gates has cycle rank at most (c - 1 + θ) n + 1 (Compiler.cycleRank_add_ncard_read_le), hence a layout of width about A (c - 1 + θ) n, and the frontier bound gives the same exponent, since A (c - 1 + θ) - 1/2 = -θ.

So the correlation is 2^{-γ n} for every γ < (θ - τ)/2 = (c* - c)/(2L) - τ/2, where c* = 1 + 1/(2A) and L = 1 + 1/A (eventually_abs_correlation_quadForm_le), and for every γ < (c* - c)/(2L) when the deficiency is o(n) (eventually_abs_correlation_quadForm_le_of_isLittleO). Note c* = (1 + L)/2: the threshold is halfway between 1 and the coefficient L of the worst-case frontier lower bound (Cslib.Circuits.Frontier.circuitLowerBound_of_layoutBound).

Main results

• Cslib.Circuits.Frontier.eventually_abs_correlation_quadForm_le: correlation 2^{-γ n} for every γ < (c* - c)/(2L) - τ/2.
• Cslib.Circuits.Frontier.eventually_abs_correlation_quadForm_le_of_isLittleO: correlation 2^{-γ n} for every γ < (c* - c)/(2L), for a sublinear deficiency.

theorem Cslib.Circuits.Frontier.two_mul_rate_eq {A c : ℝ} (hA : 0 < A) : 2 * ((1 + 1 / (2 * A) - c) / (2 * (1 + 1 / A))) = (1 / 2 - A * (c - 1)) / (1 + A)

The rate in two forms: 2 (c* - c)/(2L) = (1/2 - A (c - 1)) / (1 + A), where c* = 1 + 1/(2A) and L = 1 + 1/A.

theorem Cslib.Circuits.Frontier.eventually_abs_correlation_quadForm_le {A c τ γ : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) (hc : 1 / 2 ≤ c) (hγ : γ < (1 + 1 / (2 * A) - c) / (2 * (1 + 1 / A)) - τ / 2) (Q : (n : ℕ) → Matrix (Fin n) (Fin n) (ZMod 2)) (hQ : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑((Q n + (Q n).transpose).cutRank U) + τ * ↑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. Let subcubic graphs have layouts of width (A + o(1)) β₁ + o(|V|) (LayoutBound 3 A), and let every set of ⌊n/2⌋ coordinates have cut rank at least ⌊n/2⌋ - τ n in Q_n + Q_nᵀ for all large n. Then for every c ≥ 1/2 and every γ < (c* - c)/(2L) - τ/2, where c* = 1 + 1/(2A) and L = 1 + 1/A, 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.

theorem Cslib.Circuits.Frontier.eventually_abs_correlation_quadForm_le_of_isLittleO {A c γ : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) (hc : 1 / 2 ≤ c) (hγ : γ < (1 + 1 / (2 * A) - c) / (2 * (1 + 1 / A))) (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, sublinear deficiency. Under LayoutBound 3 A, 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), where c* = 1 + 1/(2A) and L = 1 + 1/A, for all large n every circuit of fan-in at most two 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.