The split lemma for threshold programs

Fix a split of the coordinates into U and its complement, and suppose every gate of a threshold program reads inputs from one side only (C.support j ⊆ U or C.support j ⊆ Uᶜ). Processing the gates in order while maintaining a rectangle P × Q on which every earlier gate is constant, a gate reading only U is a function of p alone on the rectangle, so splitting P by its value and keeping the larger half costs a factor 2 on P; a gate whose support lies in a fixed set A ⊆ U on which all of P agrees is constant and costs nothing. The second side is symmetric with B ⊆ Uᶜ.

• exists_rectangle_of_split_internal: starting from the inputs vanishing on A and on B, the final rectangle has f constant, with 2 ^ (|U| - |A|) ≤ |P| · 2 ^ #{j : support j ⊆ U, support j ⊄ A} and symmetrically for Q.

theorem Algebraic.Threshold.weightedSum_congr_internal {n : ℕ} (w : Fin n → ℝ) {x y : Fin n → Bool} (h : ∀ (i : Fin n), w i ≠ 0 → x i = y i) : weightedSum w x = weightedSum w y

theorem Algebraic.Threshold.weightedSum_eq_zero_internal {n : ℕ} (w : Fin n → ℝ) {x : Fin n → Bool} (h : ∀ (i : Fin n), w i ≠ 0 → x i = false) : weightedSum w x = 0

theorem Algebraic.Threshold.Program.mem_support_internal {n s : ℕ} (C : Program n s) (j : Fin s) (i : Fin n) : i ∈ C.support j ↔ C.inputWeight j i ≠ 0

theorem Algebraic.Threshold.Program.eval_eq_of_lt_internal {n s : ℕ} (C : Program n s) (x : Fin n → Bool) (v : Fin s → Bool) (j : Fin s) (hv : ∀ k < j, C.eval x k = v k) : C.eval x j = decide (0 ≤ weightedSum (C.inputWeight j) x + ((∑ k : Fin s, if k < j then C.gateWeight j k * ↑(v k).toNat else 0) + C.bias j))

theorem Algebraic.Threshold.Program.weightedSum_glue_left_internal {n s : ℕ} (C : Program n s) {j : Fin s} {U : Finset (Fin n)} (hU : C.support j ⊆ U) (p : ↥U → Bool) (q q' : ↥Uᶜ → Bool) : weightedSum (C.inputWeight j) (Cutwidth.glue U p q) = weightedSum (C.inputWeight j) (Cutwidth.glue U p q')

A gate whose support lies in U reads a glued input through p alone.

theorem Algebraic.Threshold.Program.weightedSum_glue_right_internal {n s : ℕ} (C : Program n s) {j : Fin s} {U : Finset (Fin n)} (hU : C.support j ⊆ Uᶜ) (p p' : ↥U → Bool) (q : ↥Uᶜ → Bool) : weightedSum (C.inputWeight j) (Cutwidth.glue U p q) = weightedSum (C.inputWeight j) (Cutwidth.glue U p' q)

A gate whose support lies in Uᶜ reads a glued input through q alone.

noncomputable def Algebraic.Threshold.Program.countBelow {n s : ℕ} (C : Program n s) (S T : Finset (Fin n)) (m : ℕ) : ℕ

The number of gates below m whose support lies in S but not in T.

Equations

• C.countBelow S T m = {j : Fin s | ↑j < m ∧ C.support j ⊆ S ∧ ¬C.support j ⊆ T}.card

theorem Algebraic.Threshold.Program.countBelow_succ {n s : ℕ} (C : Program n s) (S T : Finset (Fin n)) {m : ℕ} (j₀ : Fin s) (hj₀ : ↑j₀ = m) : C.countBelow S T (m + 1) = C.countBelow S T m + if C.support j₀ ⊆ S ∧ ¬C.support j₀ ⊆ T then 1 else 0

theorem Algebraic.Threshold.Program.countBelow_zero {n s : ℕ} (C : Program n s) (S T : Finset (Fin n)) : C.countBelow S T 0 = 0

theorem Algebraic.Threshold.Program.countBelow_top {n s : ℕ} (C : Program n s) (S T : Finset (Fin n)) : C.countBelow S T s = {j : Fin s | C.support j ⊆ S ∧ ¬C.support j ⊆ T}.card

theorem Algebraic.Threshold.exists_half_internal {α : Type u_1} (P : Finset α) (g : α → Bool) : ∃ (b : Bool), P.card ≤ 2 * {p ∈ P | g p = b}.card

Some side of a split by a Boolean function keeps at least half of a finite set.

theorem Algebraic.Threshold.exists_initial_internal {n : ℕ} (S A : Finset (Fin n)) (hA : A ⊆ S) : ∃ (P : Finset (↥S → Bool)), 2 ^ (S.card - A.card) ≤ P.card ∧ ∀ p ∈ P, ∀ (i : ↥S), ↑i ∈ A → p i = false

The assignments to S vanishing on A ⊆ S number 2 ^ (|S| - |A|).

def Algebraic.Threshold.Program.SplitInv {n s : ℕ} (C : Program n s) (U A B : Finset (Fin n)) (m : ℕ) : Prop

The invariant after the first m gates: a rectangle P × Q, with P vanishing on A and Q vanishing on B, on which every gate below m takes the value v, and whose sides have lost at most a factor 2 per counted gate.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Threshold.Program.splitInv_zero {n s : ℕ} (C : Program n s) {U A B : Finset (Fin n)} (hA : A ⊆ U) (hB : B ⊆ Uᶜ) : C.SplitInv U A B 0

theorem Algebraic.Threshold.Program.splitInv_succ {n s : ℕ} (C : Program n s) {U A B : Finset (Fin n)} (hA : A ⊆ U) (hB : B ⊆ Uᶜ) (hsplit : ∀ (j : Fin s), C.support j ⊆ U ∨ C.support j ⊆ Uᶜ) {m : ℕ} (hm : m < s) (h : C.SplitInv U A B m) : C.SplitInv U A B (m + 1)

theorem Algebraic.Threshold.Program.splitInv_all {n s : ℕ} (C : Program n s) {U A B : Finset (Fin n)} (hA : A ⊆ U) (hB : B ⊆ Uᶜ) (hsplit : ∀ (j : Fin s), C.support j ⊆ U ∨ C.support j ⊆ Uᶜ) (m : ℕ) : m ≤ s → C.SplitInv U A B m

theorem Algebraic.Threshold.Program.exists_rectangle_of_split_internal {n s : ℕ} (C : Program n s) {f : Cslib.BooleanFunction n} (hC : C.Computes f) (U A B : Finset (Fin n)) (hA : A ⊆ U) (hB : B ⊆ Uᶜ) (hsplit : ∀ (j : Fin s), C.support j ⊆ U ∨ C.support j ⊆ Uᶜ) : ∃ (P : Finset (↥U → Bool)) (Q : Finset (↥Uᶜ → Bool)) (b : Bool), (∀ p ∈ P, ∀ q ∈ Q, f (Cutwidth.glue U p q) = b) ∧ 2 ^ (U.card - A.card) ≤ P.card * 2 ^ {j : Fin s | C.support j ⊆ U ∧ ¬C.support j ⊆ A}.card ∧ 2 ^ (Uᶜ.card - B.card) ≤ Q.card * 2 ^ {j : Fin s | C.support j ⊆ Uᶜ ∧ ¬C.support j ⊆ B}.card

The split lemma. If every gate of C reads inputs from U only or from Uᶜ only, then for all A ⊆ U and B ⊆ Uᶜ there is a rectangle P × Q on which f is constant, with 2 ^ (|U| - |A|) ≤ |P| · 2 ^ #{j : support j ⊆ U, support j ⊄ A} and 2 ^ (|Uᶜ| - |B|) ≤ |Q| · 2 ^ #{j : support j ⊆ Uᶜ, support j ⊄ B}.