Threshold lower bounds from bounded direct input support

The bounds in this module restrict the number of original input coordinates read by each gate. Internal predecessor fan-in, circuit depth, and real coefficient magnitudes remain unrestricted. High-incidence input coordinates can be fixed before applying a random cut.

If both Boolean fibers are K-rectangle-free with K ≤ 2 ^ k, a program with q input-reading gates and at most d original inputs per gate satisfies, for every natural T, n ≤ (2 * (1 - 2⁻ᵈ) + d / (T + 1)) * q + 2 * k + (T + 1) * √(2 * n). For support at most three, an incidence-graph layout sharpens this to 2 * n < (3 + 6 / (T + 1)) * q + max 3 T * Nat.log 2 (n + q) + 6 * k + 1. The support restriction concerns aggregated coefficients, so repeated wires and cancellation are handled by the existing native circuit semantics.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.inputDegree: the number of input-reading gates that have a nonzero effective coefficient on a given original input.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.sum_inputDegree: incidence double counting.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_fixed_inputs_of_inputSupport_card_le: fixing coordinates of degree above T costs at most d * q / (T + 1) coordinates.
• Cslib.Circuits.Boolean.WeightedThreshold.le_inputGates_of_bounded_incidence: the finite lower bound after fixing an arbitrary set of high-incidence inputs.
• Cslib.Circuits.Boolean.WeightedThreshold.le_inputGates_of_inputSupport_card_le, Cslib.Circuits.Boolean.WeightedThreshold.circuit_le_of_inputSupport_card_le: the finite support bound for programs and circuits.
• Cslib.Circuits.Boolean.WeightedThreshold.two_mul_lt_inputGates_of_inputSupport_card_le_three, Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_mul_lt_of_inputSupport_card_le_three: the stronger finite incidence bound when each gate reads at most three original inputs.

References

The lower-bound refinement combines the existing fixed-coordinate rectangle lemma from [S. Schlesinger, Algebraic circuit formalizations in Complexitylib] [Sch26a] with a random partition of the direct input supports. The support-three refinement uses the existing cycle-rank layout bound on the incidence graph and the hereditary obstruction to two disjoint coordinate sets with large deficits.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.inputDegree {n g : ℕ} (p : Program signature n g) (i : Fin n) : ℕ

The number of gates reading an original input with nonzero effective coefficient.

theorem Cslib.Circuits.Boolean.WeightedThreshold.sum_inputDegree {n g : ℕ} (p : Program signature n g) : ∑ i : Fin n, inputDegree p i = ∑ gate : ↥(inputGates p), (inputSupport p ↑gate).card

Counting direct input incidences either by input or by gate gives the same total.

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_fixed_inputs_of_inputSupport_card_le {n g : ℕ} (p : Program signature n g) {d : ℕ} (hd : ∀ (gate : Fin g), (inputSupport p gate).card ≤ d) (T : ℕ) : ∃ (F : Finset (Fin n)), (∀ i ∉ F, inputDegree p i ≤ T) ∧ (T + 1) * F.card ≤ d * (inputGates p).card

Fixing high-incidence coordinates leaves degree at most T; their number times T + 1 is at most the total direct input incidence bound.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_inputGates_of_bounded_incidence {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K 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) {d : ℕ} (hd : ∀ (gate : Fin g), (inputSupport p gate).card ≤ d) (F : Finset (Fin n)) (D : ℕ) (hD : ∀ i ∉ F, inputDegree p i ≤ D) (hK : K ≤ 2 ^ k) : ↑n ≤ 2 * (1 - (1 / 2) ^ d) * ↑(inputGates p).card + ↑F.card + 2 * ↑k + (↑D + 1) * √(2 * ↑n)

After fixing F, bounded incidence gives a support-sensitive lower bound. Only effective coefficients on original input coordinates are counted.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_inputGates_of_inputSupport_card_le {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K 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) {d : ℕ} (hd : ∀ (gate : Fin g), (inputSupport p gate).card ≤ d) (T : ℕ) (hK : K ≤ 2 ^ k) : ↑n ≤ (2 * (1 - (1 / 2) ^ d) + ↑d / (↑T + 1)) * ↑(inputGates p).card + 2 * ↑k + (↑T + 1) * √(2 * ↑n)

A weighted threshold program whose gates each read at most d original inputs satisfies n ≤ (2 (1 - 2⁻ᵈ) + d / (T + 1)) q + 2 k + (T + 1) √(2 n) for every T, where q is the number of input-reading gates and both output fibers are K-rectangle-free with K ≤ 2^k. There is no restriction on internal predecessor fan-in or real coefficient magnitudes.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_le_of_inputSupport_card_le {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K 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) {d : ℕ} (hd : ∀ (gate : Fin c.size), (inputSupport c.program gate).card ≤ d) (T : ℕ) (hK : K ≤ 2 ^ k) : ↑n ≤ (2 * (1 - (1 / 2) ^ d) + ↑d / (↑T + 1)) * ↑(inputGates c.program).card + 2 * ↑k + (↑T + 1) * √(2 * ↑n)

The support-sensitive bound for a native single-output threshold circuit whose output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_mul_lt_inputGates_of_inputSupport_card_le_three {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K 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) (hsupport : ∀ (gate : Fin g), (inputSupport p gate).card ≤ 3) (T : ℕ) (hK : K ≤ 2 ^ k) : 2 * ↑n < (3 + 6 / (↑T + 1)) * ↑(inputGates p).card + ↑(max 3 T) * ↑(Nat.log 2 (n + (inputGates p).card)) + 6 * ↑k + 1

If every gate reads at most three original inputs, the incidence layout gives 2 n < (3 + 6 / (T + 1)) q + max 3 T * log₂(n + q) + 6 k + 1 for every natural T. Here log₂ is Nat.log 2, q counts input-reading gates, and both fibers are K-rectangle-free with K ≤ 2 ^ k. Internal predecessor fan-in and depth are unrestricted.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_mul_lt_of_inputSupport_card_le_three {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K 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) (hsupport : ∀ (gate : Fin c.size), (inputSupport c.program gate).card ≤ 3) (T : ℕ) (hK : K ≤ 2 ^ k) : 2 * ↑n < (3 + 6 / (↑T + 1)) * ↑(inputGates c.program).card + ↑(max 3 T) * ↑(Nat.log 2 (n + (inputGates c.program).card)) + 6 * ↑k + 1

The incidence lower bound for a native single-output threshold circuit whose output selects a gate, assuming each gate reads at most three original inputs.