A Witnessing Duality for ReLU Network Depth

A depth lower bound for ReLU networks asserts that every shallower network errs on some input; we ask when a weak theory can prove such a bound so that an error can be computed. For the exact computation of \max(x_1,\ldots,x_n), recent work shows two hidden layers suffice with unrestricted rational weights. By contrast, Haase, Hertrich and Loho (ICLR 2023) proved that integer weights require depth logarithmic in n, and Averkov, Hojny and Merkert (ICLR 2025) extended the bound to nonbias weights whose denominators are powers of a fixed integer not divisible by a prime q. With integer weights the bound is sharp: the classical balanced construction has depth \lceil\log_2 n\rceil. For each fixed q and depth cap K, we prove this known bound in VTC^0, the bounded-arithmetic theory of uniform constant-depth threshold computation, together with a refuter that is itself such a computation and whose correctness the theory proves. Given a network with at most K hidden layers, nonbias weights whose reduced denominators avoid q, arbitrary rational biases and n>q^K inputs, the refuter returns a rational input of polynomial length on which the network errs. The proof makes the obstruction finite: an iterated intersection product of piecewise-linear functions is divisible by q for the network but not for the maximum, so one of finitely many test points exposes the error. By witnessing, provable refutation corresponds to a provably correct refuter, and provable existence of a certified network to a provably correct constructor. On the construction side, we introduce certificates that label each maximum gadget by the inputs it aggregates; with them the theory verifies the balanced construction, which meets the refuter at the sharp threshold n\le2^K, and a rational family of polynomial description length and depth O(\log n/\log\log n) built from known depth-two blocks.