The cut theorem for threshold programs

Fix a split of the coordinates into U and its complement, with no assumption on the supports of the gates. Processing the gates in order while maintaining a rectangle P × Q on which every earlier gate is constant, gate m is [α(p) + β(q) + c ≥ 0] on the rectangle, where ⟨w, glue p q⟩ = α(p) + β(q) and c collects the constant contributions of the earlier gates.

• If the support of the gate misses U, then α = 0 and the gate is a function of q alone: keep the larger level set of Q, paying a factor 2 on the Q side (or nothing when the support is empty, since the gate is then constant).

• Symmetrically when the support misses Uᶜ.

• Otherwise take medians μ_P of α on P and μ_Q of β on Q. If μ_P + μ_Q + c ≥ 0, the gate is 1 on {α ≥ μ_P} × {β ≥ μ_Q}; otherwise it is 0 on {α ≤ μ_P} × {β ≤ μ_Q}. Either way both sides keep at least half, paid by the gates touching each side.

• TwoSidedRectangleFree.lt_of_split_internal: for every split U, either |U| < #{j : support j ∩ U ≠ ∅} + k or |Uᶜ| < #{j : support j ∩ Uᶜ ≠ ∅} + k, whenever f is two-sided K-rectangle-free with K ≤ 2 ^ k.

• TwoSidedRectangleFree.le_two_mul_add_internal: n ≤ 2 (s_in + k).

theorem Algebraic.Threshold.exists_median_internal {α : Type u_1} (P : Finset α) (g : α → ℝ) : ∃ (μ : ℝ), P.card ≤ 2 * {p ∈ P | g p ≤ μ}.card ∧ P.card ≤ 2 * {p ∈ P | μ ≤ g p}.card

A median of a real function on a finite set: both weak level sets have at least half of the elements.

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

The number of gates below m whose support meets S.

Equations

• C.touchBelow S m = {j : Fin s | ↑j < m ∧ (C.support j ∩ S).Nonempty}.card

theorem Algebraic.Threshold.Program.touchBelow_succ {n s : ℕ} (C : Program n s) (S : Finset (Fin n)) {m : ℕ} (j₀ : Fin s) (hj₀ : ↑j₀ = m) : C.touchBelow S (m + 1) = C.touchBelow S m + if (C.support j₀ ∩ S).Nonempty then 1 else 0

theorem Algebraic.Threshold.Program.touchBelow_zero {n s : ℕ} (C : Program n s) (S : Finset (Fin n)) : C.touchBelow S 0 = 0

theorem Algebraic.Threshold.Program.touchBelow_top {n s : ℕ} (C : Program n s) (S : Finset (Fin n)) : C.touchBelow S s = {j : Fin s | (C.support j ∩ S).Nonempty}.card

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

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

Equations

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

theorem Algebraic.Threshold.Program.cutInv_zero {n s : ℕ} (C : Program n s) (U : Finset (Fin n)) : C.CutInv U 0

theorem Algebraic.Threshold.Program.cutInv_succ {n s : ℕ} (C : Program n s) (U : Finset (Fin n)) {m : ℕ} (hm : m < s) (h : C.CutInv U m) : C.CutInv U (m + 1)

theorem Algebraic.Threshold.Program.cutInv_all {n s : ℕ} (C : Program n s) (U : Finset (Fin n)) (m : ℕ) : m ≤ s → C.CutInv U m

theorem Algebraic.Threshold.Program.exists_rectangle_of_cut_internal {n s : ℕ} (C : Program n s) {f : Cslib.BooleanFunction n} (hC : C.Computes f) (U : Finset (Fin n)) : ∃ (P : Finset (↥U → Bool)) (Q : Finset (↥Uᶜ → Bool)) (b : Bool), (∀ p ∈ P, ∀ q ∈ Q, f (Cutwidth.glue U p q) = b) ∧ 2 ^ U.card ≤ P.card * 2 ^ {j : Fin s | (C.support j ∩ U).Nonempty}.card ∧ 2 ^ Uᶜ.card ≤ Q.card * 2 ^ {j : Fin s | (C.support j ∩ Uᶜ).Nonempty}.card

The cut lemma. For every split U there is a rectangle P × Q on which f is constant, with 2 ^ |U| ≤ |P| · 2 ^ #{j : support j ∩ U ≠ ∅} and symmetrically for Q.

theorem Algebraic.Threshold.Program.card_filter_touch_le_inputGates {n s : ℕ} (C : Program n s) (S : Finset (Fin n)) : {j : Fin s | (C.support j ∩ S).Nonempty}.card ≤ C.inputGates.card

Gates whose support meets S are input-reading.

theorem Algebraic.Threshold.TwoSidedRectangleFree.lt_of_split_internal {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) (U : Finset (Fin n)) {k : ℕ} (hK : K ≤ 2 ^ k) : U.card < {j : Fin s | (C.support j ∩ U).Nonempty}.card + k ∨ Uᶜ.card < {j : Fin s | (C.support j ∩ Uᶜ).Nonempty}.card + k

The cut theorem. If C computes a two-sided K-rectangle-free function with K ≤ 2 ^ k, then under every split U one side has fewer than k more coordinates than gates touching it.

theorem Algebraic.Threshold.TwoSidedRectangleFree.le_two_mul_add_internal {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) {k : ℕ} (hK : K ≤ 2 ^ k) : n ≤ 2 * (C.inputGates.card + k)

The cut bound. If C computes a two-sided K-rectangle-free function with K ≤ 2 ^ k, then n ≤ 2 (s_in + k).