Proof-Carrying PWL Verification for ReLU Networks: Convex-Hull Semantics, Exact \SMT/\MILP Encodings, and Symbolic Certificate Checking

ReLU networks are piecewise-linear (PWL), enabling exact symbolic verification via \SMT(\LRA) or \MILP. However, safety claims in certification pipelines require not only correctness but also \emph{checkable evidence}. We develop a proof-carrying verification core for PWL neural constraints: (i) we formalize ReLU networks as unions of polyhedra indexed by activation patterns; (ii) we present exact \SMT/\MILP encodings and the canonical convex-hull relaxation for each bounded ReLU; and (iii) we introduce a certificate calculus in which bound tightening, stabilization, strengthening, and pruning steps emit explicit algebraic witnesses (LP dual multipliers and Farkas infeasibility certificates). Crucially, these witnesses are \emph{symbolic objects} that admit independent verification in exact arithmetic over $\Q$. We provide a symbolic certificate checker, normalization rules that preserve validity, and a compositional view of region-wise certificates as a global proof artifact for universal safety.