Direction-menu capacity bounds for weighted threshold circuits

Partition the input-reading gates of a weighted threshold program into d directions (dir : Fin g → Fin d), so that each input-reading gate gate has input weight vector scale gate • w (dir gate). Unlike DirectionRuns, gates of different directions may be arbitrarily interleaved in the topological order.

For each gate, its syntactic bias menu (biasMenu p gate) is the finite set of all internal sums ∑ j, gateWeight p gate j * (u j).toNat over Boolean valuations u : Fin g → Bool. Precomputing the comparison table (gate, β) ↦ decide (threshold ≤ scale gate * (w a · x) + β) for all input-reading gates in direction a and all β ∈ biasMenu p gate costs a single one-dimensional scalar block with at most T_a = ∑_{gate ∈ directionGates p dir a} |biasMenu p gate| changes (changesAtMost_trueMenuTable). Once the table for direction a is precomputed, every gate in direction a becomes a zero-change (oneDim 0) lookup from its predecessor gate values.

Choosing for each direction a the cheaper of precomputing its menu table (max 1 (4 * T_a)) or evaluating its q_a gates individually (4 ^ q_a) yields the direction-menu lower bound (two_pow_lt_of_directionMenus, Theorem 7.3 of Threshold Circuits as Decision Trees and Finite-State Programs), together with its corollaries for bounded internal fan-in (two_pow_lt_of_directionMenus_fanIn, Corollary 7.4) and bounded integer internal weights (two_pow_lt_of_directionMenus_intWeight, two_pow_lt_of_direction_intWeight).

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.gateSupport: earlier gates with nonzero internal weight into a gate.
• Cslib.Circuits.Boolean.WeightedThreshold.biasMenu: syntactic menu of attainable internal bias offsets at a gate.
• Cslib.Circuits.Boolean.WeightedThreshold.directionGates: input-reading gates assigned to a direction a : Fin d.
• Cslib.Circuits.Boolean.WeightedThreshold.directionMenuSum: sum of bias-menu cardinalities over directionGates p dir a.
• Cslib.Circuits.Boolean.WeightedThreshold.menuBlockDecomposition: the (d + g)-block decomposition precomputing menu tables for a chosen subset of directions.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_two_pow_gateSupport: bounded internal fan-in k bounds |biasMenu p gate| by 2 ^ k.
• Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_one_add_sum_natAbs, Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_one_add_mul: integer internal weights of magnitude at most W bound |biasMenu p gate| by 1 + gate * W.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_directionMenus, Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_directionMenus: Theorem 7.3 (direction-menu capacity bound).
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_directionMenus_fanIn, Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_directionMenus_fanIn: Corollary 7.4 (bounded internal fan-in).
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_directionMenus_intWeight, Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_directionMenus_intWeight, Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_direction_intWeight: bounded integer internal weights.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Section 7.2] [26]

Internal gate support and syntactic bias menus

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.gateSupport {n g : ℕ} (p : Program signature n g) (gate : Fin g) : Finset (Fin g)

Earlier gates with a nonzero aggregated internal weight into gate.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_gateSupport {n g : ℕ} (p : Program signature n g) (gate prior : Fin g) : prior ∈ gateSupport p gate ↔ gateWeight p gate prior ≠ 0

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateSupport_subset_Iio {n g : ℕ} (p : Program signature n g) (gate prior : Fin g) : prior ∈ gateSupport p gate → prior < gate

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.biasMenu {n g : ℕ} (p : Program signature n g) (gate : Fin g) : Finset ℝ

The syntactic menu of all possible internal gate biases at gate over Boolean valuations of internal gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateBias_mem_biasMenu {n g : ℕ} (p : Program signature n g) (gate : Fin g) (u : Fin g → Bool) : ∑ j : Fin g, gateWeight p gate j * ↑(u j).toNat ∈ biasMenu p gate

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_pos {n g : ℕ} (p : Program signature n g) (gate : Fin g) : 0 < (biasMenu p gate).card

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_two_pow_gateSupport {n g : ℕ} (p : Program signature n g) (gate : Fin g) : (biasMenu p gate).card ≤ 2 ^ (gateSupport p gate).card

If gate reads at most k earlier gates with nonzero weight, its bias menu has size at most 2 ^ k.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_one_add_sum_natAbs {n g : ℕ} (p : Program signature n g) (gate : Fin g) (w : Fin g → ℤ) (hw : ∀ (j : Fin g), gateWeight p gate j = ↑(w j)) : (biasMenu p gate).card ≤ 1 + ∑ j : Fin g, (w j).natAbs

Integer internal weights w bound the bias menu of gate by 1 + ∑ j, |w j|.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_one_add_mul {n g : ℕ} (p : Program signature n g) (gate : Fin g) (W : ℕ) (w : Fin g → ℤ) (hw : ∀ (j : Fin g), gateWeight p gate j = ↑(w j)) (hW : ∀ j < gate, (w j).natAbs ≤ W) : (biasMenu p gate).card ≤ 1 + ↑gate * W

Integer internal weights of magnitude at most W on earlier gates bound |biasMenu p gate| by 1 + gate.val * W.

Direction partition and menu sums

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.directionGates {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) (a : Fin d) : Finset (Fin g)

Input-reading gates assigned to direction a.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_directionGates {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) (a : Fin d) (gate : Fin g) : gate ∈ directionGates p dir a ↔ gate ∈ inputGates p ∧ dir gate = a

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.directionMenuSum {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) (a : Fin d) : ℕ

Total syntactic bias-menu size of input-reading gates in direction a.

theorem Cslib.Circuits.Boolean.WeightedThreshold.sum_card_directionGates {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) : ∑ a : Fin d, (directionGates p dir a).card = (inputGates p).card

theorem Cslib.Circuits.Boolean.WeightedThreshold.directionMenuSum_pos_of_nonempty {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) {a : Fin d} (h : (directionGates p dir a).Nonempty) : 0 < directionMenuSum p dir a

Static menu precomputation and block decomposition

theorem Cslib.Circuits.Boolean.WeightedThreshold.changesAtMost_linear_threshold (θ c β : ℝ) : ChangesAtMost (fun (t : ℝ) => decide (θ ≤ c * t + β)) 1

A linear threshold predicate decide (θ ≤ c * t + β) changes at most once along ℝ.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.WeightedThreshold.MenuTable {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) (a : Fin d) : Type

Type of the precomputed comparison table for direction a.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.trueMenuTable {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) (scale : Fin g → ℝ) (a : Fin d) (t : ℝ) : MenuTable p dir a

The precomputed comparison table for direction a at directional projection t = w a · x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.changesAtMost_trueMenuTable {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) (scale : Fin g → ℝ) (a : Fin d) : ChangesAtMost (trueMenuTable p dir scale a) (directionMenuSum p dir a)

As a function of the scalar t, the menu table for direction a changes at most directionMenuSum p dir a times.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.menuHistory {n g d : ℕ} (p : Program signature n g) (dir : Fin g → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin g → ℝ) (S : Finset (Fin d)) (i : ℕ) (x : Fin n → Bool) : ((a : Fin d) → MenuTable p dir a) × (Fin g → Bool)

Intermediate state of the (d + g)-step menu block decomposition at step i.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.menuBlockDecomposition {n g d : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (dir : Fin g → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin g → ℝ) (hdir : ∀ gate ∈ inputGates p, inputWeight p gate = scale gate • w (dir gate)) (S : Finset (Fin d)) : BlockDecomposition (fun (x : BitString n) => readout (p.eval interpretation x)) (((a : Fin d) → MenuTable p dir a) × (Fin g → Bool))

The (d + g)-block decomposition of p that precomputes menu tables for directions in S and evaluates remaining input-reading gates individually.

theorem Cslib.Circuits.Boolean.WeightedThreshold.cost_menuBlockDecomposition {n g d : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (dir : Fin g → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin g → ℝ) (hdir : ∀ gate ∈ inputGates p, inputWeight p gate = scale gate • w (dir gate)) (S : Finset (Fin d)) : (menuBlockDecomposition p readout dir w scale hdir S).cost = ∏ a : Fin d, if a ∈ S then max 1 (4 * directionMenuSum p dir a) else 4 ^ (directionGates p dir a).card

The capacity cost of menuBlockDecomposition factors across the d directions.

Theorem 7.3 and corollaries

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_directionMenus {n g d : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (dir : Fin g → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin g → ℝ) (hdir : ∀ gate ∈ inputGates p, inputWeight p gate = scale gate • w (dir gate)) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ a : Fin d, min (4 ^ (directionGates p dir a).card) (max 1 (4 * directionMenuSum p dir a))

Theorem 7.3 (Direction-menu lower bound). If the input-reading gates of p are partitioned into d directions (inputWeight p gate = scale gate • w (dir gate)), then every Boolean readout computing a two-sided K-rectangle-free function f satisfies 2 ^ n < 4 * K ^ 2 * ∏ a : Fin d, min (4 ^ q_a) (max 1 (4 * T_a)).

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_directionMenus {n d : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (dir : Fin c.size → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin c.size → ℝ) (hdir : ∀ gate ∈ inputGates c.program, inputWeight c.program gate = scale gate • w (dir gate)) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ a : Fin d, min (4 ^ (directionGates c.program dir a).card) (max 1 (4 * directionMenuSum c.program dir a))

Theorem 7.3 for circuits. Direction-menu lower bound for a single-output circuit whose output wire selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_directionMenus_fanIn {n g d : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (dir : Fin g → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin g → ℝ) (hdir : ∀ gate ∈ inputGates p, inputWeight p gate = scale gate • w (dir gate)) (k : ℕ) (hfanIn : ∀ gate ∈ inputGates p, (gateSupport p gate).card ≤ k) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ a : Fin d, min (4 ^ (directionGates p dir a).card) (max 1 (4 * ((directionGates p dir a).card * 2 ^ k)))

Corollary 7.4 (Bounded predecessor fan-in). If each input-reading gate reads at most k earlier gate outputs with nonzero coefficients, then T_a ≤ q_a * 2 ^ k in every direction.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_directionMenus_fanIn {n d : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (dir : Fin c.size → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin c.size → ℝ) (hdir : ∀ gate ∈ inputGates c.program, inputWeight c.program gate = scale gate • w (dir gate)) (k : ℕ) (hfanIn : ∀ gate ∈ inputGates c.program, (gateSupport c.program gate).card ≤ k) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ a : Fin d, min (4 ^ (directionGates c.program dir a).card) (max 1 (4 * ((directionGates c.program dir a).card * 2 ^ k)))

Corollary 7.4 for circuits. Bounded internal fan-in direction-menu bound for a single-output circuit whose output wire selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_directionMenus_intWeight {n g d : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (dir : Fin g → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin g → ℝ) (hdir : ∀ gate ∈ inputGates p, inputWeight p gate = scale gate • w (dir gate)) (W : ℕ) (w_int : Fin g → Fin g → ℤ) (hw_int : ∀ gate ∈ inputGates p, ∀ (j : Fin g), gateWeight p gate j = ↑(w_int gate j)) (hW : ∀ gate ∈ inputGates p, ∀ j < gate, (w_int gate j).natAbs ≤ W) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ a : Fin d, min (4 ^ (directionGates p dir a).card) (max 1 (4 * ((directionGates p dir a).card * (1 + (g - 1) * W))))

Bounded integer internal weights. If every input-reading gate has integer internal weights of magnitude at most W, then |biasMenu p gate| ≤ 1 + (g - 1) * W, yielding T_a ≤ q_a * (1 + (g - 1) * W).

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_directionMenus_intWeight {n d : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (dir : Fin c.size → Fin d) (w : Fin d → Fin n → ℝ) (scale : Fin c.size → ℝ) (hdir : ∀ gate ∈ inputGates c.program, inputWeight c.program gate = scale gate • w (dir gate)) (W : ℕ) (w_int : Fin c.size → Fin c.size → ℤ) (hw_int : ∀ gate ∈ inputGates c.program, ∀ (j : Fin c.size), gateWeight c.program gate j = ↑(w_int gate j)) (hW : ∀ gate ∈ inputGates c.program, ∀ j < gate, (w_int gate j).natAbs ≤ W) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ a : Fin d, min (4 ^ (directionGates c.program dir a).card) (max 1 (4 * ((directionGates c.program dir a).card * (1 + (c.size - 1) * W))))

Bounded integer internal weights for circuits.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_direction_intWeight {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (w : Fin n → ℝ) (scale : Fin g → ℝ) (hdir : ∀ gate ∈ inputGates p, inputWeight p gate = scale gate • w) (W : ℕ) (w_int : Fin g → Fin g → ℤ) (hw_int : ∀ gate ∈ inputGates p, ∀ (j : Fin g), gateWeight p gate j = ↑(w_int gate j)) (hW : ∀ gate ∈ inputGates p, ∀ j < gate, (w_int gate j).natAbs ≤ W) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * max 1 (4 * ((inputGates p).card * (1 + (g - 1) * W)))

Single-direction bounded integer internal weights. When all input-reading gates share one direction w and have integer internal weights of magnitude at most W, 2 ^ n < 4 * K ^ 2 * max 1 (4 * (|inputGates p| * (1 + (g - 1) * W))).