Claim 20.1: for every n there is a depth-2 graph (widths n+1, 2^n+1, 1, all edges) whose sign class contains every function {±1}^n → {±1}

import Definitions.Def_UnderstandingML_NeuralNetworks

open MeasureTheory

namespace UnderstandingML

/-- **Claim 20.1** (p. 271). For every `n`, there exists a graph `(V, E)` of depth `2`, such
that `H_{V,E,sign}` contains all functions from `{±1}^n` to `{±1}`.
The graph has `|V₀| = n + 1`, `|V₁| = 2^n + 1`, `|V₂| = 1` and all edges between adjacent
layers; `±1` is encoded by `Bool` (`true ↦ 1`). -/
theorem sign_nets_all_boolean (n : ℕ) :
    ∃ G : LayeredGraph, G.depth = 2 ∧ G.width 0 = n + 1 ∧ G.width 1 = 2 ^ n + 1 ∧
      G.width 2 = 1 ∧ G.numEdges = (n + 1) * (2 ^ n + 1) + (2 ^ n + 1) ∧
      ∀ f : (Fin n → Bool) → Bool, ∃ h ∈ signNetClass n G,
        ∀ x : Fin n → Bool, h (fun i ↦ if x i then (1 : ℝ) else -1) = f x := by sorry

end UnderstandingML

• 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).