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
TC0 refuter for rational networks with at most
K hidden layers and more than
qK 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
VTC0, 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,
VTC0 verifies locally checkable certificates for the balanced integer-weight maximum network of depth
⌈log2n⌉. 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≤2K. We also give certified rational constructions of polynomial encoding length and depth
O(logn/loglogn). 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.