Threshold gate activity for inner product and rectangle-free functions

For any coordinate split Fin n ≃ L ⊕ R and nonempty subsets A ⊆ (L → Bool) and B ⊆ (R → Bool), if every monochromatic subrectangle A' × B' of a gate readout has area at most M, then |A| |B| ≤ M A^2, where A is the number of attainable input-reading transcripts (Corollary 3.3). Bounding A by a Hamming ball around zero or any fixed baseline pattern v gives general size-activity bounds for both input-reading gates and all gates.

Specializing to inner product modulo two gives 2 ^ m ≤ A ^ 2 and the exact size-activity inequality 2 ^ m ≤ (∑ j ≤ e, q.choose j) ^ 2 around zero or any fixed baseline v. Here q and e may count only input-reading gates and their maximum activity, or all gates and their maximum activity. The statements include zero-dimensional inputs and arbitrary real weights.

The circuit specializations require the designated output to be a gate.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_card_attainableTranscripts_sq: the general rectangle-density pattern bound (Corollary 3.3).
• Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_sq, Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_inputActivityFrom_sq, Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_gateActivity_sq, Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_gateActivityFrom_sq: general rectangle-density size-activity bounds around zero or a fixed baseline.
• two_pow_le_card_attainableTranscripts_sq_of_hadamardCode: the attained-pattern lower bound.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_sq_of_hadamardCode, two_pow_le_sum_choose_inputActivityFrom_sq_of_hadamardCode: the exact binomial-sum size-activity inequalities on input-reading gates.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_sq_of_circuit_hadamardCode: the same bound for a native single-output circuit.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_gateActivity_sq_of_hadamardCode, two_pow_le_sum_choose_gateActivityFrom_sq_of_hadamardCode: the exact bounds using total gate count and total activity.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Theorem 3.2, Corollary 3.3, and Section 3.1] [26]

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_card_attainableTranscripts_sq {n g : ℕ} {L : Type u_1} {R : Type u_2} {β : Type u_3} (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (A : Finset (L → Bool)) (B : Finset (R → Bool)) (hA : A.Nonempty) (hB : B.Nonempty) (readout : (Fin g → Bool) → β) {M : ℕ} (hM : ∀ A' ⊆ A, ∀ B' ⊆ B, ∀ (z : β), (∀ x ∈ A', ∀ y ∈ B', readout (p.eval interpretation (inputOfSplit split x y)) = z) → A'.card * B'.card ≤ M) : A.card * B.card ≤ M * (attainableTranscripts p).card ^ 2

General rectangle-density pattern bound (Corollary 3.3): if every monochromatic subrectangle of A × B under a fixed gate readout has area at most M, then |A| |B| ≤ M A^2, where A is the number of attainable input-reading transcripts.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_sq {n g : ℕ} {L : Type u_1} {R : Type u_2} {β : Type u_3} (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (A : Finset (L → Bool)) (B : Finset (R → Bool)) (hA : A.Nonempty) (hB : B.Nonempty) (readout : (Fin g → Bool) → β) {M : ℕ} (hM : ∀ A' ⊆ A, ∀ B' ⊆ B, ∀ (z : β), (∀ x ∈ A', ∀ y ∈ B', readout (p.eval interpretation (inputOfSplit split x y)) = z) → A'.card * B'.card ≤ M) : A.card * B.card ≤ M * (∑ j ∈ Finset.range (inputActivity p + 1), (inputGates p).card.choose j) ^ 2

General rectangle-density activity bound (Corollary 3.3) on input-reading gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_inputActivityFrom_sq {n g : ℕ} {L : Type u_1} {R : Type u_2} {β : Type u_3} (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (v : ↥(inputGates p) → Bool) (A : Finset (L → Bool)) (B : Finset (R → Bool)) (hA : A.Nonempty) (hB : B.Nonempty) (readout : (Fin g → Bool) → β) {M : ℕ} (hM : ∀ A' ⊆ A, ∀ B' ⊆ B, ∀ (z : β), (∀ x ∈ A', ∀ y ∈ B', readout (p.eval interpretation (inputOfSplit split x y)) = z) → A'.card * B'.card ≤ M) : A.card * B.card ≤ M * (∑ j ∈ Finset.range (inputActivityFrom p v + 1), (inputGates p).card.choose j) ^ 2

General rectangle-density activity bound on input-reading gates relative to any fixed baseline v.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_gateActivity_sq {n g : ℕ} {L : Type u_1} {R : Type u_2} {β : Type u_3} (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (A : Finset (L → Bool)) (B : Finset (R → Bool)) (hA : A.Nonempty) (hB : B.Nonempty) (readout : (Fin g → Bool) → β) {M : ℕ} (hM : ∀ A' ⊆ A, ∀ B' ⊆ B, ∀ (z : β), (∀ x ∈ A', ∀ y ∈ B', readout (p.eval interpretation (inputOfSplit split x y)) = z) → A'.card * B'.card ≤ M) : A.card * B.card ≤ M * (∑ j ∈ Finset.range (gateActivity p + 1), g.choose j) ^ 2

General rectangle-density activity bound (Corollary 3.3) across all gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_mul_le_mul_sum_choose_gateActivityFrom_sq {n g : ℕ} {L : Type u_1} {R : Type u_2} {β : Type u_3} (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (v : Fin g → Bool) (A : Finset (L → Bool)) (B : Finset (R → Bool)) (hA : A.Nonempty) (hB : B.Nonempty) (readout : (Fin g → Bool) → β) {M : ℕ} (hM : ∀ A' ⊆ A, ∀ B' ⊆ B, ∀ (z : β), (∀ x ∈ A', ∀ y ∈ B', readout (p.eval interpretation (inputOfSplit split x y)) = z) → A'.card * B'.card ≤ M) : A.card * B.card ≤ M * (∑ j ∈ Finset.range (gateActivityFrom p v + 1), g.choose j) ^ 2

General rectangle-density activity bound across all gates relative to any fixed baseline v.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_card_attainableTranscripts_sq_of_hadamardCode {n g : ℕ} {ι : Type u_4} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (attainableTranscripts p).card ^ 2

The square of the number of attainable input-reading transcripts is at least the size of one side's Boolean cube whenever a fixed gate readout computes inner product.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_sq_of_hadamardCode {n g : ℕ} {ι : Type u_4} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (inputActivity p + 1), (inputGates p).card.choose j) ^ 2

Inner product forces the exact binomial sum at the program's input-reading activity to have square at least 2 ^ m, where m is the number of coordinates on either side.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_sq_of_circuit_hadamardCode {n : ℕ} {ι : Type u_4} [Fintype ι] (c : Circuit signature n 1) (split : Fin n ≃ ι ⊕ ι) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (h : ∀ (x y : ι → Bool), c.eval interpretation (inputOfSplit split x y) 0 = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (inputActivity c.program + 1), (inputGates c.program).card.choose j) ^ 2

A native single-output circuit computing inner product obeys the size-activity inequality provided its output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_gateActivity_sq_of_hadamardCode {n g : ℕ} {ι : Type u_4} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (gateActivity p + 1), g.choose j) ^ 2

Inner product forces the binomial sum at total gate activity to have square at least 2 ^ m. All gates are counted, including unused gates and gates without direct inputs.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_gateActivity_sq_of_circuit_hadamardCode {n : ℕ} {ι : Type u_4} [Fintype ι] (c : Circuit signature n 1) (split : Fin n ≃ ι ⊕ ι) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (h : ∀ (x y : ι → Bool), c.eval interpretation (inputOfSplit split x y) 0 = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (gateActivity c.program + 1), c.size.choose j) ^ 2

A native single-output inner-product circuit also obeys the bound using all gates, provided its output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_inputActivityFrom_sq_of_hadamardCode {n g : ℕ} {ι : Type u_4} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (v : ↥(inputGates p) → Bool) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (inputActivityFrom p v + 1), (inputGates p).card.choose j) ^ 2

Inner product forces the binomial sum at the program's shifted-baseline input-reading activity around any fixed baseline v to have square at least 2 ^ m.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_sum_choose_gateActivityFrom_sq_of_hadamardCode {n g : ℕ} {ι : Type u_4} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (v : Fin g → Bool) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (gateActivityFrom p v + 1), g.choose j) ^ 2

Inner product forces the binomial sum at the program's shifted-baseline total gate activity around any fixed baseline v to have square at least 2 ^ m.