Residuation–Galois Calculus for Exact Safety Preimages of

Monotone Max–Plus Neural Networks

Nader Taffach1,* Mohammad Al-Shiekh1

1 Department of Mathematics, Idlib University, Idlib, Syria

Received: August 02, 2025 Revised: October 30, 2025 Accepted: December 22, 2025 ⋆ Corresponding author

ABSTRACT

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.

Keywords: Abstract interpretation Galois connection Max–plus algebra Residuation Monotone neural network

Exact robustness certificate Tropical computation

1. INTRODUCTION

Abstract interpretation replaces a concrete semantic domain

by an ordered abstraction connected through a Galois relation

[1, 2, 3, 4]. Neural-network verification has adopted this

principle through interval, zonotope, polyhedral, and linearrelaxation

domains [5, 6, 7, 8, 9, 10]. The resulting bounds are

generally sound but not exact because correlation is discarded

or nonlinear transformers are relaxed. Formal analyses of interval

expressivity, fixpoint abstraction, and domain-theoretic

robustness sharpen this distinction [11, 12, 13].

This paper isolates a class for which exactness is algebraic.

Let F : Rn → Rm be isotone under the product order. For

every box [ℓ,u],

α(F([ℓ,u])) = [F(ℓ),F(u)], (1)

where α is the interval hull. Thus interval analysis loses

no coordinatewise range information. Nonnegative-weight

monotone networks satisfy this hypothesis [14, 15, 16, 17,

18].

A stronger inverse statement becomes available over the max–

plus semiring. For

T(x) =W ⊗x⊕b, (W ⊗x) j = max

(Wji+xi), (2)