Theorem 20.2: a sign network whose class contains all functions {0,1}^n → {0,1} has 2^{n/3} ≤ 2|V|, so the minimal size s(n) is exponential in n

Proved

UnderstandingML.sign_net_all_boolean_size

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

expressive-powerlower-boundneural-networksvc-dimension

Theorem 20.2. For every $n$ , let $s(n)$ be the minimal integer such that there exists a graph $(V, E)$ with $|V| = s(n)$ such that the hypothesis class $H_{V,E,\operatorname{sign}}$ contains all the functions from $\{0,1\}^n$ to $\{0,1\}$ . Then, $s(n)$ is exponential in $n$ .

Formally, as the proof gives it ( $2^n \le \operatorname{VCdim} \le 2|E|\log_2(16|E|)$ and $|E| \le |V|^2$ ): every layered graph of depth $\ge 1$ whose sign class contains all functions $\{0,1\}^n \to \{0,1\}$ satisfies $2^{n/3} \le 2|V|$ . (The sigmoid case, stated without proof, is not included.)

Preamble

import Definitions.Def_UnderstandingML_NeuralNetworks

open MeasureTheory

Formal statement

namespace UnderstandingML

/-- **Theorem 20.2** (p. 272). For every `n`, let `s(n)` be the minimal integer such that there
exists a graph `(V, E)` with `|V| = s(n)` such that the hypothesis class `H_{V,E,sign}` contains
all the functions from `{0,1}^n` to `{0,1}`. Then `s(n)` is exponential in `n`.
Explicitly, as the proof gives it (`2^n ≤ VCdim ≤ O(|E| log |E|)` and `|E| ≤ |V|²`): every
such graph has `2^n ≤ 8|V|³`, i.e. `|V| ≥ 2^{n/3}/2`. -/
theorem sign_net_all_boolean_size (n : ℕ) (G : LayeredGraph) (hd : 1 ≤ G.depth)
    (hG : ∀ f : (Fin n → Bool) → Bool, ∃ h ∈ signNetClass n G,
      ∀ x : Fin n → Bool, h (fun i ↦ if x i then (1 : ℝ) else 0) = f x) :
    (2 : ℝ) ^ ((n : ℝ) / 3) ≤ 2 * G.size := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §20.3 p. 272, Theorem 20.2 with its proof

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph