Threshold-circuit lower bounds for the explicit family

Algebraic.Cutwidth.Extractor.sourceReductionHardFamily is one uniformly polynomial-time Boolean family: the balanced padding of a flat-source sumset extractor with error 35/72 and sublinear source entropy. Its sumset dispersion makes it two-sided rectangle-free under every split of the coordinates, balanced or not, at a threshold K(n) with log₂ K(n) = o(n) (sourceReductionHardFamily_twoSidedRectangleFree). The capacity bounds of Complexitylib.Algebraic.LowerBound.Threshold then give, for every ε > 0 and all sufficiently large n:

• sourceReductionHardFamily_lt_inputGates (C1): every weighted real threshold program of any depth and fan-out computing the family has more than (1/2 - ε) n input-reading gates; gates reading only other gates are free.
• sourceReductionHardFamily_lt_inputGates_of_direction (C2): if every input weight vector is a multiple of one vector, more than (1 - ε) n input-reading gates.
• sourceReductionHardFamily_lt_inputGates_add_runs (C3): if the gates split into B consecutive runs along single directions, s_in + 2B > (1 - ε) n.
• sourceReductionHardFamily_lt_transitions (C2′): every representation F(⟨w, x⟩) of the family by a function F : ℝ → Bool with T transitions has T > 2 ^ ((1 - ε) n).
• sourceReductionHardFamily_lt_sum_logb (C4): in every activation program computing the family whose input-reading gate j changes at most T j times, the input-reading gates carry more than (1 - ε) n bits log₂ max 1 (4 T j) in total.

For comparison, Roychowdhury, Orlitsky, and Siu (IEEE Trans. Inf. Theory 40(2), 1994) and Gröger and Turán prove that inner product mod 2 needs about n / 4 gates in threshold circuits of unbounded depth, and Kane and Williams (STOC 2016) prove superlinear bounds for depth two and three. The threshold n above inherits the enormous threshold of the explicit family.

theorem Algebraic.Threshold.twoSidedRectangleFree_of_flatSumsetDisperser {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : Cutwidth.FlatSumsetDisperser f K) : TwoSidedRectangleFree f K

A two-sided flat sumset disperser is two-sided rectangle-free at the same threshold.

theorem Algebraic.Threshold.sourceReductionHardFamily_twoSidedRectangleFree : ∀ᶠ (n : ℕ) in Filter.atTop, TwoSidedRectangleFree (Cutwidth.Extractor.sourceReductionHardFamily n) (Cutwidth.Aggregate.familyThreshold n)

The explicit family is two-sided rectangle-free. Eventually, under every split of the coordinates, every rectangle on which sourceReductionHardFamily n is constant has a side with fewer than Aggregate.familyThreshold n elements; the binary logarithm of this threshold is o(n) (Aggregate.familyThreshold_log_isLittleO).

theorem Algebraic.Threshold.sourceReductionHardFamily_lt_inputGates {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : ℕ) (C : Program n s), C.Computes (Cutwidth.Extractor.sourceReductionHardFamily n) → (1 / 2 - ε) * ↑n < ↑C.inputGates.card

C1 for the explicit family. For every ε > 0 and all large n, every weighted real threshold program, of any depth and fan-out, computing sourceReductionHardFamily n has more than (1/2 - ε) n gates with a nonzero input weight vector.

theorem Algebraic.Threshold.sourceReductionHardFamily_lt_inputGates_of_direction {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : ℕ) (C : Program n s) (w : Fin n → ℝ), (∀ (j : Fin s), ∃ (c : ℝ), C.inputWeight j = c • w) → C.Computes (Cutwidth.Extractor.sourceReductionHardFamily n) → (1 - ε) * ↑n < ↑C.inputGates.card

C2 for the explicit family. For every ε > 0 and all large n, every threshold program computing sourceReductionHardFamily n whose input weight vectors are all multiples of one vector has more than (1 - ε) n input-reading gates.

theorem Algebraic.Threshold.sourceReductionHardFamily_lt_inputGates_add_runs {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s B : ℕ) (C : Program n s) (a : C.DirectionRuns B), C.Computes (Cutwidth.Extractor.sourceReductionHardFamily n) → (1 - ε) * ↑n < ↑C.inputGates.card + 2 * ↑B

C3 for the explicit family. For every ε > 0 and all large n, if the gates of a threshold program computing sourceReductionHardFamily n split into B consecutive runs along single directions, then s_in + 2B > (1 - ε) n, where s_in counts the input-reading gates.

theorem Algebraic.Threshold.sourceReductionHardFamily_lt_transitions {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (w : Fin n → ℝ) (F : ℝ → Bool) (T : ℕ), ChangesAtMost F T → (∀ (x : Fin n → Bool), Cutwidth.Extractor.sourceReductionHardFamily n x = F (weightedSum w x)) → 2 ^ ((1 - ε) * ↑n) < ↑T

C2′ for the explicit family. For every ε > 0 and all large n, every representation sourceReductionHardFamily n x = F (⟨w, x⟩) by a function F : ℝ → Bool changing at most T times along the reals has T > 2 ^ ((1 - ε) n).

theorem Algebraic.Threshold.sourceReductionHardFamily_lt_sum_logb {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : ℕ) (C : ActivationProgram n s) (T : Fin s → ℕ), (∀ j ∈ C.inputGates, ChangesAtMost (C.activation j) (T j)) → C.Computes (Cutwidth.Extractor.sourceReductionHardFamily n) → (1 - ε) * ↑n < ∑ j ∈ C.inputGates, Real.logb 2 ↑(max 1 (4 * T j))

C4 for the explicit family. For every ε > 0 and all large n, every activation program computing sourceReductionHardFamily n whose input-reading gate j has an activation changing at most T j times satisfies ∑ⱼ log₂ (max 1 (4 T j)) > (1 - ε) n, the sum ranging over the input-reading gates. A threshold gate contributes 2.