Pointwise Wasserstein verification of neural networks via closed-form bound concretization

Affine-bound verifiers such as CROWN, DeepPoly, and DeepZ certify neural networks against $el{l}_p$ perturbations by producing a valid affine bound A · x + b and minimizing it over the ball through the dual norm $\Vert$$A$$\Vert$_$q$. We show that this last step—the concretization—admits a closed form for Wasserstein balls: the worst case of any valid affine bound over a W1 ball is the budget ε times the maximal edge drop \|$B^T$ $A$\|_$\infty$, the W1-Lipschitz constant of the affine envelope, computed in O(|E|) = O(n) tensor operations on the pixel graph under the L1 ground metric, with no transport-side optimization. The form is exact on the relaxed (signed-measure) ball and is therefore a sound certificate on its own; an optional LP tier, gated by a zero-cost test that never changes a certification decision in our benchmarks, restores exactness on the probability-measure ball. Because the closed form depends only on the envelope, not on the domain it was computed on, every $el{l}_p$ verifier is a ready-made envelope generator; and because the interface consumes validity rather than provenance, even learned envelopes are admitted by a check built from the same closed form, which certifies or abstains but never issues a false certificate. The method yields per-sample certified radii with an exact two-term gap decomposition that localizes all conservatism to the envelope, and the closed form matches explicit LPs to solver tolerance at roughly three orders of magnitude lower concretization cost.