Closed-Face Integrality and Exact Conditional Termination for Cone-Monotone Integer Equality Relations

Abstract

This paper gives an exact characterization of conditional termination for a class of nondeterministic homogeneous integer equality relations defined by Bλ = Aλ′ over nonnegative integer coefficient vectors. Under pointedness of the source cone, nonzero source generators and cone-monotone displacement, the paper proves that finite convergence of the predecessor sequence is equivalent to uniform finite mortality and, in turn, to an arithmetic condition on every closed face of the source cone. Each closed face carries a canonical deterministic quotient obtained after removing the directions generated by nondeterministic factorization. Finite convergence occurs exactly when every such quotient is integral over the integers, equivalently when each has an integer characteristic polynomial. The proof combines affine-semigroup conductors, continuation lattices, rational controllability, automatic ascent from nonclosed faces, deep pumping and a finite-tube induction. These ingredients also yield an effective recognition procedure and exact computation of the weakest nontermination precondition. The paper includes quantitative results. Closed-face lattice stabilization is bounded in terms of the index of an integral serial lattice, and the proof yields a computable global upper bound on predecessor convergence. A fixed-dimensional parametric family shows that convergence depth can nevertheless grow exponentially in the binary input size, even when the deterministic quotient is trivial. A recursive worst-case upper envelope in input length is also established. The results extend the known exact conditional-termination landscape beyond octagonal relations and finite-monoid affine systems. The class permits genuinely nondeterministic relations, infinite ambient matrix monoids and arbitrary physical dimension. Exact-arithmetic verification code and computational checks accompany the paper.