The excess bound for threshold programs

Fix a set F of inputs and a family 𝓑 of pairwise disjoint blocks covering the remaining inputs, such that every gate either reads inputs from F only or has its residual support (outside F) inside a single block. Write e_b for the number of gates whose nonempty residual support lies in the block b, and φ_b := |b| - e_b for the excess of the block. If every excess is at most M and the program computes a two-sided K-rectangle-free function with K ≤ 2 ^ k, then n < |F| + s_in + M + 2k.

The proof disconnects the inputs of F (Program.restrictInputs), which turns the residual supports into the supports of a program computing the restriction of f with the inputs of F fixed to false. The blocks then split into two groups of excess at least k each (exists_subset_sum_ge_internal), and the split lemma applied to the union U of one group, with the saturated blocks (φ_b = 0) fixed, yields a rectangle P × Q for the restricted function. Fixing the coordinates of F ⊆ Uᶜ to false on the Q side (fixFalseRight) gives a rectangle for f itself, shrinking Q by a factor of at most 2 ^ |F| (card_le_card_image_fixFalseRight), which the count of Uᶜ absorbs. Both sides then have at least 2 ^ k elements.

theorem Algebraic.Threshold.exists_subset_sum_ge_internal {ι : Type u_1} [DecidableEq ι] (𝓑 : Finset ι) (φ : ι → ℕ) (M k : ℕ) (hφ : ∀ b ∈ 𝓑, φ b ≤ M) (htot : 2 * k + M ≤ ∑ b ∈ 𝓑, φ b) : ∃ 𝒢 ⊆ 𝓑, k ≤ ∑ b ∈ 𝒢, φ b ∧ k ≤ ∑ b ∈ 𝓑 \ 𝒢, φ b

Subset sum. Items of value at most M with total value at least 2k + M split into two groups of value at least k each.

theorem Algebraic.Threshold.le_of_two_pow_le_mul_internal {P g d k K : ℕ} (hP : 2 ^ d ≤ P * 2 ^ g) (hd : k + g ≤ d) (hK : K ≤ 2 ^ k) : K ≤ P

The arithmetic closing step of a split: from 2 ^ d ≤ P · 2 ^ g with k + g ≤ d and K ≤ 2 ^ k, the side P has at least K elements.

theorem Algebraic.Threshold.le_of_two_pow_le_mul_image_internal {Q Q' g d k K m : ℕ} (hQ : 2 ^ d ≤ Q * 2 ^ g) (hQ' : Q ≤ 2 ^ m * Q') (hd : k + (m + g) ≤ d) (hK : K ≤ 2 ^ k) : K ≤ Q'

The closing step when the side Q is first projected onto Q' with fibers of size at most 2 ^ m.

theorem Algebraic.Threshold.sum_eq_sum_filter_add_sum_tsub_add_sum_internal {ι : Type u_1} (𝓗 : Finset ι) (c e : ι → ℕ) : ∑ b ∈ 𝓗, c b = ∑ b ∈ 𝓗 with c b ≤ e b, c b + ∑ b ∈ 𝓗, (c b - e b) + ∑ b ∈ 𝓗 with ¬c b ≤ e b, e b

Splitting a sum of sizes by saturation: the saturated items (c ≤ e) contribute their size, the unsaturated ones their excess c - e plus e.

def Algebraic.Threshold.fixFalse {n : ℕ} (F : Finset (Fin n)) (x : Fin n → Bool) : Fin n → Bool

The input x with the coordinates in F fixed to false.

Equations

• Algebraic.Threshold.fixFalse F x i = if i ∈ F then false else x i

def Algebraic.Threshold.fixFalseRight {n : ℕ} (U F : Finset (Fin n)) (q : ↥Uᶜ → Bool) : ↥Uᶜ → Bool

The second side q of a split with the coordinates in F ⊆ Uᶜ fixed to false.

Equations

• Algebraic.Threshold.fixFalseRight U F q i = if ↑i ∈ F then false else q i

theorem Algebraic.Threshold.fixFalse_glue {n : ℕ} (U F : Finset (Fin n)) (hFU : Disjoint F U) (p : ↥U → Bool) (q : ↥Uᶜ → Bool) : fixFalse F (Cutwidth.glue U p q) = Cutwidth.glue U p (fixFalseRight U F q)

theorem Algebraic.Threshold.card_le_card_image_fixFalseRight {n : ℕ} (U F : Finset (Fin n)) (hFU : Disjoint F U) (Q : Finset (↥Uᶜ → Bool)) : Q.card ≤ 2 ^ F.card * (Finset.image (fixFalseRight U F) Q).card

Fixing the coordinates of F ⊆ Uᶜ to false has fibers of size at most 2 ^ |F|.

noncomputable def Algebraic.Threshold.Program.restrictInputs {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) : Program n s

The program C with the inputs of F disconnected: their weights are set to 0 in every gate. On inputs vanishing on F, it evaluates as C.

Equations

• C.restrictInputs F = { inputWeight := fun (j : Fin s) (i : Fin n) => if i ∈ F then 0 else C.inputWeight j i, gateWeight := C.gateWeight, bias := C.bias, output := C.output }

theorem Algebraic.Threshold.Program.support_restrictInputs {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) (j : Fin s) : (C.restrictInputs F).support j = C.support j \ F

theorem Algebraic.Threshold.Program.weightedSum_restrictInputs {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) (j : Fin s) (x : Fin n → Bool) : weightedSum ((C.restrictInputs F).inputWeight j) x = weightedSum (C.inputWeight j) (fixFalse F x)

theorem Algebraic.Threshold.Program.evalFrom_restrictInputs {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) (fixed : Finset (Fin s)) (η : Fin s → Bool) (z : Fin s → ℝ) : (C.restrictInputs F).evalFrom fixed η z = C.evalFrom fixed η z

theorem Algebraic.Threshold.Program.eval_restrictInputs {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) (x : Fin n → Bool) : (C.restrictInputs F).eval x = C.eval (fixFalse F x)

theorem Algebraic.Threshold.Program.computes_restrictInputs {n s : ℕ} (C : Program n s) {f : Cslib.BooleanFunction n} (hC : C.Computes f) (F : Finset (Fin n)) : (C.restrictInputs F).Computes fun (x : Cslib.BitString n) => f (fixFalse F x)

noncomputable def Algebraic.Threshold.Program.residualGates {n s : ℕ} (C : Program n s) (F b : Finset (Fin n)) : Finset (Fin s)

The gates whose residual support outside F is nonempty and lies in b.

Equations

• C.residualGates F b = {j : Fin s | ¬C.support j ⊆ F ∧ C.support j \ F ⊆ b}

theorem Algebraic.Threshold.Program.mem_residualGates {n s : ℕ} (C : Program n s) (F b : Finset (Fin n)) (j : Fin s) : j ∈ C.residualGates F b ↔ ¬C.support j ⊆ F ∧ C.support j \ F ⊆ b

theorem Algebraic.Threshold.Program.residualGates_subset_inputGates {n s : ℕ} (C : Program n s) (F b : Finset (Fin n)) : C.residualGates F b ⊆ C.inputGates

theorem Algebraic.Threshold.Program.disjoint_residualGates {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) {b b' : Finset (Fin n)} (hbb' : Disjoint b b') : Disjoint (C.residualGates F b) (C.residualGates F b')

theorem Algebraic.Threshold.Program.sum_card_residualGates_le {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) (𝓑 : Finset (Finset (Fin n))) (hdisj : (↑𝓑).PairwiseDisjoint id) : ∑ b ∈ 𝓑, (C.residualGates F b).card ≤ C.inputGates.card

Over pairwise disjoint blocks, the residual gates number at most the input gates.

theorem Algebraic.Threshold.Program.card_filter_le_sum_residualGates {n s : ℕ} (C : Program n s) (F : Finset (Fin n)) (𝓑 𝓗 : Finset (Finset (Fin n))) (hblocks : ∀ (j : Fin s), C.support j ⊆ F ∨ ∃ b ∈ 𝓑, C.support j \ F ⊆ b) (W X : Finset (Fin n)) (hW : ∀ b ∈ 𝓑, ∀ i ∈ b, i ∈ W → b ∈ 𝓗) (hX : ∀ b ∈ 𝓗, b.card ≤ (C.residualGates F b).card → b ⊆ X) : {j : Fin s | (C.restrictInputs F).support j ⊆ W ∧ ¬(C.restrictInputs F).support j ⊆ X}.card ≤ ∑ b ∈ 𝓗 with ¬b.card ≤ (C.residualGates F b).card, (C.residualGates F b).card

The gates of the disconnected program counted on the side W of a split, with the set X fixed, lie in the unsaturated blocks of the group 𝓗 meeting W.

theorem Algebraic.Threshold.TwoSidedRectangleFree.lt_of_blocks_internal {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) (F : Finset (Fin n)) (𝓑 : Finset (Finset (Fin n))) (hdisj : (↑𝓑).PairwiseDisjoint id) (hcover : ∀ i ∉ F, ∃ b ∈ 𝓑, i ∈ b) (hF : ∀ b ∈ 𝓑, Disjoint b F) (hblocks : ∀ (j : Fin s), C.support j ⊆ F ∨ ∃ b ∈ 𝓑, C.support j \ F ⊆ b) (M : ℕ) (hM : ∀ b ∈ 𝓑, b.card ≤ {j : Fin s | ¬C.support j ⊆ F ∧ C.support j \ F ⊆ b}.card + M) {k : ℕ} (hK : K ≤ 2 ^ k) : n < F.card + C.inputGates.card + M + 2 * k

The excess bound. Let F be a set of inputs and 𝓑 a family of pairwise disjoint blocks covering the inputs outside F, such that every gate reads inputs from F only or has its residual support outside F inside a single block. If every block b has excess |b| - e_b ≤ M, where e_b counts the gates with nonempty residual support inside b, and the program computes a two-sided K-rectangle-free function with K ≤ 2 ^ k, then n < |F| + s_in + M + 2k.