One-dimensional capacity of threshold circuits of unbounded depth

The model is Program n s: a straight-line program of s weighted threshold gates on n Boolean inputs, with arbitrary real weights (integer weights are a special case), arbitrary depth, and arbitrary fan-in and fan-out. Gate j is 1 exactly when ∑ i, inputWeight j i * x i + ∑_{k < j} gateWeight j k * (gate k) + bias j ≥ 0 (Program.eval_eq). The bounds count only the input-reading gates Program.inputGates, those with a nonzero input weight vector; gates that read only other gates are free.

Let f be two-sided K-rectangle-free (TwoSidedRectangleFree): under every split of the coordinates, every rectangle on which f is constant has a side with fewer than K elements.

Main results

• exists_sorted_group (Lemma 1): sorting a set by a real key and cutting it into G consecutive groups, some group is good for all but a T / G fraction of a family of functions of the key that each change at most T times (ChangesAtMost). Each such function is nonconstant on at most T groups (ChangesAtMost.card_nonconstant_groups_le).
• Program.piecesAtMost_evalFrom, Program.changesAtMost_evalFrom (Lemma 2): a run of threshold gates whose input contributions are λ_j t for one real parameter t has at most 2 ^ r pieces in t, where r counts the gates with λ_j ≠ 0.
• TwoSidedRectangleFree.two_pow_lt_mul_cost (Theorem U, one-dimensional capacity): every BlockDecomposition of f has 2ⁿ < 4 K² · cost, where the cost multiplies 4T over the one-dimensional blocks with T ≥ 1 changes and V over the summary blocks.
• TwoSidedRectangleFree.two_pow_lt_of_directionRuns: Theorem U for threshold programs split into consecutive runs along single directions, with run costs 4 (2 ^ rᵢ - 1).
• TwoSidedRectangleFree.two_pow_lt_four_pow_inputGates, TwoSidedRectangleFree.lt_two_mul_add_two_mul_inputGates (C1): every threshold program computing f has 2ⁿ < 4 K² · 4 ^ s_in; with K ≤ 2 ^ k, n < 2k + 2 + 2 s_in.
• TwoSidedRectangleFree.two_pow_lt_of_direction, TwoSidedRectangleFree.lt_of_direction (C2): if all input weight vectors are multiples of one vector, 2ⁿ < 16 K² · 2 ^ s_in and n < 2k + 4 + s_in.
• TwoSidedRectangleFree.two_pow_lt_of_runs, TwoSidedRectangleFree.lt_of_runs (C3): with B runs along single directions, 2ⁿ < 4 K² · 4 ^ B · 2 ^ s_in and n < 2k + 2 + 2B + s_in.
• TwoSidedRectangleFree.two_pow_lt_of_multilevel, TwoSidedRectangleFree.two_pow_sub_lt_of_multilevel (C2′): if f = F(⟨w, x⟩) for a function F with T transitions, 2ⁿ < 4 K² · max 1 (4T), and T > 2 ^ (n - 2k - 4).
• TwoSidedRectangleFree.two_pow_lt_of_activations (C4, mixed gate costs): in an ActivationProgram whose input-reading gate j has an activation changing at most T j times, 2ⁿ < 4 K² · ∏ⱼ max 1 (4 T j); a threshold gate costs 4, an exact-threshold or interval gate 8, and gates reading only gates are free.
• TwoSidedRectangleFree.lt_of_split (C0, the cut theorem) and TwoSidedRectangleFree.le_two_mul_add: for every set U of inputs, |U| < touch(U) + k or |Uᶜ| < touch(Uᶜ) + k, where touch(S) counts the gates reading some input of S; at a balanced split, n ≤ 2 (s_in + k) (Internal.Cut). A gate pays one bit on every side it reads, which is where the following structured bounds gain.
• TwoSidedRectangleFree.lt_of_support_card_le_two (C5, the component bound): if every gate reads at most two inputs, n < s_in + 2k, twice the gate count of (C1). Split the inputs along the connected components of the gates' input supports (Program.support), so no gate reads both sides, and make each gate constant by halving one side only (Complexitylib.Algebraic.LowerBound.Threshold.Internal.Split and Internal.Components).
• TwoSidedRectangleFree.lt_of_blocks (C6, the excess bound): after fixing any set F of inputs, partition the rest into blocks such that every gate reads inputs of one block outside F; if every block b has |b| ≤ e_b + M, with e_b the gates reading inside b, then n < |F| + s_in + M + 2k (Internal.Excess). (C5) is the case F = ∅, M = 1.

The explicit polynomial-time family sourceReductionHardFamily is two-sided rectangle-free with log₂ K = o(n); the asymptotic bounds for it are in Complexitylib.Algebraic.LowerBound.Threshold.Family.

theorem Algebraic.Threshold.PiecesAtMost.changesAtMost {β : Type u_1} {Φ : ℝ → β} {M : ℕ} (h : PiecesAtMost Φ M) : ChangesAtMost Φ (M - 1)

A function with at most M pieces changes at most M - 1 times.

theorem Algebraic.Threshold.ChangesAtMost.card_nonconstant_groups_le {β : Type u_1} {Ψ : ℝ → β} {T : ℕ} (h : ChangesAtMost Ψ T) {z : ℕ → ℝ} (hz : Monotone z) (L G : ℕ) : {g ∈ Finset.range G | ∃ j < L, ∃ j' < L, Ψ (z (g * L + j)) ≠ Ψ (z (g * L + j'))}.card ≤ T

Each function is nonconstant on few groups. Cut the positions into consecutive groups of L. A function changing at most T times along the nondecreasing sequence z is nonconstant on at most T of the first G groups.

theorem Algebraic.Threshold.exists_sorted_group {β : Type u_1} {ι : Type u_2} {κ : Type u_3} (P : Finset ι) (Q : Finset κ) (α : ι → ℝ) (Ψ : κ → ℝ → β) {T G : ℕ} (hG : 0 < G) (hΨ : ∀ q ∈ Q, ChangesAtMost (Ψ q) T) : ∃ P' ⊆ P, ∃ Qbad ⊆ Q, P.card / G ≤ P'.card ∧ G * Qbad.card ≤ T * Q.card ∧ ∀ q ∈ Q, q ∉ Qbad → ∀ p ∈ P', ∀ p' ∈ P', Ψ q (α p) = Ψ q (α p')

Lemma 1 (sorted groups). Sort P by the real key α and cut it into G consecutive groups of ⌊|P| / G⌋ elements. If every Ψ q changes at most T times, some group P' has the functions p ↦ Ψ q (α p) constant on P' for every q ∈ Q outside a set Qbad with G |Qbad| ≤ T |Q|.

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

Gate semantics. Gate j is 1 exactly when its weighted input sum, plus the weighted values of the earlier gates, plus its bias, is nonnegative.

theorem Algebraic.Threshold.Program.piecesAtMost_evalFrom {n s : ℕ} (C : Program n s) (fixed : Finset (Fin s)) (η : Fin s → Bool) (slope : Fin s → ℝ) : PiecesAtMost (fun (t : ℝ) => C.evalFrom fixed η fun (j : Fin s) => slope j * t) (2 ^ {j : Fin s | j ∉ fixed ∧ slope j ≠ 0}.card)

Lemma 2 (pieces of a run). If every gate outside fixed receives the input contribution slope j * t, and the gates in fixed are set by η, the gate values have at most 2 ^ r pieces as functions of t, where r counts the gates outside fixed with a nonzero slope.

theorem Algebraic.Threshold.Program.changesAtMost_evalFrom {n s : ℕ} (C : Program n s) (fixed : Finset (Fin s)) (η : Fin s → Bool) (slope : Fin s → ℝ) : ChangesAtMost (fun (t : ℝ) => C.evalFrom fixed η fun (j : Fin s) => slope j * t) (2 ^ {j : Fin s | j ∉ fixed ∧ slope j ≠ 0}.card - 1)

Lemma 2, change form. The same run of gates changes at most 2 ^ r - 1 times.

theorem Algebraic.Threshold.ActivationProgram.eval_eq {n s : ℕ} (C : ActivationProgram n s) (x : Fin n → Bool) (j : Fin s) : C.eval x j = C.activation j (weightedSum (C.inputWeight j) x + ∑ k : Fin s, if k < j then C.gateWeight j k * ↑(C.eval x k).toNat else 0)

Gate semantics of activation programs. Gate j applies its activation to its weighted input sum plus the weighted values of the earlier gates.

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_lt_mul_cost {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {H : Type u_2} (D : BlockDecomposition f H) : 2 ^ n < 4 * K ^ 2 * D.cost

Theorem U (one-dimensional capacity). If f is two-sided K-rectangle-free, every block decomposition of f satisfies 2ⁿ < 4 K² · cost: the product of 4T over its one-dimensional blocks with T ≥ 1 changes and of V over its summary blocks is more than 2ⁿ / (4 K²).

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_lt_of_directionRuns {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) {B : ℕ} (R : C.DirectionRuns B) : 2 ^ n < 4 * K ^ 2 * ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost

Theorem U for threshold programs. Split the gates of a threshold program computing f into B consecutive runs along single directions, with rᵢ input-reading gates in run i. Then 2ⁿ < 4 K² · ∏ᵢ cᵢ, where cᵢ = 4 (2 ^ rᵢ - 1) if rᵢ ≥ 1 and cᵢ = 1 otherwise.

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_lt_four_pow_inputGates {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) : 2 ^ n < 4 * K ^ 2 * 4 ^ C.inputGates.card

C1: input-reading gates of threshold circuits. Every weighted threshold program computing a two-sided K-rectangle-free function has 2ⁿ < 4 K² · 4 ^ s_in, where s_in counts the gates with a nonzero input weight vector; gates reading only gates are free.

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

C1, logarithmic form. With K ≤ 2 ^ k, every threshold program computing f has n < 2k + 2 + 2 s_in, that is, more than (n - 2k - 2) / 2 input-reading gates.

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_lt_of_direction {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) (w : Fin n → ℝ) (along : ∀ (j : Fin s), ∃ (c : ℝ), C.inputWeight j = c • w) : 2 ^ n < 16 * K ^ 2 * 2 ^ C.inputGates.card

C2: one direction. If every input weight vector of a threshold program computing f is a real multiple of one vector w, then 2ⁿ < 16 K² · 2 ^ s_in.

theorem Algebraic.Threshold.TwoSidedRectangleFree.lt_of_direction {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {k : ℕ} (hK : K ≤ 2 ^ k) {C : Program n s} (hC : C.Computes f) (w : Fin n → ℝ) (along : ∀ (j : Fin s), ∃ (c : ℝ), C.inputWeight j = c • w) : n < 2 * k + 4 + C.inputGates.card

C2, logarithmic form. With K ≤ 2 ^ k, a threshold program computing f whose input weight vectors are all multiples of one vector has n < 2k + 4 + s_in.

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_lt_of_runs {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) {B : ℕ} (R : C.DirectionRuns B) : 2 ^ n < 4 * K ^ 2 * 4 ^ B * 2 ^ C.inputGates.card

C3: direction runs. If the gates of a threshold program computing f split into B consecutive runs along single directions, then 2ⁿ < 4 K² · 4 ^ B · 2 ^ s_in.

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

C3, logarithmic form. With K ≤ 2 ^ k and B direction runs, n < 2k + 2 + 2B + s_in.

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_lt_of_multilevel {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : Cslib.BitString n), f x = F (weightedSum w x)) : 2 ^ n < 4 * K ^ 2 * max 1 (4 * T)

C2′: multilevel threshold representations. If f x = F (⟨w, x⟩) for a function F changing at most T times, then 2ⁿ < 4 K² · max 1 (4T).

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_sub_lt_of_multilevel {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {k : ℕ} (hK : K ≤ 2 ^ k) (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : Cslib.BitString n), f x = F (weightedSum w x)) (hn : 2 * k + 4 ≤ n) : 2 ^ (n - (2 * k + 4)) < T

C2′, logarithmic form. With K ≤ 2 ^ k and 2k + 4 ≤ n, a multilevel threshold representation f = F(⟨w, x⟩) needs more than 2 ^ (n - 2k - 4) transitions.

theorem Algebraic.Threshold.TwoSidedRectangleFree.two_pow_lt_of_activations {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : ActivationProgram n s} (hC : C.Computes f) (T : Fin s → ℕ) (hT : ∀ j ∈ C.inputGates, ChangesAtMost (C.activation j) (T j)) : 2 ^ n < 4 * K ^ 2 * ∏ j ∈ C.inputGates, max 1 (4 * T j)

C4: mixed gate costs. In an activation program computing f whose input-reading gate j has an activation changing at most T j times, 2ⁿ < 4 K² · ∏ⱼ max 1 (4 T j), the product ranging over the input-reading gates; gates reading only gates are free.

theorem Algebraic.Threshold.TwoSidedRectangleFree.lt_of_split {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {k : ℕ} (hK : K ≤ 2 ^ k) {C : Program n s} (hC : C.Computes f) (U : Finset (Fin n)) : 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 (C0). For every set U of inputs, with no assumption on the gates, |U| < touch(U) + k or |Uᶜ| < touch(Uᶜ) + k, where touch(S) counts the gates whose support meets S. Each gate pays one bit on every side it reads: given the earlier gates, a gate reading one side alone is a function of that side, and a gate reading both is monotone in the two weighted sums, so a quadrant at the medians makes it constant.

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

The sharpened general bound. Every weighted threshold program computing f has n ≤ 2 (s_in + k): the cut theorem at a balanced split. This sharpens (C1), n < 2k + 2 + 2 s_in, by one.

theorem Algebraic.Threshold.TwoSidedRectangleFree.lt_of_support_card_le_two {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {k : ℕ} (hK : K ≤ 2 ^ k) {C : Program n s} (hC : C.Computes f) (h2 : ∀ (j : Fin s), (C.support j).card ≤ 2) : n < C.inputGates.card + 2 * k

The component bound (C5). If every gate reads at most two inputs ((C.support j).card ≤ 2, with C.support j the inputs of nonzero weight in gate j), then n < s_in + 2k whenever K ≤ 2 ^ k: the input-reading gates number more than n - 2k, twice the general bound (C1). The proof splits the inputs along connected components of the gates' input supports, so that no gate reads both sides, and then makes each gate constant by halving one side only.

theorem Algebraic.Threshold.TwoSidedRectangleFree.lt_of_blocks {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {k : ℕ} (hK : K ≤ 2 ^ 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) : n < F.card + C.inputGates.card + M + 2 * k

The excess bound (C6). Fix any set F of inputs and partition the remaining inputs into blocks 𝓑 such that every gate reads, outside F, inputs of a single block. For a block b, let e_b count the gates whose support outside F is nonempty and lies in b; suppose |b| ≤ e_b + M for every block. Then n < |F| + s_in + M + 2k whenever K ≤ 2 ^ k. Taking F = ∅ and the blocks to be the connected components of the input supports recovers (C5), where M = 1; a block with many gates on few inputs has |b| ≤ e_b and costs nothing beyond its inputs.