A depth lower bound for ReLU networks asserts that every sufficiently shallow network fails on some input. What does a proof of such a bound compute? We study this question for exact computation of the maximum of $n$ real inputs, with depth measured by the number of hidden layers. For every separately fixed prime $q$ and depth bound $K$, we give a uniform $\mathsf{TC}^0$ refuter for rational networks with at most $K$ hidden layers and more than $q^K$ inputs, provided that the reduced denominators of their nonbias weights are not divisible by $q$. Biases may be arbitrary rationals. The refuter finds a rational input on which the network fails, and its correctness is provable in $\mathbf{VTC}^0$, the bounded-arithmetic theory of uniform constant-depth threshold computation. The underlying numerical depth lower bound follows from Averkov, Hojny and Merkert (ICLR 2025), extending Haase, Hertrich and Loho (ICLR 2023); our contribution is an internal proof that makes its geometric argument into a feasible refuter. On the construction side, $\mathbf{VTC}^0$ verifies locally checkable certificates for the balanced integer-weight maximum network of depth $\lceil\log_2 n\rceil$. At $q=2$, the construction and refuter meet: for each fixed $K$, the theory verifies that integer-nonbias-weight networks with arbitrary rational biases can compute the maximum with at most $K$ hidden layers exactly when $n\le 2^K$. We also give certified rational constructions of polynomial encoding length and depth $O(\log n/\log\log n)$. These results instantiate a witnessing duality: bounded proofs of certified existence and of refutation correspond, respectively, to threshold-computable constructors and refuters whose guarantees the theory proves.

翻译：暂无翻译