Correlation of one circuit with a quadratic form

Two partitions of the inputs of a circuit with one output into rectangle classes bound its correlation with a quadratic form S over 𝔽₂ (Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le):

• unread inputs (sq_correlation_quadForm_mul_le_of_unread): if the circuit does not read the inputs in D, the inputs it accepts and those it rejects are rectangles for the cut D, so correlation² · 2^{ρ(D)} ≤ 2;
• the frontier of a layout (sq_correlation_quadForm_mul_le_of_layout): the inputs that the circuit accepts are the accepted inputs of an unambiguous read-once branching program, that of its constraint network along a layout (Cslib.Circuits.Frontier.Network.branchingProgram). The inputs whose accepting paths share a state at layer t form a rectangle for the cut of the inputs read by the first t vertices (ReadOnceNBP.Unambiguous.peers_eq_rectangle), and the states are values on the frontier, at most 2 ^ |frontier| of them (Network.ncard_image_path_le). With the rejected inputs likewise, correlation² · 2^{ρ(X)} ≤ 2 · 2^{|frontier|}.

Here ρ is the cut rank of the polar matrix Q + Qᵀ. If every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - e, then smaller sets D have cut rank at least |D| - e (ncard_le_cutRank_add_of_bisection), and since a circuit of fan-in two reads its inputs one at a time along a layout (Network.exists_ncard_readIn_initial_eq), some layer has read exactly ⌊n/2⌋ of them. This gives the finite bounds correlation² ≤ 2^{1 + e - k} for a circuit leaving k ≤ ⌊n/2⌋ inputs unread (sq_correlation_quadForm_le_of_unread) and correlation² ≤ 2^{1 + w + e - ⌊n/2⌋} for a layout of width w (sq_correlation_quadForm_le_of_layout).

Main results

• Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le_of_unread, Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le_of_layout: rectangle classes of a circuit.
• Cslib.Circuits.Frontier.sq_correlation_quadForm_le_of_unread, Cslib.Circuits.Frontier.sq_correlation_quadForm_le_of_layout: the finite bounds under a bisection hypothesis on the cut ranks.

Rectangle classes of a circuit

theorem Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le_of_unread {σ : Signature} {n : ℕ} (I : Interpretation σ Bool) (Acc : Set Bool) (c : Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) {D : Set (Fin n)} (hD : D ⊆ (Compiler.network c I fun (x : Fin 1) => Acc).readᶜ) : correlation {x : Fin n → Bool | BitString.quadForm Q x = true} {x : Fin n → Bool | c.eval I x 0 ∈ Acc} ^ 2 * 2 ^ (Q + Q.transpose).cutRank D ≤ 2

Unread inputs. If a circuit does not read the inputs in D, the inputs it accepts and those it rejects are rectangles for the cut D, so its correlation with the quadratic form of Q satisfies correlation² · 2^{ρ(D)} ≤ 2, where ρ is the cut rank of Q + Qᵀ.

theorem Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le_of_layout {σ : Signature} {n : ℕ} (I : Interpretation σ Bool) (Acc : Set Bool) (c : Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) (π : Layout (Compiler.Vertex c)) {t : ℕ} (ht : t ≤ Nat.card (Compiler.Vertex c)) : correlation {x : Fin n → Bool | BitString.quadForm Q x = true} {x : Fin n → Bool | c.eval I x 0 ∈ Acc} ^ 2 * 2 ^ (Q + Q.transpose).cutRank ((Compiler.network c I fun (x : Fin 1) => Acc).readIn (π.initial t)) ≤ 2 * 2 ^ ((Compiler.graph c).frontier π t).ncard

Frontier classes. Along a layout of the graph of a circuit, the inputs with a given output and a given state at layer t ≤ |V| of the branching program form a rectangle for the cut X of the inputs read by the first t vertices. So the correlation of the circuit with the quadratic form of Q satisfies correlation² · 2^{ρ(X)} ≤ 2 · 2^{|frontier t|}, where ρ is the cut rank of Q + Qᵀ.

Finite bounds under a bisection hypothesis

theorem Cslib.Circuits.Frontier.ncard_le_cutRank_add_of_bisection {n : ℕ} {M : Matrix (Fin n) (Fin n) (ZMod 2)} {e : ℝ} (hM : ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑(M.cutRank U) + e) {D : Set (Fin n)} (hD : D.ncard ≤ n / 2) : ↑D.ncard ≤ ↑(M.cutRank D) + e

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

theorem Cslib.Circuits.Frontier.sq_correlation_quadForm_le_of_unread {σ : Signature} {n : ℕ} (I : Interpretation σ Bool) (Acc : Set Bool) (c : Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) {e : ℝ} (hQ : ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑((Q + Q.transpose).cutRank U) + e) {k : ℕ} (hk : k ≤ n / 2) (hkd : k ≤ (Compiler.network c I fun (x : Fin 1) => Acc).readᶜ.ncard) : correlation {x : Fin n → Bool | BitString.quadForm Q x = true} {x : Fin n → Bool | c.eval I x 0 ∈ Acc} ^ 2 ≤ 2 ^ (1 + e - ↑k)

Unread inputs, finite form. If every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - e in Q + Qᵀ, a circuit that leaves at least k ≤ ⌊n/2⌋ inputs unread has correlation² ≤ 2^{1 + e - k} with the quadratic form of Q.

theorem Cslib.Circuits.Frontier.sq_correlation_quadForm_le_of_layout {σ : Signature} {n : ℕ} (I : Interpretation σ Bool) (Acc : Set Bool) (c : Circuit σ n 1) (Q : Matrix (Fin n) (Fin n) (ZMod 2)) {e : ℝ} (hQ : ∀ (U : Set (Fin n)), U.ncard = n / 2 → ↑(n / 2) ≤ ↑((Q + Q.transpose).cutRank U) + e) (π : Layout (Compiler.Vertex c)) {w : ℕ} (hw : (Compiler.graph c).width π ≤ w) (hread : n / 2 ≤ (Compiler.network c I fun (x : Fin 1) => Acc).read.ncard) : correlation {x : Fin n → Bool | BitString.quadForm Q x = true} {x : Fin n → Bool | c.eval I x 0 ∈ Acc} ^ 2 ≤ 2 ^ (1 + ↑w + e - ↑(n / 2))

The frontier bound, finite form. If every set of ⌊n/2⌋ coordinates has cut rank at least ⌊n/2⌋ - e in Q + Qᵀ, a circuit that reads at least ⌊n/2⌋ inputs, whose graph has a layout of width at most w, has correlation² ≤ 2^{1 + w + e - ⌊n/2⌋} with the quadratic form of Q.