aspg-40-4464-1792533362 20261020215602 American Scientific Publishing Group admin@americaspg.com American Scientific Publishing Group Pure Mathematics for Theoretical Computer Science PMTCS 2995-3162 2026 6 1 Nader Taffach Department of Mathematics, Idlib University, Idlib, Syria Mohammad Al-Shiekh Department of Mathematics, Idlib University, Idlib, Syria A proof-only calculus is developed for exact set abstraction and backward safety certification of monotone neural operators. A Galois insertion between concrete sets and interval boxes yields the best correct interval transformer. For every coordinatewise monotone map F, this transformer maps [ℓ,u] exactly to [F(ℓ),F(u)]; hence layerwise interval propagation is hull-exact for networks with nonnegative weights and isotone activations. The analysis is sharpened for max–plus layers T(x) =W ⊗x⊕b. Their upper safety preimages are either empty or principal ideals generated by the residualW\y, where (W\y)i = inf j:Wji>−∞(yj−Wji). Reverse residual propagation through a depth-L network computes the greatest input vector satisfying a prescribed upper output bound. Consequently, the largest weighted ℓ∞ radius around a nominal input is obtained in closed form, without optimization, branching, sampling, or relaxation. Soundness, maximality, compositionality, exactness, homogeneous collapse, and target-bound stability are proved. Four open problems concern signed architectures, two-sided class margins, residuated transformer attention, and completeness beyond boxes. 2026 32 39 4464 https://creativecommons.org/licenses/by/4.0/ 10.54216/PMTCS.060105 https://americaspg.com/journal/40/article/4464 https://americaspg.com/storage/articles/manuscripts/01KYFKB0S08P3CQWBVB5HD04BP.pdf