Every CPWL function is a finite sum of hinging hyperplanes (Wang–Sun)

Theorem (Wang–Sun, 2005). Fix an integer $n \geq 1$, and let $f : \mathbb{R}^n \to \mathbb{R}$ be continuous piecewise linear: continuous, and affine on each cell of some finite polyhedral subdivision of $\mathbb{R}^n$. Then there exist a finite $K \geq 1$, signs $s_1, \dots, s_K \in \{-1, +1\}$, index sets $S_1, \dots, S_K$ each of size at most $n+1$, and affine functions $\ell_{k,j} : \mathbb{R}^n \to \mathbb{R}$ for $k \in \{1, \dots, K\}$ and $j \in S_k$, such that

The theorem reduces the exact representation of an arbitrary continuous piecewise linear function to that of a single maximum of $n+1$ affine arguments, which is why depth bounds for ReLU networks reduce to depth bounds for one max gate.

Formalization Note This is a corrected, canonical restatement of an earlier registration of the same theorem (WangSun.Main) whose formal statement embedded the CPWL/IsHinge/IsHH inductive type and definitions directly inline in its own preamble (via an ambient variable {n : ℕ} plus a bare inductive declaration) rather than through the platform's Definitions.Def_CPWL module. That combination caused every proof attempt against it, and against a first corrected restatement that kept the same inline-preamble style, to fail with an identical parser error regardless of content. This restatement imports Definitions.Def_CPWL directly (the same route already used successfully by the sibling WangSun.Main_shared) and otherwise states word-for-word the same theorem.