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

Balance the two finite bounds at the threshold θ n unread inputs, where θ = (1/2 - A (c - 1)) / (1 + A):

• with at least θ n unread inputs, the correlation is at most 2^{-(θ - τ) n / 2 + O(1)};
• with fewer, the compiled network has cycle rank at most (c - 1 + θ) n + 1, 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.

theorem Complexity.Correlation.abs_le_two_rpow_of_sq_le {y γ : ℝ} {n : ℕ} (h : y ^ 2 ≤ 2 ^ (-(2 * γ) * ↑n)) : |y| ≤ 2 ^ (-γ * ↑n)

From a squared bound to an absolute bound with half the exponent.

theorem Complexity.Correlation.eventually_abs_corr_le {A c τ γ : ℝ} (hA : 0 < A) (hlayout : Frontier.LayoutBound 3 A) (hc : 1 / 2 ≤ c) (hγ : 2 * γ < (1 / 2 - A * (c - 1)) / (1 + A) - τ) (Q : (n : ℕ) → Matrix (Fin n) (Fin n) (ZMod 2)) (hQ : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑(cutRank (Q n) U) + τ * ↑n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (C : Cslib.Circuits.Circuit σ n 1), C.FanInAtMost 2 → ↑C.innerSize ≤ c * ↑n → |(2 * Frontier.agreement (quadForm (Q n)) fun (x : Fin n → Bool) => C.eval I x 0) - 1| ≤ 2 ^ (-γ * ↑n)

Exponentially small correlation, rate form. Under the layout hypothesis with coefficient A, if every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - τ n, then every fan-in-two circuit with at most c n gates of positive arity, c ≥ 1/2, has correlation at most 2^{-γ n} with the quadratic form, for every γ with 2 γ < (1/2 - A (c - 1)) / (1 + A) - τ and all large n.

theorem Complexity.Correlation.eventually_abs_corr_le_of_isLittleO {A c γ : ℝ} (hA : 0 < A) (hlayout : Frontier.LayoutBound 3 A) (hc : 1 / 2 ≤ c) (hγ : 2 * γ < (1 / 2 - A * (c - 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) ≤ ↑(cutRank (Q n) U) + e n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (C : Cslib.Circuits.Circuit σ n 1), C.FanInAtMost 2 → ↑C.innerSize ≤ c * ↑n → |(2 * Frontier.agreement (quadForm (Q n)) fun (x : Fin n → Bool) => C.eval I x 0) - 1| ≤ 2 ^ (-γ * ↑n)

Exponentially small correlation, sublinear deficiency. If every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - o(n), the rate is every γ with 2 γ < (1/2 - A (c - 1)) / (1 + A).

theorem Complexity.Correlation.isLittleO_two_mul_robustDeficiency_add_one : (fun (n : ℕ) => ↑(2 * robustDeficiency (n / 2) + 1)) =o[Filter.atTop] fun (n : ℕ) => ↑n

The deficiency 2 (2 ⌊√⌊n/2⌋⌋ + 1) + 1 is sublinear.