On the Monniaux Problem in Abstract Interpretation

TL;DR

This paper investigates the decidability of the Monniaux Problem in abstract interpretation, proving undecidability for certain program classes and invariants, but identifying decidability in simple linear loops.

Contribution

It establishes the undecidability of the Monniaux Problem for unguarded affine programs with semilinear invariants and shows decidability for simple linear loops.

Findings

Undecidability for unguarded affine programs with semilinear invariants.

Decidability for simple linear loops.

Clarifies boundaries of decidability in abstract interpretation.

Abstract

The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program $P$, a safety (\emph{e.g.}, non-reachability) specification $\varphi$, and an abstract domain of invariants $\mathcal{D}$, does there exist an inductive invariant $I$ in $\mathcal{D}$ guaranteeing that program $P$ meets its specification $\varphi$. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.

Figures

Equations

$$\mathcal{H}=\left\{z\in {\mathbb{C}}^d\mid \sum _{i=1}^d\text{Re}\left(z\overline{u}\right)\succ a\right\},$$

$$\Pi (\mathcal{I},d)=\left\{z\in {\mathbb{C}}^d\mid \exists t\in {\mathbb{C}}^{d^{\prime }},(z,t)\in \mathcal{I}\right\}$$

$$\text{Section}\left(\mathcal{I},t\right)=\left\{z\in {\mathbb{C}}^d\mid (z,t)\in \mathcal{I}\right\},$$

$$A=\frac{1}{2}\left[\begin{array}{cc}1& -2\\ 2& 1\end{array}\right],$$

$$\mathcal{I}=\{x,Ax\}\cup \text{Conv}{\left(\{A^{n}x,n\le 8\}\right)}^{\mathsf{c}}.$$

$$A=\frac{1}{\sqrt{5}}\left[\begin{array}{cc}1& -2\\ 2& 1\end{array}\right].$$

$$A=\left[\begin{array}{cc}{A}^{\prime }& I_2\\ 0& A^{\prime }\end{array}\right],$$

$$A=\left[\begin{array}{cc}{A}^{\prime }& 0\\ 0& -1\end{array}\right],$$

$$A=\left[\begin{array}{cc}{A}^{\prime }& 0\\ 0& -A^{\prime }\end{array}\right],$$

$${\mathcal{I}}_0=\{u\in {\mathbb{R}}^8\mid (u_1,u_2,u_3,u_4)=\pm 7(u_5,u_6,u_7,u_8)\},$$

$$\{u\in {\mathbb{R}}^8\mid (u_3,u_4)=\pm 7(u_7,u_8)\},$$

$$M_i=\left[\begin{array}{ccc}1& \left[u^{(i)}\right]& -\left[v^{(i)}\right]\\ 0& 4^{-n_i}& 0\\ 0& 0& 4^{-m_i}\end{array}\right]$$

$$M_w=\left[\begin{array}{ccc}1& \left[u^{(w)}\right]& -\left[v^{(w)}\right]\\ 0& 4^{-|u^{(w)}|}& 0\\ 0& 0& 4^{-|v^{(w)}|}\end{array}\right],M_w\left[\begin{array}{c}0\\ 1\\ 1\end{array}\right]=\left[\begin{array}{c}\left[u^w\right]-\left[v^w\right]\\ 4^{-|u^w|}\\ 4^{-|v^w|}\end{array}\right].$$

$$\mathcal{I}^{\prime}=\big{\{}(s,c,d):|s|\geq 4(c+d)+4^{-n_{0}-1}\wedge c\geq 0\wedge d\geq 0\big{\}}$$

$$\mathcal{I}^{\prime\prime}=\big{\{}M_{w}x:w\in\{1,\dots,9\}^{*}\wedge|w|\leq n_{0}+1\big{\}}$$

$$s$$

$$=(u_n^{(wi)}-v_n^{(wi)})4^{1-n}+\sum _{j=n+1}^{|wi|}(u_j^{(wi)}-v_j^{(wi)})4^{1-j}$$

$$|s|$$

$$⩾4^{1-n}+4^{-n}$$

$$⩾4(c+d)+4^{-n_0-1}$$

$$|s^{\prime }|$$

$$⩾|s|-d\max (\left[u^{(i)}\right],\left[v^{(i)}\right])$$

$$⩾4(c+d)+4^{-n_0-1}-d\max (\left[u^{(i)}\right],\left[v^{(i)}\right])$$

$$⩾4(c+d)+4^{-n_0-1}-d\frac{8}{3}$$

$$=4(c+d/3)+4^{-n_0-1}$$

$$⩾4(c^{\prime }+d^{\prime })+4^{-n_0-1}$$

$$M_s=\left[\begin{array}{cccc}0& \cdots & 0& I_3\\ I_3& & & \\ & \ddots & & \\ & & I_3& 0\end{array}\right],M_p=\left[\begin{array}{ccc}{M}_1& \cdots & M_9\\ 0& \cdots & 0\\ ⋮& & ⋮\\ 0& \cdots & 0\end{array}\right],z^{\downarrow i}=\left[\begin{array}{c}{0}_{3i}\\ z\\ 0_{24-3i}\end{array}\right].$$

$$\mathcal{J}=\bigcup _{i=0}^8\left\{z^{\downarrow i}:z\in \mathcal{I}\right\}$$

$${\hat{M}}_i=\left[\begin{array}{ccc}{M}_i& & \\ & 1& 2\\ & 0& 1\end{array}\right],M_e=\left[\begin{array}{ccc}{0}_{3\times 3}& & \\ & 1& 0\\ & 0& 1\end{array}\right],M_{-}=\left[\begin{array}{ccc}{I}_3& & \\ & 1& -2\\ & 0& 1\end{array}\right]$$

$${\mathcal{I}}^{\prime }$$

$${\mathcal{I}}^{\prime \prime }$$

$$s=|[u^{(w{\upharpoonright }_k)}]-[v^{(w{\upharpoonright }_k)}]|=4^{-\ell }[t]⩽4^{-\ell }\frac{8}{3}⩽4c<4(c+d).$$

$$\left[\begin{array}{cccc}\lambda & 1& & \\ & \lambda & \ddots & \\ & & \ddots & 1\\ & & & \lambda \end{array}\right]$$

$$(s^2,c^2,d^2,n^2,r^2,k^2,a^2)=(s^1-4(c^1+d^1),s^1-4(c^1+d^1),s^1,n^1,s^1,k^1,a^1)$$

$$M_x(s^2,c^2,d^2,n^2,r^2,k^2,a^2)=(s^2+c^2,c^2,d^2+r^2,n^2,r^2,k^2-1,a^2).$$

Full text

In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.

1 Introduction

Invariants are one of the most fundamental and useful notions in the quantitative sciences, appearing in a wide range of contexts, from gauge theory, dynamical systems, and control theory in physics, mathematics, and engineering to program verification, static analysis, abstract interpretation, and programming language semantics (among others) in computer science. In spite of decades of scientific work and progress, automated invariant synthesis remains a topic of active research, especially in the fields of program analysis and abstract interpretation, and plays a central role in methods and tools seeking to establish correctness properties of computer programs; see, e.g., [20], and particularly Sec. 8 therein.

The focus of the present paper is the Monniaux Problem on the decidability of the existence of separating invariants, which was formulated by David Monniaux in [25, 26] and also raised by him in a series of personal communications with various members of the theoretical computer science community over the past five years or so. There are in fact a multitude of versions of the Monniaux Problem—indeed, it would be more appropriate to speak of a class of problems rather than a single question—but at a high level the formulation below is one of the most general:

Consider a program $P$ operating over some numerical domain (such as the integers or rationals), and assume that $P$ has an underlying finite control-flow graph over the set of nodes $Q=\{q_{1},\ldots,q_{r}\}$. Let us assume that $P$ makes use of $d$ numerical variables, and each transition $q\overset{t}{\longrightarrow}q^{\prime}$ comprises a function $f_{t}:\mathbb{R}^{d}\rightarrow\mathbb{R}^{d}$ as well as a guard $g_{t}\subseteq\mathbb{R}^{d}$. Let $x,y\in\mathbb{Q}^{d}$ be two points in the ambient space. By way of intuition and motivation, we are interested in the reachability problem as to whether, starting in location $q_{1}$ with variables having valuation $x$, it is possible to reach location $q_{r}$ with variables having valuation $y$, by following the available transitions and under the obvious interpretation of the various functions and guards. Unfortunately, in most settings this problem is well-known to be undecidable.

Let $\mathcal{D}\subseteq 2^{\mathbb{R}^{d}}$ be an ‘abstract domain’ for $P$, i.e., a collection of subsets of $\mathbb{R}^{d}$. For example, $\mathcal{D}$ could be the collection of all convex polyhedra in $\mathbb{R}^{d}$, or the collection of all closed semialgebraic sets in $\mathbb{R}^{d}$, etc.

The Monniaux Problem can now be formulated as a decision question: is it possible to adorn each control location $q$ with an element $\mathcal{I}_{q}\in\mathcal{D}$ such that:

$x\in\mathcal{I}_{q_{1}}$; 2. 2.

The collection of $\mathcal{I}_{q}$’s forms an inductive invariant: for each transition $q\overset{t}{\longrightarrow}q^{\prime}$, we have that $f_{t}(\mathcal{I}_{q}\cap g_{t})\subseteq\mathcal{I}_{q^{\prime}}$; and 3. 3.

$y\notin\mathcal{I}_{q_{r}}$.

We call such a collection $\{\mathcal{I}_{q}:q\in Q\}$ a separating inductive invariant for program $P$. (Clearly, the existence of a separating inductive invariant constitutes a proof of non-reachability for $P$ with the given $x$ and $y$.)

Associated with this decision problem, in positive instances one is also potentially interested in the synthesis problem, i.e., the matter of algorithmically producing a suitable separating invariant $\{\mathcal{I}_{q}:q\in Q\}$.111In the remainder of this paper, the term ‘invariant’ shall always refer to the inductive kind.

The Monniaux Problem is therefore parameterised by a number of items, key of which are (i) the abstract domain $\mathcal{D}$ under consideration, and (ii) the kind of functions and guards allowed in transitions.

Our main interest in this paper lies in the decidability of the existence of separating invariants for various instances of the Monniaux Problem. We give below a cursory cross-sectional survey of existing work and results in this direction.

Arguably the earliest positive result in this area is due to Karr, who showed that strongest affine invariants (conjunctions of affine equalities) for affine programs (no guards, and all transition functions are given by affine expressions) could be computed algorithmically [19]. Note that the ability to synthesise strongest (i.e., smallest with respect to set inclusion) invariants immediately entails the decidability of the Monniaux Problem instance, since the existence of some separating invariant is clearly equivalent to whether the strongest invariant is separating. Müller-Olm and Seidl later extended this work on affine programs to include the computation of strongest polynomial invariants of fixed degree [27], and a randomised algorithm for discovering affine relations was proposed by Gulwani and Necula [16]. More recently, Hrushovski et al. showed how to compute a basis for all polynomial relations at every location of a given affine program [16].

The approaches described above all compute invariants consisting exclusively of conjunctions of equality relations. By contrast, an early and highly influential paper by Cousot and Halbwachs considers the domain of convex closed polyhedra [9], for programs having polynomial transition functions and guards. Whilst no decidability results appear in that paper, much further work was devoted to the development of restricted polyhedral domains for which theoretical guarantees could be obtained, leading (among others) to the octagon domain of Miné [24], the octahedron domain of Clarisó and Cortadella [6], and the template polyhedra of Sankaranarayanan et al. [29]. In fact, as observed by Monniaux [26], if one considers a domain of convex polyhedra having a uniformly bounded number of faces (therefore subsuming in particular the domains just described), then for any class of programs with polynomial transition relations and guards, the existence of separating invariants becomes decidable, as the problem can equivalently be phrased in the first-order theory of the reals.

One of the central motivating questions for the Monniaux Problem is whether one can always compute separating invariants for the full domain of polyhedra. Unfortunately, on this matter very little is known at present. In recent work, Monniaux showed undecidability for the domain of convex polyhedra and the class of programs having affine transition functions and polynomial guards [26]. One of the main results of the present paper is to show undecidability for the domain of semilinear sets222A semilinear set consists of a finite union of polyhedra, or equivalently is defined as the solution set of a Boolean combination of linear inequalities. and the class of affine programs (without any guards)—in fact, affine programs with only a single control location and two transitions:

Theorem 1.1

Let $A,B\in\mathbb{Q}^{d\times d}$ be two rational square matrices of dimension $d$, and let $x,y\in\mathbb{Q}^{d}$ be two points in $\mathbb{Q}^{d}$. Then the existence of a semilinear set $\mathcal{I}\subseteq\mathbb{R}^{d}$ having the following properties:

$x\in\mathcal{I}$; 2. 2.

$A\mathcal{I}\subseteq\mathcal{I}$* and $B\mathcal{I}\subseteq\mathcal{I}$; and* 3. 3.

$y\notin\mathcal{I}$**

is an undecidable problem.

Remark 1

It is worth pointing out that the theorem remains valid even for sufficiently large fixed $d$ (our proof shows undecidability for $d=336$, but this value could undoubtedly be improved). If moreover one requires $\mathcal{I}$ to be topologically closed, one can lower $d$ to having fixed value $27$ (which again is unlikely to be optimal). Finally, an examination of the proof reveals that the theorem also holds for the domain of semialgebraic sets, and in fact for any domain of o-minimal sets in the sense of [1]. The proof also carries through whether one considers the domain of semilinear sets having rational, algebraic, or real coordinates.

Although the above is a negative (undecidability) result, it should be viewed in a positive light; as Monniaux writes in [26], “We started this work hoping to vindicate forty years of research on heuristics by showing that the existence of polyhedral inductive separating invariants in a system with transitions in linear arithmetic (integer or rational) is undecidable.” Theorem 1.1 shows that, at least as regards non-convex invariants, the development and use of heuristics is indeed vindicated and will continue to remain essential. Related questions of completeness of given abstraction scheme have also been examined by Giaccobazzi et al. in [14, 13].

It is important to note that our undecidability result requires at least two transitions. In fact, much research work has been expended on the class of simple affine loops, i.e., one-location programs equipped with a single self-transition. In terms of invariants, Fijalkow et al. establish in [10, 11] the decidability of the existence of semialgebraic separating invariants, and specifically state the question of the existence of separating semilinear invariants as an open problem. Almagor et al. extend this line of work in [1] to more complex targets (in lieu of the point $y$) and richer classes of invariants. The second main result of the present paper is to settle the open question of [10, 11] in the affirmative:

Theorem 1.2

Let $A\in\mathbb{Q}^{d\times d}$ be a rational square matrix of dimension $d$, and let $x,y\in\mathbb{Q}^{d}$ be two points in $\mathbb{Q}^{d}$. It is decidable whether there exists a closed semilinear set $\mathcal{I}\subseteq\mathbb{R}^{d}$ having algebraic coordinates such that:

$x\in\mathcal{I}$; 2. 2.

$A\mathcal{I}\subseteq\mathcal{I}$; and 3. 3.

$y\notin\mathcal{I}$.

Remark 2

The proof shows that, in fixed dimension $d$, the decision procedure runs in polynomial time. It is worth noting that one also has decidability if $A$, $x$, and $y$ are taken to have real-algebraic (rather than rational) entries.

Let us conclude this section by briefly commenting on the important issue of convexity. At its inception, abstract interpretation had a marked preference for domains of convex invariants, of which the interval domain, the octagon domain, and of course the domain of convex polyhedra are prime examples. Convexity confers several distinct advantages, including simplicity of representation, algorithmic tractability and scalability, ease of implementation, and better termination heuristics (such as the use of widening). The central drawback of convexity, on the other hand, is its poor expressive power. This has been noted time and again: “convex polyhedra […] are insufficient for expressing certain invariants, and what is often needed is a disjunction of convex polyhedra.” [2]; “the ability to express non-convex properties is sometimes required in order to achieve a precise analysis of some numerical properties” [12]. Abstract interpretation can accommodate non-convexity either by introducing disjunctions (see, e.g., [2] and references therein), or via the development of special-purpose domains of non-convex invariants such as donut domains [12]. The technology, data structures, algorithms, and heuristics supporting the use of disjunctions in the leading abstract-interpretation tool Astrée are presented in great detail in [8]. In the world of software verification, where predicate abstraction is the dominant paradigm, disjunctions—and hence non-convexity—are nowadays native features of the landscape.

It is important to note that the two main results presented in this paper, Theorems 1.1 and 1.2, have only been proven for families of invariants that are not necessarily convex. The Monniaux Problem restricted to families of convex invariants remains open and challenging.

2 Preliminaries

2.1 Complex and algebraic numbers

The set of complex numbers is $\mathbb{C}$, and for a complex number $z$ its modulus is $|z|$, its real part is $\text{Re}\left(z\right)$ and its imaginary part is $\text{Im}\left(z\right)$.

Let $\mathbb{C}^{*}$ denote the set of non-zero complex numbers. We write $S^{1}$ for the complex unit circle, i.e. the set of complex numbers of modulus $1$. We let $\mathbb{U}$ denote the set of roots of unity, i.e. complex numbers $z\in S^{1}$ such that $z^{n}=1$ for some $n\in\mathbb{N}$.

When working in $\mathbb{C}^{d}$, the norm of a vector $z$ is $||z||$, defined as the maximum of the moduli of each complex number $z_{i}$ for $i$ in $\left\{1,\ldots,d\right\}$. For $\varepsilon>0$ and $z$ in $\mathbb{C}^{d}$, we write $B(z,\varepsilon)$ for the open ball centered in $z$ of radius $\varepsilon$. The topological closure of a set $\mathcal{I}\subseteq\mathbb{C}^{d}$ is $\overline{\mathcal{I}}$, its interior ${\kern 0.0pt\mathcal{I}}^{\mathrm{o}}$, and its frontier $\partial{\mathcal{I}}$, defined as $\overline{\mathcal{I}}\cap\overline{\mathbb{C}^{d}\setminus\mathcal{I}}$.

We will mostly work in the field $\mathbb{A}\subseteq\mathbb{C}$ of algebraic numbers, that is, roots of polynomials with coefficients in $\mathbb{Z}$. It is possible to represent and manipulate algebraic numbers effectively, by storing their minimal polynomial and a sufficiently precise numerical approximation. An excellent reference in computational algebraic number theory is [7]. All standard algebraic operations such as sums, products, root-finding of polynomials, or computing Jordan normal forms of matrices with algebraic entries can be performed effectively.

2.2 Semilinear sets

We now define semilinear sets in $\mathbb{C}^{d}$, by identifying $\mathbb{C}^{d}$ with $\mathbb{R}^{2d}$. A set $\mathcal{I}\subseteq\mathbb{R}^{2d}$ is semilinear if it is the set of real solutions of some finite Boolean combination of linear inequalities with algebraic coefficients. We give an equivalent definition now using half-spaces and polyhedra. A half-space $\mathcal{H}$ is a subset of $\mathbb{C}^{d}$ of the form

[TABLE]

for some $u$ in $\mathbb{A}^{d}$, $a$ in $\mathbb{A}\cap\mathbb{R}$ and \mbox{\succ}\in\left\{\geq,>\right\}. A polyhedron is a finite intersection of half-spaces, and a semilinear set a finite union of polyhedra.

We recall some well known facts about semilinear sets which will be useful for our purposes.

Lemma 1 (Projections of Semilinear Sets)

Let $\mathcal{I}$ be a semilinear set in $\mathbb{C}^{d+d^{\prime}}$. Then the projection of $\mathcal{I}$ on the first $d$ coordinates, defined by

[TABLE]

is a semilinear set.

Lemma 2 (Sections of Semilinear Sets)

Let $\mathcal{I}$ be a semilinear set in $\mathbb{C}^{d+d^{\prime}}$ and $t$ in $\mathbb{C}^{d^{\prime}}$. Then the section of $\mathcal{I}$ along $t$, defined by

[TABLE]

is a semilinear set.

Furthermore, there exists a bound $B$ in $\mathbb{R}$ such that for all $t$ in $\mathbb{C}^{d^{\prime}}$ of norm at most $1$, if $\text{Section}\left(\mathcal{I},t\right)$ is non-empty, then it contains some $z$ in $\mathbb{C}^{d}$ of norm at most $B$.

For the reader’s intuitions, note that the last part of this lemma does not hold for more complicated sets. For instance, consider the hyperbola defined by $\mathcal{I}=\left\{(x,y)\in\mathbb{R}^{2}\mid xy=1\right\}$. Choosing a small $x$ forces to choose a large $y$, hence there exist no bound $B$ as stated in the lemma for $\mathcal{I}$.

The dimension of a set $X$ of $\mathbb{R}^{d}$ is the minimal $k$ in $\mathbb{N}$ such that $X$ is included in a finite union of affine subspaces of dimension at most $k$.

Lemma 3 (Dimension of Semilinear Sets)

Let $\mathcal{I}$ be a semilinear set in $\mathbb{R}^{d}$. If ${\kern 0.0pt\mathcal{I}}^{\mathrm{o}}=\emptyset$, then $\mathcal{I}$ has dimension at most $d-1$.

3 Main results overview

We are interested in instances of the Monniaux Problem in which there are no guards, all transitions are affine (or equivalently linear, since affine transitions can be made linear by increasing the dimension of the ambient space by 1), and invariants are semilinear. This gives rise to the semilinear invariant problem, where an instance is given by a set of square matrices $A_{1},\dots,A_{k}\in\mathbb{A}^{d\times d}$ and two points $x,y\in\mathbb{A}^{d}$. A semilinear set $\mathcal{I}\subseteq\mathbb{C}^{d}$ is a separating invariant if

$x\in\mathcal{I}$, 2. 2.

$A_{i}\mathcal{I}\subseteq\mathcal{I}$ for all $i\leq k$, 3. 3.

$y\notin\mathcal{I}$.

The semilinear invariant problem asks whether such an invariant exists.

We need to introduce some terminology. The triple $((A_{i})_{i\leq k},x,y)$ is a reach instance if there exists a matrix $M$ belonging to the semigroup generated by $(A_{i})_{i\leq k}$ such that $Mx=y$, and otherwise it is a non-reach instance. Clearly a separating invariant can only exist for non-reach instances. An instance for $k=1$ is called an Orbit instance.

3.1 Undecidability for several matrices

Our first result is the undecidability of the semilinear invariant problem. We start by showing it is undecidable in fixed dimension, with a fixed number of matrices and requiring that the invariant be closed. We defer the proofs until Section 4.

Theorem 3.1

The semilinear invariant problem is undecidable for 9 matrices of dimension 3 and closed invariants.

In establishing the above, we used many matrices of small dimension. One could instead use only two matrices, but increasing the dimension to 27.

Theorem 3.2

The semilinear invariant problem is undecidable for 2 matrices of dimension 27 and closed invariants.

In the above results, it can happen that the target belongs to the closure of the set of reachable points. We now show that we can ignore those “non-robust” systems and maintain undecidability.

Theorem 3.3

The semilinear invariant problem is undecidable for “robust” instances, i.e. instances in which the target point does not belong to the closure of the set of reachable points.

The proof of the above result does not require that the invariants be closed. We can therefore establish Theorem 1.1 by making use of the same construction as in the proof of Theorem 3.2 to encode all the matrices of Theorem 3.3 into only two distinct matrices.

3.2 Decidability for simple linear loops

In this section, we are only concerned with Orbit instances. Since it is possible to decide (in polynomial time) whether an Orbit instance is reach or non-reach [17, 18], we can always assume that we are given a non-reach instance. All decidability results are only concerned with closed invariants, this is crucial in several proofs.

Theorem 3.4

There is an algorithm that decides whether an Orbit instance admits a closed semilinear invariant. Furthermore, it runs in polynomial time assuming the dimension d is fixed.

We now comment a few instructive examples to illustrate the different cases that arise. The proof of Theorem 3.4 is postponed to Section 5.

Example 1

Consider the Orbit instance $\ell=(A,x,y)$ in dimension $2$ where

[TABLE]

$x=(1,0)$ and $y=(3,3)$. The orbit is depicted on Figure 1. Here, $A$ is a counterclockwise rotation around the origin with an expanding scaling factor. A suitable semilinear invariant can be constructed by taking the complement of the convex hull of a large enough number of points of the orbit, and adding the missing points. In this example, we can take

[TABLE]

Constructing an invariant of this form will often be possible, for instance when $A$ has an eigenvalue of modulus $>1$. A similar (yet more involved) construction gives the same result when $A$ has an eigenvalue of modulus $<1$. The case in which all eigenvalues have modulus 1 is more involved. Broadly speaking, invariant properties in such cases are often better described by sets involving equations or inequalities of higher degree [10], which is why interesting semilinear invariants do not exist in many instances. However, delineating exactly which instances admit separating semilinear invariants is challenging, and is our main technical contribution on this front. The following few examples illustrate some of the phenomena that occur.

Example 2

Remove the expanding factor from the previous instance, that is, put instead

[TABLE]

Now $A$ being a rotation of an irrational angle, the orbit of $x$ is dense in the circle of radius 1. It is quite easy to prove that no semilinear invariant exists (except for the whole space $\mathbb{R}^{2}$) for this instance, whatever the value of $y$. This gives a first instance of non-existence of a semilinear invariants. Many such examples exist, and we shall now supply a more subtle one. Note that simple invariants do exist, such as the unit circle, which is a semialgebraic set but not a semilinear one.

Example 3

Consider $\ell=(A,x,y)$ in dimension $4$ with

[TABLE]

where $A^{\prime}$ is the matrix from Example 2, $x=(0,0,1,0)$ and $y$ is arbitrary. When repeatedly applying $A$ to $x$, the last two coordinates describe a circle of radius 1 as in the previous example. However, the first two coordinates diverge: at each step, they are rotated and the last two coordinates are added. In this instance, no semilinear invariant exists (except again for the whole space $\mathbb{R}^{4}$), however proving this is somewhat involved. Note however once more that a semialgebraic invariant may easily be constructed.

In examples 2 and 3, no non-trivial semilinear invariant exist, or equivalently any semilinear invariant must contain $\mathcal{I}_{0}$, where $\mathcal{I}_{0}$ is the whole space. In all instances for which constructing an invariant is not necessarily immediate (as is the case in Example 1), we will provide a minimal invariant, that is, a semilinear $\mathcal{I}_{0}$ with the property that any semilinear invariant will have to contain $\mathcal{I}_{0}$. In such cases there exists a semilinear invariant (namely $\mathcal{I}_{0}$) if and only if $y\notin\mathcal{I}_{0}$. We conclude with two examples having such minimal semilinear invariants.

Example 4

Consider $\ell=(A,x,y)$ in dimension $3$ with

[TABLE]

where $A^{\prime}$ is the matrix of Example 2, a $2$-dimensional rotation by an angle which is not a rational multiple of $2\pi$ and $x=(1,0,1)$. As we iterate matrix $A$, the two first coordinates describe a circle, and the third coordinate alternates between $1$ and $-1$: the orbit is dense in the union of two parallel circles. Yet the minimal semilinear invariant comprises the union of the two planes containing these circles.

Example 5

Consider $\ell=(A,x,y)$ in dimension $8$ with

[TABLE]

where $A^{\prime}$ is the matrix from Example 3. This can be seen as two instances of Example 3 running in parallel. Let $x=(0,0,1,0,0,0,-7,0)$, and note that both blocks of $x$ are initially related by a multiplicative factor, namely $-7(x_{1},x_{2},x_{3},x_{4})=(x_{5},x_{6},x_{7},x_{8})$. Moreover, as the first block is multiplied by the matrix $A^{\prime}$ while the second one is multiplied by $-A^{\prime}$, the multiplicative factor relating the two blocks alernates between $7$ and $-7$. Thus, the minimal semilinear invariant in this setting is

[TABLE]

which has dimension 4. If however, we had $x=(0,0,1,0,1,0,-7,0)$, then the minimal semilinear invariant would be

[TABLE]

which has dimension 6. Roughly speaking, no semilinear relation holds between $(u_{1},u_{2})$ and $(u_{5},u_{6})$.

4 Undecidability proofs

4.1 Proof of Theorem 3.1

We reduce an instance of the $\omega$-PCP problem defined as follows: given nine pairs of non-empty words $\{(u^{(1)},v^{(1)}),\dots,(u^{(9)},v^{(9)})\}$ on alphabet $\{0,2\}$, does there exist an infinite word $w=w_{1}w_{2}\dots$ on alphabet $\{1,\dots,9\}$ such that $u^{(w_{1})}u^{(w_{2})}\dots=v^{(w_{1})}v^{(w_{2})}\dots$ . This problem is known to be undecidable [15].

In order to simplify future notations, given a finite or infinite word $w$, we denote $|w|$ the length of the word $w$ and given an integer $i\leq|w|$, we write $w_{i}$ for the $i$’th letter of $w$. Given a finite or infinite word $w$ on alphabet $\{1,\dots,9\}$ we denote $u^{(w)}$ and $v^{(w)}$ the words on the alphabet $\{0,2\}$ such that $u^{(w)}=u^{(w_{1})}u^{(w_{2})}\dots$ and $v^{(w)}=v^{(w_{1})}v^{(w_{2})}\dots$. Given a (finite or infinite) word $w$ on the alphabet $\{0,2\}^{*}$, denote by $\left[w\right]=\sum_{i=1}^{|w|}w_{i}4^{1-i}$ the quaternary encoding of $w$. It is clear that it satisfies $\left[ww^{\prime}\right]=\left[w\right]+4^{-|w|}\left[w^{\prime}\right]$ and that $\left[w\right]\in[0,\tfrac{8}{3}]$.

Let $\{(u^{(1)},v^{(1)}),\dots,(u^{(9)},v^{(9)})\}$ be an instance of the $\omega$-PCP problem. For all $i\leq 9$, for readibility, we denote $|u^{(i)}|={n_{i}}$ and $|v^{(i)}|={m_{i}}$. We build the matrices $M_{1},\dots,M_{9}$ where

[TABLE]

In the following, we write $M_{w}$ for $w=w_{1}\dots w_{k}\in\{1,\dots,9\}^{*}$ the matrix $M=M_{w_{k}}\dots M_{w_{1}}$, which can be checked to satisfy

[TABLE]

Let us show that there exists a separating invariant of $((M_{i})_{i\leq 9},x,y)$ where $x=(0,1,1)$ and $y=(0,0,0)$ iff the $\omega$-PCP instance has no solution.

Let us first assume the $\omega$-PCP instance has a solution $w$. Fix $r\in\mathbb{N}$ and let $w\restriction_{r}=w_{1}\cdots w_{r}$ and $x_{r}=M_{w\restriction_{r}}x$. We have that $x_{r}=(\left[u^{(w\restriction_{r})}\right]-\left[v^{(w\restriction_{r})}\right],$ $4^{-|u^{(w\restriction_{r})}|},4^{-|v^{(w\restriction_{r})}|})$ and since $u^{(w)}=v^{(w)}$, it is clear that $x_{r}\to 0=y$ as $r\to\infty$. Any separating invariant $\mathcal{I}$ must contain this sequence $x_{r}$ since $\mathcal{I}$ contains the initial point and is stable under $(M_{i})_{i\leq 9}$. Moreover, $\mathcal{I}$ is closed so it must contain the limit of the sequence, $(0,0,0)$, which is the target point. Thus $\mathcal{I}$ cannot be a separating invariant. Therefore there is no separating invariant of $((M_{i})_{i\leq 9},(0,1,1),(0,0,0))$.

Now, let us assume the $\omega$-PCP instance has no solution. There exists $n_{0}\in\mathbb{N}$ such that for every infinite word $w$ on alphabet $\{0,\dots,9\}$ there exists $n\leq n_{0}$ such that $u^{(w)}_{n}\neq v^{(w)}_{n}$. Indeed, consider the tree which root is labelled by $(\varepsilon,\varepsilon)$ and, given a node $(u,v)$ of the tree, if for all $n\leq\min(|u|,|v|)$ we have $u_{n}=v_{n}$, then this node has $9$ children: the nodes $(uu^{(i)},vv^{(i)})$ for $i=1\dots 9$. This tree is finitely branching and does not contain any infinite path (which would induce a solution to the $\omega$-PCP instance). Thus, according to König’s lemma, it is finite. We can therefore choose the height of this tree as our $n_{0}$.

We define the invariant $\mathcal{I}=\mathcal{I}^{\prime}\cup\mathcal{I}^{\prime\prime}$ where333This is a semilinear invariant since $|x|\geqslant y$ if and only if $x\geqslant y\vee-x\geqslant y$.

[TABLE]

and

[TABLE]

Let us show that $\mathcal{I}$ is a separating invariant of $((M_{i})_{i\leq 9},(0,1,1),(0,0,0))$. By definition, $\mathcal{I}$ is closed, semilinear, contains $x$ and does not contain $y$. The difficult point is to show stability under $M_{i}$ for $i\leq 9$.

• •

Let $M_{w}x\in\mathcal{I}^{\prime\prime}$, for some $w$: there are two cases. Either $|w|\leqslant n_{0}$, then $|wi|\leqslant n_{0}+1$, therefore $M_{i}M_{w}x=M_{wi}z\in\mathcal{I}^{\prime\prime}$. Otherwise, $M_{i}M_{w}x=M_{wi}x=(s,c,d)$ where $s=\left[u^{(wi)}\right]-\left[v^{(wi)}\right]$, $c=4^{-|u^{(wi)}|}$ and $d=4^{-|v^{(wi)}|}$. But then, there exists $n\leqslant n_{0}$ such that $u^{(wi)}_{n}\neq v^{(wi)}_{n}$. Let $n$ be the smallest such number, then

[TABLE]

since $u^{(wi)}_{j}=v^{(wi)}_{j}$for $j<n$. Thus,

[TABLE]

This shows that $M_{i}(M_{w}x)\in\mathcal{I}^{\prime}\subseteq\mathcal{I}$.

• •

Let $z=(s,c,d)\in\mathcal{I}^{\prime}$, then $|s|\geqslant 4(c+d)+4^{-n_{0}-1}$. Without loss of generality, assume that $d\geqslant c$ (this is completely symmetric in $c$ and $d$). Let $(s^{\prime},c^{\prime},d^{\prime})=M_{i}z$, and we check that then

[TABLE]

since $c^{\prime}=c4^{-|u^{(i)}|}$ and $d^{\prime}=d4^{-|v^{(i)}|}$. This shows that $M_{i}z\in\mathcal{I}^{\prime}\subseteq\mathcal{I}$.

This shows that $\mathcal{I}$ is thus stable and concludes the reduction.

4.2 Proof of Theorem 3.2

We reduce the instances of Theorem 3.1 to $2$ matrices of size $27$. The first matrix $M_{s}$ shifts upwards the position of the values in the point by 3, while the second matrix $M_{p}$ applies one of the matrices of the previous reduction, depending on the position of the values within the matrices, then put the obtained value at the top. In other words, $M_{p}M_{s}^{i-1}$ for $1\leq i\leq 9$ intuitively has the same effect as $M_{i}$ had in the proof of Theorem 3.1. In the following, we reuse the notations and results of the proof of Theorem 3.1.

Define matrices $M_{s}$ and $M_{p}$, where $I_{3}$ is the identity matrix of size $3\times 3$, and for any $z\in\mathbb{R}^{3}$ and $i\in\left\{0,\ldots,8\right\}$, the $i^{th}$ shift $z^{\downarrow i}\in\mathbb{R}^{27}$ of $z$, where $\boldsymbol{0}_{n}\in\mathbb{R}^{n}$ denotes the zero vector of size $n$, as follows:

[TABLE]

It follows that $M_{s}z^{\downarrow i}=z^{\downarrow i+1\bmod 9}$ and $M_{p}z^{\downarrow i}=(M_{i+1}z)^{\downarrow 0}$. Assume that there exists a separating invariant $\mathcal{I}$ for $(M_{1},\ldots,M_{9},x,y)$ and let

[TABLE]

which is a closed semilinear set. Then for any $z^{\downarrow i}\in\mathcal{J}$, we have $M_{s}z^{\downarrow i}=z^{\downarrow i+1\bmod 9}\in\mathcal{I}$ by definition and $M_{p}z^{\downarrow i}=(M_{i}z)^{\downarrow 0}\in\mathcal{J}$ since $M_{i}z\in\mathcal{I}$ by virtue of $z\in\mathcal{I}$ and $\mathcal{I}$ being invariant. Furthermore, $x^{\prime}=x^{\downarrow 0}\in\mathcal{I}$ since $x\in\mathcal{I}$, and $y^{\prime}=y^{\downarrow 0}\notin\mathcal{J}$ for otherwise we would have $y\in\mathcal{I}$. Therefore $\mathcal{J}$ is a separating invariant for $(M_{s},M_{p},x^{\prime},y^{\prime})$.

Assume that there exists a separating invariant $\mathcal{J}$ for $(M_{s},M_{p},x^{\prime},y^{\prime})$ and let $\mathcal{I}=\left\{z:z^{\downarrow 0}\in\mathcal{J}\right\}$ which is a closed semilinear set. Clearly $x\in\mathcal{I}$ since $x^{\prime}=x^{\downarrow 0}\in\mathcal{J}$ and $y\notin\mathcal{I}$ since $y^{\prime}=y^{\downarrow 0}\notin\mathcal{J}$. Let $z\in\mathcal{I}$ and $i\in\left\{1,\ldots,9\right\}$, then $(M_{i}z)^{\downarrow 0}=M_{p}M_{s}^{i-1}z^{\downarrow 0}\in\mathcal{J}$ and since $z^{\downarrow 0}\in\mathcal{J}$ and $\mathcal{J}$ is invariant under $M_{s}$ and $M_{p}$, thus $M_{i}z\in\mathcal{I}$. Therefore $\mathcal{I}$ is a non-reachability invariant for $(M_{1},\ldots,M_{9},x,y)$.

4.3 Proof sketch of Theorem 3.3

We do the proof of Theorem 3.3 twice: first we use linear guards in order to limit the selection of the matrices. The added power of the guards allows for a relatively simple proof. This first proof can be seen as an extended sketch of the second one, in Appendix 0.A, where we remove the guards to obtain the result claimed. We do so by emulating the guards using extra variables.

We reduce from the $\omega$-PCP problem and reuse some of the notations of the proof of Theorem 3.1. Let $\{(u^{(1)},v^{(1)}),\dots,(u^{(9)},v^{(9)})\}$ be an instance of the $\omega$-PCP problem. We build the matrices $\hat{M}_{1},\dots,\hat{M}_{9},M_{e},M_{-}$ where

[TABLE]

and $M_{1},\ldots,M_{9}$ are from the proof of Theorem 3.1. Moreover, when in $(s,c,d,n,a)$, the matrices $\hat{M}_{i}$ and $M_{e}$ can only be selected if the linear guard $|s|<4(c+d)$ holds, and the matrix $M_{-}$ can only be selected if $s=c=d=0$.

Informally, in state $(s,c,d,n,a)$, the subvector $(s,c,d)$ has the same role as before: $s$ contains the difference of the values of the numbers obtained using the $v_{i}$ and $u_{i}$, while $c$ and $d$ are used in order to help compute this value. In the proof of Theorem 3.1, we showed that when the $\omega$-PCP instance had no solution, there existed a value $n_{0}$ such that any pair of words created with the alphabet $(u^{(i)},v^{(i)})$ differed on one of the first $n_{0}$ terms. The variable $n$ is used with the guards in order to detect this value $n_{0}$: if such an $n_{0}$ exists, then at most $n_{0}+1$ matrices $M_{i}$ can be selected before the guard stops holding. Moreover, firing a matrix $M_{i}$ adds 2 to $n$ ensuring that when the guard stops holding, $n$ is smaller or equal to $2(n_{0}+1)$. Conversely, if no such $n_{0}$ exist, then there is a way to select matrices $M_{i}$ such that the guard always holds, allowing the variable $n$ to become an even number as high as one wants. The existence of an upper bound on the value of $n$ is used to build an invariant or to prove that there cannot exist an invariant. Finally, the value $a$ is only here in order to allow for affine modification of the values. It is never modified.

Let $\hat{x}=(x,0,1)$ and $\hat{y}=(y,1,1)$. Note that $\hat{y}$ is not in the adherence of the reachable set as the fourth variable of any reachable point is an even number while $y$’s is an odd one.

Assume the $\omega$-PCP instance does not possess a solution. Then there exists $n_{0}\in\mathbb{N}$ such that any pair of words $(u^{(w)},v^{(w)})$ differs on one of the first $n_{0}$ letters. Define the invariant $\mathcal{I}=\mathcal{I}^{\prime}\cup\mathcal{I}^{\prime\prime}$ where

[TABLE]

This invariant is clearly semilinear, it contains $\hat{x}$ and does not contain $\hat{y}$. If $z=(0,0,0,n,1)\in\mathcal{I}^{\prime\prime}$ then only $M_{-}$ can be triggered due to the guards and $M_{-}z=(0,0,0,n-2,1)\in\mathcal{I}^{\prime\prime}$. Now if $z=(s,c,d,n,a)=\hat{M}_{w}\hat{x}\in\mathcal{I}^{\prime}$ for some $w\in\{1,\dots,9\}^{*}$, then $M_{-}$ cannot be fired as the guard does not hold. If one fires $M_{e}$, by construction of $\mathcal{I}^{\prime}$, $n$ is an even number smaller than $2(n_{0}+1)$, thus $M_{e}z\in\mathcal{I}^{\prime\prime}$. Now in order to fire a matrix $\hat{M}_{i}$, one needs $|s|<4(c+d)$ to hold. We showed in the proof of Theorem 3.1 that, from the initial configuration $x$, after $n_{0}+1$ transitions using one of the matrices $M_{i}$ then $1/4^{n_{0}+1}\leqslant|s|-4(c+d)$. As a consequence, if the guard holds, then $|w|\leqslant n_{0}$ and $\hat{M}_{i}z=\hat{M}_{wi}\hat{x}\in\mathcal{I}^{\prime}$. Therefore, $\mathcal{I}$ is a separating invariant of $(\hat{M}_{1},\dots\hat{M}_{9},M_{e},M_{-},\hat{x},\hat{y})$.

Now assume the $\omega$-PCP possesses a solution $w\in\{1,\dots,9\}^{\omega}$. For $k\in\mathbb{N}$, we denote $w\restriction_{k}$ the prefix of length $k$ of $w$. Let $k\in\mathbb{N}$ and $(s,c,d,n,a)=\hat{M}_{w\restriction_{k}}x$, then $|s|<4(c+d)$. Indeed, assume that $u^{(w\restriction_{k})}$ is longer than $v^{(w\restriction_{k})}$. Then $u^{(w\restriction_{k})}=v^{(w\restriction_{k})}t$ for some word $t\in\left\{0,2\right\}^{*}$ because $u^{w}{(w)}v^{(w)}$. Let $\ell=|u^{(w\restriction_{k})}|$ and recall that $c=4^{-\ell}$, then

[TABLE]

The symmetric case is similar but uses $d$ instead. Therefore the guard is satisfied and $M_{e}\hat{M}_{w\restriction_{k}}\hat{x}=(0,0,0,2k,1)\in\mathcal{I}$ is reachable for all $k\in\mathbb{N}$. Let $\mathcal{I}$ be a semilinear invariant containing the reachability set, then $\mathcal{I}\cap\{(0,0,0,x,1):x\in\mathbb{R}\}$ is semilinear and contains $(0,0,0,2k,1)$ for all $k\in\mathbb{N}$. This implies that it necessarily contains an unbounded interval and there must exists $k_{0}\in\mathbb{N}$ such that $(0,0,0,2k_{0}+1,1)\in\mathcal{I}$. Since $\mathcal{I}$ is stable by the matrix $M_{-}$, $\mathcal{I}$ contains the target $y$. Therefore, $\mathcal{I}$ is not a separating invariant of $((\hat{M}_{1},\dots\hat{M}_{9},M_{e},M_{-}),x,y)$.

5 Decidability proofs

This section is aimed at sketching the main ideas of the proof of Theorem 3.4 while avoiding technicalities and details. We point to the appendix for full proofs. Recall that we only consider closed semilinear invariants.

• •

We first normalize the Orbit instance, which amounts to putting matrix $A$ in Jordan normal form, and eliminating some easy instances. This is described in Section 5.1.

• •

We then eliminate some positive cases in Section 5.2. More precisely, we construct invariants whenever one of the three following conditions is realized:

• –

$A$ has an eigenvalue of modulus $>1$.

• –

$A$ has an eigenvalue of modulus $<1$.

• –

$A$ has a Jordan block of size $\geq 2$ with an eigenvalue that is a root of unity.

• •

We are now left with an instance where all eigenvalues are of modulus 1 and not roots of unity, which is the most involved part of the paper. In this setting, we exhibit the minimal semilinear invariant $\mathcal{I}$ containing $x$. In particular, there exists a semilinear invariant (namely, $\mathcal{I}$) if and only if $y\notin\mathcal{I}$. This part is explained in Section 5.3.

5.1 Normalization

As a first step, recall that every matrix $A$ can be written in the form $A=Q^{-1}JQ$, where $Q$ is invertible and $J$ is in Jordan normal form. The following lemma transfers semilinear invariants through the change-of-basis matrix $Q$.

Lemma 4

Let $\ell=(A,x,y)$ be an Orbit instance, and $Q$ an invertible matrix in $\mathbb{A}^{d\times d}$. Construct the Orbit instance $\ell_{Q}=(QAQ^{-1},Qx,Qy)$. Then $\mathcal{I}$ is a semilinear invariant for $\ell_{Q}$ if, and only if, $Q^{-1}\mathcal{I}$ is a semilinear invariant for $\ell$.

Proof

First of all, $Q^{-1}\mathcal{I}$ is semilinear if, and only if, $\mathcal{I}$ is semilinear. We have:

• •

$QAQ^{-1}\mathcal{I}\subseteq\mathcal{I}$ if, and only if, $AQ^{-1}\mathcal{I}\subseteq Q^{-1}\mathcal{I}$,

• •

$Qx\in\mathcal{I}$ if, and only if, $x\in Q^{-1}\mathcal{I}$,

• •

$Qy\notin\mathcal{I}$, if, and only if, $y\notin Q^{-1}\mathcal{I}$.

This concludes the proof.

Thanks to Lemma 4, we can reduce the problem of the existence of semilinear invariants for Orbit instances to cases in which the matrix is in Jordan normal form, i.e., is a diagonal block matrix, where the blocks (called Jordan blocks) are of the form:

[TABLE]

Note that this transformation can be achieved in polynomial time [3, 4]. Formally, a Jordan block is a matrix $\lambda I+N$ with $\lambda\in\mathbb{C}$, $I$ the identity matrix and $N$ the matrix with $1$’s on the upper diagonal, and [math]’s everywhere else. The number $\lambda$ is an eigenvalue of $A$. We will use notation $\mathcal{J}_{d}(\lambda)$ for the Jordan block of size $d$ with eigenvalue $\lambda$. A Jordan block of dimension one is called diagonal, and $A$ is diagonalisable if, and only if, all Jordan blocks are diagonal.

The $d$ dimensions of the matrix $A$ are indexed by pairs $(J,k)$, where $J$ ranges over the Jordan blocks and $k\in\left\{1,\ldots,d(J)\right\}$ where $d(J)$ is the dimension of the Jordan block $J$. For instance, if the matrix $A$ has two Jordan blocks, $J_{1}$ of dimension $1$ and $J_{2}$ of dimension $2$, then the three dimensions of $A$ are $(J_{1},1)$ (corresponding to the Jordan block $J_{1}$) and $(J_{2},1),(J_{2},2)$ (corresponding to the Jordan block $J_{2}$).

For a point $v$ and a subset $S$ of $\left\{1,\ldots,d\right\}$, let $v_{S}$ be the projection of $v$ on the dimensions in $S$, and extend this notation to matrices. For instance, $v_{J}$ is the point corresponding to the dimensions of the Jordan block $J$, and $v_{J,>k}$ is projected on the coordinates of the Jordan block $J$ whose index is greater than $k$. We write $S^{\mathsf{c}}$ for the coordinates which are not in $S$.

There are a few degenerate cases which we handle now. We say that an Orbit instance $\ell=(A,x,y)$ in Jordan normal form is normalized if:

• •

There is no Jordan block associated with the eigenvalue [math], or equivalently $A$ is invertible.

• •

For each Jordan block $J$, the last coordinate of the point $x_{J}$ is not zero, i.e. $x_{J,d(J)}\neq 0$.

• •

There is no diagonal Jordan block with an eigenvalue which is a root of unity,

• •

Any Jordan block $J$ with an eigenvalue of modulus $<1$ has $y_{J}\neq 0.$

Lemma 5

The existence of semilinear invariants for Orbit instances reduces to the same problem for normalized Orbit instances in Jordan normal form.

Lemma 5 is proved in Appendix 0.B.

5.2 Positive cases

Many Orbit instances present a divergence which we can exploit to construct a semilinear invariant. Such behaviours are easily identified once the matrix is in Jordan Normal Form, as properties of its Jordan blocks. We isolate three such cases.

• •

If there is an eigenvalue of modulus $>1$. Call $J$ its Jordan block. Projecting to the last coordinate of $J$ the orbit of $x$ diverges to $\infty$ in modulus (see Example 1). A long enough “initial segment” $\{x,Ax,\dots,A^{k}x\}$ together with the complement of its convex hull (on the last coordinate of $J$) constitutes a semilinear invariant. See Appendix 0.C for details.

• •

If there is an eigenvalue of modulus $<1$ in block $J$, the situation is quite similar with a convergence towards 0. However, the construction we give is more involved, the reason being that we may not just concentrate on the last nonzero coordinate $x_{J,l}$ of $x_{J}$, since $y_{J,l}$ may very well be 0, which belongs to the adherence of the orbit on this coordinate. Yet on the full block, $y_{J}\neq 0$. We show how to construct, for any $0<\varepsilon$, a semilinear invariant $\mathcal{I}$ such that $B(0,\varepsilon^{\prime})\subseteq\mathcal{I}\subseteq B(0,\varepsilon)$ for some $\varepsilon^{\prime}>0$. Picking $\varepsilon$ small enough we make sure that $y\notin\mathcal{I}$, and then $\{x,Ax,\dots,A^{k}x\}\cup\mathcal{I}$ is a semilinear invariant if $k$ is large enough so that $||A^{k}x||\leq\varepsilon^{\prime}$. See Appendix 0.D for more details.

• •

Finally, if there is an eigenvalue which is a root of unity, say $\lambda^{n}=1$, on a Jordan block $J$ of size at least 2 (that is, a non diagonal block), then penultimate coordinate on $J$ of the orbit goes to $\infty$ in modulus. In this case, the orbit on this coordinate is contained in a union of $n$ half-lines which we cut far enough away from 0 and add an initial segment to build a semilinear invariant. See Appendix 0.E for details.

Note that in each of these cases, we concentrate on the corresponding (stable) eigenspace, construct a separating semilinear invariant for this restriction of the problem, and extend it to the full space by allowing any value on other coordinates.

5.3 Minimal invariants

We have now reduced to an instance where all eigenvalues have modulus 1 and are not roots of unity. Intuitively, in this setting, semilinear invariants fail, as they are not precise enough to exploit subtle multiplicative relations that may hold among eigenvalues. However, it may be the case that some coarse information in the input can still be stabilised by an semilinear invariant, for instance if two synchronised blocks are exactly identical (see Examples 4 and 5 for more elaborate cases).

We start by identifying exactly where semilinear invariants fail. Call two eigenvalues equivalent if their quotient is a root of unity (that is, they have a multiplicative relationship of degree 1). We show that whenever no two different eigenvalues are even non-equivalent, the only stable semilinear sets are trivial. As a consequence, computing the minimal semilinear invariant in this setting is easy, as it is basically the whole space (except where $x$ is 0). However, this lower bound (non-existence of semilinear invariant) constitutes the most technically involved part. Our proof is inductive with as base case the diagonal case, where it makes crucial use of the Skolem-Mahler-Lech theorem. This is the subject of Appendix 0.F.1.

When the matrix has several equivalent eigenvalues, we show how to iteratively reduce the dimension in order to eventually fall into the previous scenario. Rougly speaking, if $A$ is comprised of two identical blocks $B$, we show that it suffices to compute a minimal invariant $\mathcal{I}_{B}$ for $B$, since $\{z\mid\tilde{z}_{1}\in\mathcal{I}_{B}\text{ and }\tilde{z}_{2}=\tilde{z}_{1}\}$ (with obvious notations) is a minimal invariant for $A$. This is achieved, by first assuming that all equivalent eigenvalues are in fact equal and then easily reducing to this case by considering a large enough iterations of $A$, in Appendix 0.F.1.

Appendix 0.A Proof of Theorem 3.3

We now turn to the second proof without the use of guards. The idea is similar, however, the reduction is far more involved as the use of a guard is now replaced by the test of reachability of additional variables.

We reduce an instance of the $\omega$-PCP problem. Let $\{(u^{(1)},v^{(1)}),\dots,(u^{(9)},v^{(9)})\}$ be an instance of the $\omega$-PCP problem. We denote $|u^{(i)}|={n_{i}}$ and $|v^{(i)}|={m_{i}}$ and we build the matrices $M_{1},\dots M_{9},M^{1}_{m},M^{2}_{m},$ $M_{x},M_{e},M_{-},M_{p},M_{d}$ of dimension 21 where:

• •

for $i=1\dots 9$, $M_{i}[1,1]=1,M_{i}[1,2]=\left[u^{(i)}\right]=(u^{(i)}_{1}+u^{(i)}_{2}/4+\dots+u^{(i)}_{n_{i}}/4^{{n_{i}}-1})$, $M_{i}[1,3]=-\left[v^{(i)}\right]$, $M_{i}[2,2]=1/4^{n_{i}}$, $M_{i}[3,3]=1/4^{m_{i}}$, $M_{i}[4,4]=1$, $M_{i}[4,7]=2$, $M_{i}[5,5]=1$, $M_{i}[6,6]=4^{n_{i}+m_{i}}$ $M_{i}[7,7]=1$ and all other values are set to 0.

• •

$M^{1}_{m}[8,1]=1$, $M^{1}_{m}[8,2]=-4=M^{1}_{m}[8,3]$, $M^{1}_{m}[9,1]=1$, $M^{1}_{m}[9,2]=-4=M^{1}_{m}[9,3]$, $M^{1}_{m}[9,5]=-1$, $M^{1}_{m}[10,1]=1$, $M^{1}_{m}[11,4]=1$, $M^{1}_{m}[12,1]=1$, $M^{1}_{m}[13,6]=1$, $M^{1}_{m}[14,7]=1$ and all other values are set to 0.

• •

$M^{2}_{m}[8,1]=-1$, $M^{2}_{m}[8,2]=-4=M^{2}_{m}[8,3]$, $M^{2}_{m}[8,5]=-1$, $M^{2}_{m}[9,1]=-1$, $M^{2}_{m}[9,2]=-4=M^{2}_{m}[9,3]$, $M^{2}_{m}[9,5]=-1$, $M^{2}_{m}[10,1]=-1$, $M^{2}_{m}[11,4]=1$, $M^{2}_{m}[12,1]=-1$, $M^{2}_{m}[13,6]=1$, $M^{2}_{m}[14,7]=1$ and all other values are set to 0.

• •

for $i=8\dots 14$, $M_{x}[i,i]=1$, $M_{x}[8,9]=M_{x}[10,12]=1$, $M_{x}[13,14]=-1$ and all other values are set to 0.

• •

$M_{e}[15,8]=M_{e}[17,10]=M_{e}[18,11]=M_{e}[20,13]=M_{e}[21,14]=1$ and all other values are set to 0.

• •

$M_{-}[18,21]=-2$, for $i=15\dots 21$, $M_{-}[i,i]=1$ and all other values are set to 0.

• •

$M_{p}[15,21]=1$, for $i=15\dots 21$, $M_{p}[i,i]=1$ and all other values are set to 0.

• •

$M_{d}[17,21]=-1$, for $i=15\dots 21$, $M_{d}[i,i]=1$ and all other values are set to 0.

Let us explain informally the effects of the different matrices. The dimensions can be separated in three blocs of 7 each. The seven variables associated to the bloc number $i\in\{1,2,3\}$ are called $(s^{i},c^{i},d^{i},n^{i},r^{i},k^{i},a^{i})$. As a general overview, the first bloc is used to apply the matrices $M_{i}$ as in the previous proof (with the guards), the second bloc ensures every value is an integer allowing us, in the third bloc, to use reachability tests in order to verify that the guard of the previous proof holds.

• •

The matrices $M_{i}$ only affects the first bloc of variables. On these variables, the effect of these matrices is similar to the effect of the matrices $\tilde{M_{i}}$ of the extended sketch of proof of the Theorem 3.3. The one difference comes from the additional variables $r^{1}$, which is not used but kept for symmetry with the other blocs, and $k^{1}$ which is increased strongly by $M_{i}$ in a way ensuring that $k^{1}s^{1},k^{1}c^{1}$ and $k^{1}d^{1}$ are integers.

• •

The matrices $M^{1}_{m}$ and $M^{2}_{m}$ modifies the variables of the bloc 1 and transfer them to the second bloc. Precisely, we have that applying $M_{m}^{1}$ realise the following transformation

[TABLE]

and the variables of the bloc 1 are set to 0. $M_{m}^{2}$ has a similar effect, replacing instances of $s^{1}$ by $-s^{1}$.

• •

The matrix $M_{x}$ affects the second bloc this way:

[TABLE]

Remark that, from the values $(s^{2},s^{2},d^{2},n^{2},d^{2},k^{2},a^{2})$ reached after firing one of the matrix $M_{m}^{i}$, using $M_{x}$ successively $k^{2}$ times reaches the values $(k^{2}s^{2},s^{2},k^{2}d^{2},n^{2},d^{2},0,a^{2})$. This ensures the first and third variables are now integers.

• •

$M_{e}$ moves the variable to the third bloc while putting to 0 two variables that are not useful any more $c^{3}$ and $r^{3}$ (remark thus than one could simply use matrices of dimension 19 instead of 21. We kept 21 to simplify the representation). In other words, after applying $M_{e}$ we have

[TABLE]

and all other variables are set to 0.

• •

The matrices $M_{p}$, $M_{d}$ and $M_{-}$ respectively increases by 1, decreases by 1 and decreases by 2 the value of $s^{3}$, $d^{3}$ and $n^{3}$.

The use of these three blocs divides the firing of a sequence of matrices in three steps. The first step corresponds to the firing of the matrices $M_{i}$ which are the only ones keeping the values within the first dimension bloc. This first step is similar to what was done in the previous proof. Using one of the two matrices $M^{i}_{m}$, $i\in\{1,2\}$, starts the second step by moving the values to the second bloc (the use of two different matrices is required to represent and check the absolute value in the guard of the previous proof). From now on, the matrices $M_{i}$ have no effect on the system. The goal of the second, and partially the third, step is to verify whether the guard of the previous proof held when the second step started. To do so, we first use the matrix $M_{x}$ in order to turn the first two variables into integers. If $M_{x}$ is not applied an adequate number of times, then the variable labelled by $k$ will never be equal to [math], ensuring non-reachability of the target. We then use the matrix $M_{e}$ to start the third step. Assuming the multiplication was correctly done, then $s^{3}$ and $d^{3}$ are now integers. Moreover, $s^{3}<0$ and $d^{3}>0$ iff the guard of the previous proof held when the first step ended. Thus reaching the target on all variables, except for $n^{3}$, is possible iff the guard was indeed respected. The case of the counter $n^{3}$ is then identical to the one of $n$ in the previous proof.

Let us formally show that there exists a separating invariant of the instance $((M_{1},\dots M_{9},M^{1}_{m},M^{2}_{m},M_{x},M_{e},M_{-},M_{p},M_{d}),x,y)$ with $x\in\{(0,1,1,0,1,1,1)\}\times\{0\}^{14}$ and $y\in\{0\}^{14}\times\{(-1,0,0,1,0,0,1)\}$ iff the $\omega$-PCP has no solution.

Assume first that the $\omega$-PCP does not possess a solution. There thus exists $n_{0}\in\mathbb{N}$ such that any pair of words $(u^{(w)},v^{(w)})$ on $\{0,2\}$ generated from the $\omega$-PCP instance differs on one of the first $n_{0}$ letters.

We define the invariant $I=I_{1}\cup I_{2}\cup I_{3}$ where

• •

$I_{1}=\{M_{w}x\mid w\in\{1,\dots,9\}^{*}\wedge|w|\leq n_{0}+1\}\cup\{(s^{1},c^{1},d^{1},n^{1},r^{1},k^{1},1)\mid|s^{1}|\geq 4(c^{1}+d^{1})\}\times\{0\}^{14}$.

• •

$I_{2}=\{M^{j}_{x}M_{m}^{i}M_{w}x\mid i\in\{1,2\}\wedge j\in\mathbb{N}\wedge w\in\{1,\dots,9\}^{*}\wedge|w|\leq n_{0}+1\}\cup\{0\}^{7}\times\{(s^{2},c^{2},d^{2},n^{2},r^{2},k^{2},1)\mid k^{2}\leq-1\vee(d^{2}<0\wedge r^{2}<0)\vee(s^{2}\geq 0\wedge c^{2}\geq 0)\}\times\{0\}^{7}$.

$I_{2}$ is semilinear: while the first set is technically an infinite set of points, when $j$ is high enough, the variable $k^{2}$ becomes negative, ensuring that the point belongs to the second set of $I_{2}$ (which is clearly semilinear). Thus the first set only adds to $I_{2}$ a finite number of points. It is not closed however. This is not important in this proof as we do not require this condition here. $\overline{I_{2}}$ could also be used, but would require some additional arguments.

• •

$I_{3}=\{M_{p}^{j_{2}}M_{d}^{j_{3}}M^{j_{4}}_{-}M_{e}M^{j_{1}}_{x}M_{m}^{i}M_{w}x\mid i\in\{1,2\}\wedge j_{1},j_{2},j_{3},j_{4}\in\mathbb{N}\wedge w\in\{1,\dots,9\}^{*}\wedge|w|\leq n_{0}+1\}\cup\{0\}^{14}\times\{(s^{3},c^{3},d^{3},n^{3},r^{3},k^{3},1)\mid k^{3}\leq 1\vee n^{3}\leq 0\vee s^{3}\geq 0\vee d^{3}<0\}$.

As for $I_{2}$, the first set represents an infinite number of points, but which all reach the second set after a bounded number of steps.

This invariant contains the initial configuration but not the target. It is semilinear. Let us show that it is stable.

Let $h\in I$, we denote the variables within $h$ of the block of seven dimensions number $i\in\{1,2,3\}$ by $(s^{i},c^{i},d^{i},n^{i},r^{i},k^{i},a^{i})$.

$\bullet$ Case $h\in I_{1}$. If $|s^{1}|\geq 4(c^{1}+d^{1})$, then for $i\leq 9$, $M_{i}h$ satisfies the same property and for $j\in\{1,2\}$, $M^{j}_{m}h\in\{0\}^{7}\times\{(s^{2},c^{2},d^{2},n^{2},r^{2},k^{2},1)\mid(d^{2}<0\wedge r^{2}<0)\vee(s^{2}\geq 0\wedge c^{2}\geq 0)\}\times\{0\}^{7}\subseteq I_{2}$. The other matrices do not modify $s^{1},c^{1}$ and $d^{1}$ ensuring the property still holds. If there exists $w\in\{1,\dots,9\}^{*},|w|\leq n_{0}+1$ such that $h=M_{w}x$, then for $j\in\{1,2\}$, $M^{j}_{m}h\in I_{2}$, if $|w|\leq n_{0}$, for all $i\leq 9$, $M_{i}h\in I_{1}$ and if $|w|=n_{0}+1$, then,as seen in the proof of Theorem 3.1, $|s^{1}|\geq 4(c^{1}+d^{1})$. The other matrices do not modify the variables.

$\bullet$ Case $h\in I_{2}$. Only two matrices can affect $h$ in meaningful ways: $M_{x}$ and $M_{e}$. As $M_{e}$ transfer the values to the third block without affecting the positivity (or negativity) of $s^{2},d^{2}$ and $k^{2}$, $M_{e}h\in I_{3}$. As $M_{x}$ removes 1 from $k^{2}$ and adds $c^{2}$ to $s^{2}$ and $r^{2}$ to $d^{2}$, if $h$ satisfies $k^{2}\leq-1\vee(d^{2}<0\wedge r^{2}<0)\vee(s^{2}\geq 0\wedge c^{2}\geq 0)$, then so does $M_{x}h$. Finally, if $h$ can be written in the form $M^{j}_{x}M_{m}^{i}M_{w}x$, then it is immediately also the case for $M_{x}h$.

$\bullet$ Case $h\in I_{3}$. The matrices that affect the variables in meaningful ways are $M_{p}$, $M_{d}$ and $M_{-}$. As they are commutative and respectively increases by 1, decreases by 1 and decreases by 2 the value of $s^{3}$, $d^{3}$ and $n^{3}$, we have that all $M_{p}h$, $M_{d}h$ and $M_{-}h$ are in $I_{3}$.

Thus $I$ is a separating invariant of the instance.

Conversely, assume the $\omega$-PCP possesses a solution $w\in\{1,\dots,9\}^{\omega}$. For $z\in\mathbb{N}$, we denote $w\restriction_{z}$ the prefix of length $z$ of $w$ and $h_{z}=M_{w\restriction_{z}}x$. Then for all $z\in\mathbb{N}$, $|s_{z}^{1}|<4(c_{z}^{1}+d_{z}^{1})$ as showed in the proof of Theorem 3.1. If $s_{z}^{1}\geq 0$ (resp. $s_{z}^{1}<0$), triggering the sequence of matrices $M_{e}(M_{x})^{k^{1}_{z}}M^{1}_{m}$ (resp. $M_{e}(M_{x})^{k^{1}_{z}}M^{2}_{m}$) on $h_{z}$ one reaches a point $g_{z}\in\{0\}^{14}\times\{(s^{3},0,d^{3},2z,0,0,1)\}$ where $s^{3}$ is a strictly negative integer and $d^{3}$ is a positive integer. Therefore, using the matrices $M_{p}$ and $M_{d}$ one can reach the point $y_{2z}\in\{0\}^{14}\times\{(-1,0,0,2z,0,0,1)\}$. As this is true for all $z\in\mathbb{N}$, any semilinear invariant $I$ containing all the points $y_{2z}$ contains a point $y_{m}$ with $m\in\mathbb{N}$ an odd integer. Therefore as $I$ is stable under $M_{-}$, it must contains the target and thus is not a separating invariant of $((M_{1},\dots M_{9},M^{1}_{m},M^{2}_{m},M_{x},M_{e},M_{-},M_{p},M_{d}),x,y)$.

This concludes the reduction.

Appendix 0.B Proof of Lemma 5

Let $\ell=(A,x,y)$ be a non-reach instance in Jordan normal form.

• •

Suppose $A$ is not invertible, we distinguish two cases.

• –

If for some Jordan block $J$ associated with the eigenvalue [math], we have that $y$ is not the zero vector, i.e., $y_{J}\neq 0$, then $\mathcal{I}=\left\{x,Ax,\ldots,A^{d-1}x\right\}\cup\left\{z\in\mathbb{C}^{d}\mid z_{J}=0\right\}$ is a semilinear invariant. Indeed, the Jordan block $J$ is nilpotent, so for any point $u$ and $n\geq d$, we have that $J^{n}u=0$, so in particular $(A^{n}x)_{J}=0$. Moreover, since by assumption $y$ is not reachable, it is not one of $A^{n}x$ for $n<d$, and $y_{J}\neq 0$, so $y\notin\mathcal{I}$.

• –

Otherwise, let $J$ be a Jordan block associated with the eigenvalue [math], such that $y_{J}=0$. Consider the Orbit instance $\ell^{\prime}=(A_{J^{\mathsf{c}}},(A^{d}x)_{J^{\mathsf{c}}},y_{J^{\mathsf{c}}})$. We claim that $\ell$ admits a semilinear invariant if, and only if, $\ell^{\prime}$ does.

Let $\mathcal{I}$ be a semilinear invariant for $\ell$. Build $\mathcal{I}^{\prime}=\left\{z\in\mathbb{C}^{J^{\mathsf{c}}}\mid(z,0)\in\mathcal{I}\right\}$. We argue that $\mathcal{I}^{\prime}$ is a semilinear invariant for $\ell^{\prime}$. Indeed, $(A^{d}x)_{J^{\mathsf{c}}}\in\mathcal{I}^{\prime}$ since $A^{d}x\in\mathcal{I}$ and $(A^{d}x)_{J}=0$, because the Jordan block $J$ is nilpotent. The stability of $\mathcal{I}^{\prime}$ under $A_{J^{\mathsf{c}}}$ is clear, and $y_{J^{\mathsf{c}}}$ is not in $\mathcal{I}^{\prime}$ because $y_{J}=0$, so if $y_{J^{\mathsf{c}}}$ would be in $\mathcal{I}^{\prime}$ this would imply that $y$ is in $\mathcal{I}$.

Conversely, let $\mathcal{I}^{\prime}$ be a semilinear invariant for $\ell^{\prime}$, let $\mathcal{I}=\mathcal{I}^{\prime}\times\mathbb{C}^{J}$, then $\left\{x,Ax,\ldots,A^{d-1}x\right\}\cup\mathcal{I}$ is a semilinear invariant for $\ell$.

We reduced the existence of semilinear invariants from $\ell$ to $\ell^{\prime}$, removing one Jordan block $J$ such that $y_{J}=0$. Proceeding this way for each such Jordan block, we reduce to the case where the matrix is invertible.

• •

Suppose $A$ contains a Jordan block $J$ such that $x_{J,d(J)}=0$. We distinguish two cases.

• –

If for some Jordan block $J$ we have $x_{J,d(J)}=0$ and $y_{J,d(J)}\neq 0$, then the set $\mathcal{I}=\left\{z\in\mathbb{C}^{d}\mid z_{J,d(J)}=0\right\}$ is a semilinear invariant for $\ell$.

• –

Otherwise, let $J$ be a Jordan block such that $x_{J,d(J)}=y_{J,d(J)}=0$. Write $p$ for the dimension $(J,d(J))$. Consider the Orbit instance $\ell_{p}=(A_{p^{c}},x_{p^{c}},y_{p^{c}})$, we claim that $\ell$ admits a semilinear invariant if, and only if, $\ell_{p}$ does.

Let $\mathcal{I}$ be a semilinear invariant for $\ell$. Build $\mathcal{I}_{p}=\left\{z\in\mathbb{C}^{p^{c}}\mid(z,0)\in\mathcal{I}\right\}$, then $\mathcal{I}_{p}$ is a semilinear invariant for $\ell_{p}$. Conversely, let $\mathcal{I}_{p}$ be a semilinear invariant for $\ell_{p}$, let $\mathcal{I}=\left\{z\in\mathbb{C}^{d}\mid z_{p}=0\text{ and }z_{p^{c}}\in\mathcal{I}_{p}\right\}$, then $\mathcal{I}$ is a semilinear invariant for $\ell$.

We reduced the existence of semilinear invariants from $\ell$ to $\ell_{p}$, removing the last dimension in a Jordan block $J$ such that $x_{J,d(J)}=0$. Proceeding this way for each such Jordan block, we reduce to the case where there are no such Jordan blocks.

• •

Suppose $A$ has a diagonal Jordan block $J$, that is, $d(J)=1$, with eigenvalue $\lambda$ with $\lambda^{n}=1$. We set $n$ minimal such that $\lambda^{n}=1$ and distinguish two cases

• –

If for every $k\leq n-1$, $y_{J}\neq\lambda^{k}x_{J}$, then the set $\mathcal{I}=\bigcup_{k=0}^{n-1}\{z\mid z_{J}=\lambda^{k}x_{J}\}$ is a semilinear invariant for $\ell$.

• –

Otherwise, let $k\leq n-1$ be such that $y_{J}=\lambda^{k}x_{J}$. We claim that there exists an invariant for $\ell$ if and only if there exists an invariant for $\ell^{\prime}=(A_{J^{\mathsf{c}}}^{n},A_{J^{\mathsf{c}}}^{k}x_{J^{\mathsf{c}}},y_{J^{\mathsf{c}}})$. Let $\mathcal{I}^{\prime}$ be an invariant for $\ell^{\prime}$. For $k^{\prime}\in\{0,\dots,n-1\},$ we put

[TABLE]

$\mathcal{I}=\{x,Ax,\dots,A^{k-1}x\}\cup\bigcup_{k^{\prime}=0}^{n-1}\mathcal{I}_{k^{\prime}}$, and prove that the semilinear set $\mathcal{I}$ is an invariant for $\ell$. It is clear that $x\in\mathcal{I}$. Moreover, $y$ does not belong to $\mathcal{I}$: indeed, $y\notin\{x,Ax,\dots,A^{k-1}x\}$ and $y\notin\bigcup_{k^{\prime}=1}^{n-1}\mathcal{I}_{k^{\prime}}$ because $y_{J}=\lambda^{k}x_{J}\neq\lambda^{k+k^{\prime}}x_{J}$ for any $k^{\prime}\in\{1,\dots,n-1\}$ (we assume $x_{J}\neq 0$ thanks to a previous reduction), and $y\notin\mathcal{I}_{0}$ since $\mathcal{I}^{\prime}$ is an invariant for $\ell^{\prime}$. Finally, $\mathcal{I}$ is stable for $A$ since $A^{k}x\in\mathcal{I}_{0}$, $A\mathcal{I}_{k^{\prime}}=\mathcal{I}_{k^{\prime}+1}$ if $k<n-1$ and $A\mathcal{I}_{n-1}=A^{n}\mathcal{I}_{0}\subseteq\mathcal{I}_{0}$ since $\lambda^{n}=1$ and $A_{J^{\mathsf{c}}}^{n}\mathcal{I}^{\prime}\subseteq\mathcal{I}^{\prime}$.

Conversely, let $\mathcal{I}$ be an invariant for $\ell$. We let $\mathcal{I}^{\prime}$ be the projection on $J^{\mathsf{c}}$ of $A^{k}\mathcal{I}\cap\{z\mid z_{J}=\lambda^{k}x_{J}\}$, and claim it is an invariant for $\ell^{\prime}$. Indeed, quite clearly $A_{J^{\mathsf{c}}}^{k}x_{J^{\mathsf{c}}}\in\mathcal{I}^{\prime}$ and $\mathcal{I}^{\prime}$ is stable for $A_{J^{\mathsf{c}}}^{n}$. Now, if $y_{J^{\mathsf{c}}}\in\mathcal{I}^{\prime}$ then it must be that $y\in\mathcal{I}$, a contradiction.

• •

Let $J$ be a Jordan block of $A$ with eigenvalue $\lambda<1$ and such that $y_{J}=0$. If there are infinitely many integers $n$ such that $A_{J^{\mathsf{c}}}^{n}x_{J^{\mathsf{c}}}=y_{J^{\mathsf{c}}},$ then $y\in\overline{\{A^{n}x,n\in\mathbb{N}\}}$, so there exists no closed invariant for $\ell$. Otherwise, we let $n_{0}\in\mathbb{N}$ be such that $y_{J^{\mathsf{c}}}\notin\{A_{J^{\mathsf{c}}}^{n}x_{J^{\mathsf{c}}},n\geq n_{0}\}$, and claim that $\ell$ is equivalent to $\ell^{\prime}=(A_{J^{\mathsf{c}}},A_{J^{\mathsf{c}}}^{n_{0}}x_{J^{\mathsf{c}}},y_{J^{\mathsf{c}}})$. Let $\mathcal{I}^{\prime}$ be a semilinear invariant for $\ell^{\prime}$. Then $\mathcal{I}=\{x,Ax,\dots,A^{n_{0}-1}x\}\cup\{z\mid z_{J^{\mathsf{c}}}\in\mathcal{I}^{\prime}\}$ is an invariant for $\ell$. Conversely, let $\mathcal{I}$ be an invariant for $\ell$. Let $\delta=\frac{1}{2}d(y,\mathcal{I})>0,$ where the distance is defined according to the infinity norm on $\mathbb{C}^{d}$. Using Lemma 8 from section 0.D, we construct a semilinear $P\subseteq\mathbb{C}^{J}$ which is stable for $A_{J},$ contains $(A^{n}x)_{J}$ for some $n$, and is included in $B(0,\delta)$. Let $\mathcal{I}^{\prime}$ be the projection of $\{z\mid z\in\mathcal{I}\text{ and }z_{J}\in P\}$ on $J^{\mathsf{c}}$. Then $A_{J^{\mathsf{c}}}^{n}x_{J^{\mathsf{c}}}\in\mathcal{I}^{\prime}$ and $\mathcal{I}^{\prime}$ is stable for $A_{J^{\mathsf{c}}}$. Assume that $y_{J^{\mathsf{c}}}\in\mathcal{I}^{\prime}$, that is, there exists $\tilde{y}\in P$ such that $y_{1}=(y_{J^{\mathsf{c}}},\tilde{y})\in\mathcal{I}$. Then $d(y,\mathcal{I})\leq d(y,y_{1})=||\tilde{y}||\leq\delta/2$ which is a contradiction, so $y_{J^{\mathsf{c}}}\notin\mathcal{I}^{\prime}$. Finally, $\{A_{J^{\mathsf{c}}}^{n_{0}}x_{J^{\mathsf{c}}},A_{J^{\mathsf{c}}}^{n_{0}+1}x_{J^{\mathsf{c}}},\dots,A_{J^{\mathsf{c}}}^{n-1}x_{J^{\mathsf{c}}}\}\cup\mathcal{I}^{\prime}$ is an invariant for $\ell^{\prime}$ which concludes the proof.

Appendix 0.C Some eigenvalue has modulus greater than 1

We start with a simple lemma.

Lemma 6

Let $\lambda$ be a complex non-real number of modulus greater than $1$ and $x$ be a non-zero complex number. Then the sequence of polyhedra in $\mathbb{C}$ $\left(\text{Conv}\left(\left\{\lambda^{i}x\mid i\in\left\{0,\ldots,n\right\}\right\}\right)\right)_{n\in\mathbb{N}}$ is strictly increasing and its limit is $\mathbb{C}$.

Proof

To see that the sequence is strictly increasing, observe that for all $n$ in $\mathbb{N}$, we have

[TABLE]

It follows that $\lambda^{n+1}x$ is not in $\text{Conv}\left(\left\{\lambda^{i}x\mid i\in\left\{0,\ldots,n\right\}\right\}\right)$.

We now prove that its limit is $\mathbb{C}$. We write $x=|x|e^{i\theta}$ and $\lambda=|\lambda|e^{i\alpha}$, with $\theta,\alpha$ in $[0,2\pi)$. Since $\lambda$ is not a real number, $\alpha$ is not [math]. Let $n_{0}$ in $\mathbb{N}$ such that $n_{0}\alpha>2\pi$. Observe that [math] is in $\text{Conv}\left(\left\{\lambda^{i}x\mid i\in\left\{0,\ldots,n_{0}\right\}\right\}\right)$.

We claim that for all $n\in\mathbb{N}$, we have

[TABLE]

Let $z=|z|e^{i\beta}$ such that $|z|<|\lambda|^{n}\cdot|x|$. Let $p$ in $\left\{0,\ldots,n_{0}-1\right\}$ such that $\beta$ is in $[\theta+(n+p)\alpha,\theta+(n+p+1)\alpha)$. Then $z$ is in $\text{Conv}\left(\left\{0,\lambda^{n+p}x,\lambda^{n+p+1}x\right\}\right)$.

The claim follows, since the union of the balls $B(0,|\lambda|^{n}\cdot|x|)$ for $n\in\mathbb{N}$ is $\mathbb{C}$.

Theorem 0.C.1

Let $\ell=(A,x,y)$ be a normalized Orbit instance in Jordan normal form. Assume that $\ell$ is a non-reach instance. If the matrix $A$ has an eigenvalue whose modulus is greater than $1$, then there exists a semilinear invariant for $\ell$.

On an intuitive level first: some coordinate of $(A^{n}x)_{n\in\mathbb{N}}$ diverges to infinity, so eventually gets larger in absolute value than the corresponding coordinate in $y$. This allows us to construct an invariant for $\ell$ by taking the first points and then all points having a large coordinate in the diverging dimension. For the invariant to be semilinear we consider the complement of the convex envelope of an initial segment of points.

Proof

Let $J$ be a Jordan block of $A$ with eigenvalue $\lambda$ of modulus $>1$. Since $\ell$ is non-trivial, we have $x_{J,d(J)}\neq 0$. We distinguish two cases.

• •

Suppose that $\lambda$ is a real number.

For all $n\in\mathbb{N}$, we have $(A^{n}x)_{J,d(J)}=\lambda^{n}x_{J,d(J)}$, so it diverges to infinity in modulus. It follows that there exists $n_{0}$ in $\mathbb{N}$ such that $|(A^{n_{0}}x)_{J,d(J)}|>2\sqrt{2}\cdot|y_{J,d(J)}|$. Let

[TABLE]

We argue that $\mathcal{I}$ is a semilinear invariant for $\ell$. The non-trivial point is that $\mathcal{I}$ is stable under $J$. First, $A^{n_{0}}x$ is in $\mathcal{I}$ because

[TABLE]

Second, let $z\in\mathbb{C}^{d}$ such that $|\text{Re}\left(z_{J,d(J)}\right)|+|\text{Im}\left(z_{J,d(J)}\right)|\geq 2|y_{d}|$, we have that $(Az)_{J,d(J)}=\lambda z_{J,d(J)}$, so $|\text{Re}\left((Az)_{J,d(J)}\right)|+|\text{Im}\left((Az)_{J,d(J)}\right)|=|\lambda|(|\text{Re}\left(z_{J,d(J)}\right)|+|\text{Im}\left(z_{J,d(J)}\right)|)>2|y_{J,d(J)}|$, implying that $Az$ is in $\mathcal{I}$. Note that the previous equality holds because $\lambda$ is a real number.

• •

Suppose that $\lambda$ is not a real number.

Consider the sequence $\left(\text{Conv}\left(\left\{\lambda^{i}x_{J,d(J)}\mid i\in\left\{1,\ldots,n\right\}\right\}\right)\right)_{n\in\mathbb{N}}$ of polyhedra in $\mathbb{C}$. Thanks to Lemma 6, this sequence is strictly increasing and its limit is $\mathbb{C}$. Let $n_{0}$ in $\mathbb{N}$ such that $y_{J,d(J)}$ and $x_{J,d(J)}$ are both in the interior of $\text{Conv}\left(\left\{\lambda^{i}x_{J,d(J)}\mid i\in\left\{1,\ldots,n_{0}\right\}\right\}\right)$. Let us denote this convex set by $C$, and let

[TABLE]

We argue that $\mathcal{I}$ is a semilinear invariant for $\ell$. The non-trivial point is that $\mathcal{I}$ is stable under $A$.

We first need to prove that $A^{n_{0}+1}x$ is in $\mathcal{I}$. We have $(A^{n_{0}+1}x)_{J,d(J)}=\lambda^{n_{0}+1}x_{J,d(J)}$, which is not in $\overline{\text{Conv}\left(\left\{\lambda^{i}x_{J,d(J)}\mid i\in\left\{1,\ldots,n_{0}\right\}\right\}\right)}$, because this sequence of polyhedra is strictly increasing. Thus $A^{n_{0}+1}x$ is in $\mathcal{I}$.

Finally, let $z\in\mathbb{C}^{d}$ such that $z_{J,d(J)}\notin\overline{C}$, we show that $Az$ is in $\mathcal{I}$. We have $(Az)_{J,d(J)}=\lambda z_{J,d(J)}$. Assume towards contradiction that $(Az)_{J,d(J)}$ is in $C$, so $\lambda z_{J,d(J)}$ is a convex combination of $\left\{\lambda^{i}x_{J,d(J)}\mid i\in\left\{1,\ldots,n_{0}\right\}\right\}$. This implies that $z_{J,d(J)}$ is a convex combination of $\left\{\lambda^{i-1}x_{J,d(J)}\mid i\in\left\{1,\ldots,n_{0}\right\}\right\}$. Since $x_{J,d(J)}$ is in $C$, this implies that $z_{J,d(J)}$ is in $C$, which is a contradiction. Thus $Az$ is in $\mathcal{I}$, and $\mathcal{I}$ is a semilinear invariant for $\ell$.

Appendix 0.D Some eigenvalue has modulus less than 1

We start with a simple lemma.

Lemma 7

Let $\lambda$ be a complex non-real number of modulus less than $1$ and $x$ be a non-zero complex number. Then the sequence $\left(\text{Conv}\left(\left\{\lambda^{i}x\mid i\in\left\{0,\ldots,n\right\}\right\}\right)\right)_{n\in\mathbb{N}}$ of polyhedra in $\mathbb{C}$ is ultimately constant, and its limit contains an open neighbourhood of [math].

Proof

We write $x=|x|e^{i\theta}$ and $\lambda=|\lambda|e^{i\alpha}$, with $\theta,\alpha$ in $[0,2\pi)$. Since $\lambda$ is not a real number, $\alpha$ is not [math]. Let $n_{0}$ in $\mathbb{N}$ such that $n_{0}\alpha>2\pi$. Observe that [math] is in $\text{Conv}\left(\left\{\lambda^{i}x\mid i\in\left\{0,\ldots,n_{0}\right\}\right\}\right)$.

We claim that $B(0,|\lambda|^{n_{0}}\cdot|x|)$ is included in $\text{Conv}\left(\left\{\lambda^{i}x\mid i\in\left\{0,\ldots,n_{0}\right\}\right\}\right)$. Let $z=|z|e^{i\beta}$ such that $|z|<|\lambda|^{n_{0}}\cdot|x|$. Let $p$ in $\left\{0,\ldots,n_{0}-1\right\}$ such that $\beta$ is in $[\theta+p\alpha,\theta+(p+1)\alpha)$. Then $z$ is in $\text{Conv}\left(\left\{0,\lambda^{p}x,\lambda^{p+1}x\right\}\right)$.

The claim follows, since for all $n>n_{0}$, we have that $\lambda^{n}x$ is in $B(0,|\lambda|^{n_{0}}\cdot|x|)$.

The following Lemma is the cornerstone for this section.

Lemma 8

Let $\varepsilon>0$ and $\lambda\in\mathbb{C}$ with $|\lambda|<1$. There exists a semilinear set $\mathcal{I}\subseteq B(0,\varepsilon)\subseteq\mathbb{C}^{d}$ which is stable for $\mathcal{J}_{d}(\lambda)$, and contains $B(0,\varepsilon^{\prime})$ for some $0<\varepsilon^{\prime}<\varepsilon$.

Proof

We let $J$ denote $\mathcal{J}_{d}(\lambda)$, and prove the Lemma by induction on $d$. We first treat the case where $\lambda\in\mathbb{R}$. Let

[TABLE]

Then $B(0,\varepsilon(1-|\lambda|)^{d}/2)\subseteq\mathcal{I}$. We show that $J\mathcal{I}\subseteq\mathcal{I}$. Let $z\in\mathcal{I}$. Then $(Jz)_{d}=\lambda z_{d}$, so $|\text{Re}\left((Jz)_{d}\right)|+|\text{Im}\left((Jz)_{d}\right)|\leq|\lambda|(|\text{Re}\left(z_{d}\right)|+|\text{Im}\left(z_{d}\right)|)\leq\varepsilon(1-|\lambda|)^{d}$. Now if $i<d$, $(Jz)_{i}=\lambda z_{i}+z_{i+1}$, so

[TABLE]

Hence $\mathcal{I}$ is stable for $J$, which concludes this first case. We now assume that $\lambda\notin\mathbb{R}$. We start with the base case $d=1$. Let $u\in\mathbb{C}$ of modulus $\varepsilon$, for instance $u=\varepsilon$. We let $\mathcal{I}=\text{Conv}\left(\left\{\lambda^{i}u\mid i\in\left\{0,\ldots,p\right\}\right\}\right)$. Since extremal points of $\mathcal{I}$ are of the form $\lambda^{i}u$, of modulus $|\lambda|^{i}\varepsilon<\varepsilon$, it holds that $\mathcal{I}\subseteq B(0,\varepsilon)$.

Let $d>1$, and assume the result known for smaller dimensions. We let $u$ be a complex number of modulus $\varepsilon/2$, for instance, $u=\varepsilon/2\in\mathbb{C}$ . We let $\alpha=|\lambda|^{p}\varepsilon$ which is such that $\alpha<\varepsilon$ and $B(0,\alpha)\subseteq\text{Conv}\left(\left\{\lambda^{i}u\mid i\in\left\{0,\ldots,p\right\}\right\}\right)$ and put $\varepsilon^{\prime}=\frac{\alpha}{2}(1-|\lambda|)$. We let $\mathcal{I}^{\prime}$ be a semilinear subset of $\mathbb{C}^{d-1}$ given by induction, stable for $\mathcal{J}_{d-1}(\lambda)$, and such that

[TABLE]

for some $\varepsilon^{\prime\prime}>0$. In particular, $0\in\pi_{1}(\mathcal{I}^{\prime})$.

We consider the sequence $(C_{j})_{j\in\mathbb{N}}$ of semilinear subsets of $\mathbb{C}$ given by $C_{0}=\{u\}$ and for all $j$,

[TABLE]

Let us know prove two facts about the sequence $(C_{j})_{j}$.

• •

For all $j$, and $z\in C_{j}$, $|z|\leq|\lambda|^{j}\frac{\varepsilon}{2}+\varepsilon^{\prime}\sum_{i=0}^{j-1}|\lambda|^{i}$, which we prove by induction. This is clear for $j=0$, and if it holds for elements $z\in C_{j}$, an element $\lambda z+z^{\prime}\in C_{j+1}$ with $z^{\prime}\in\pi_{1}(\mathcal{I}^{\prime})$ is such that

[TABLE]

• •

There exists $j_{0}$ such that $C_{j_{0}}\subseteq B(0,\alpha)\subseteq\text{Conv}\left(\{C_{0},\dots C_{j_{0}-1}\}\right)$. Indeed, the sequence $|\lambda|^{j}\frac{\varepsilon}{2}+\varepsilon^{\prime}\sum_{i=0}^{j-1}|\lambda|^{i}$ goes to $\frac{\varepsilon^{\prime}}{1-|\lambda|}$, so for large enough $j$, $C_{j}\subseteq B(0,\frac{2\varepsilon^{\prime}}{1-|\lambda|})=B(0,\alpha)$. Now $0\in\pi_{1}(\mathcal{I}^{\prime})$, so by an easy induction, $\lambda^{j}u\in C_{j}$. Hence,

[TABLE]

We now let

[TABLE]

Then

• •

$\mathcal{I}\subseteq B(0,\frac{\varepsilon}{2}+\frac{\varepsilon^{\prime}}{1-|\lambda|})\subseteq B(0,\frac{\varepsilon}{2}+\frac{\alpha}{2})\subseteq B(0,\varepsilon)$.

• •

$B(0,\min(\alpha,\varepsilon^{\prime\prime}))\subseteq\mathcal{I}$, and

• •

$\mathcal{I}$ is stable for $J$, because $J(C_{j}\times\mathcal{I}^{\prime})\subseteq C_{j+1}\times\mathcal{I}^{\prime}$.

This concludes the induction, and the proof of the Lemma.

We may now prove the following Theorem.

Theorem 0.D.1

Let $\ell=(x,A,y)$ be a normalized Orbit instance. Assume that $\ell$ is a non-reach instance. If the matrix $A$ has an eigenvalue whose modulus is smaller than 1, then there exists a semilinear invariant for $\ell$.

Proof

Let $J$ be a Jordan block of $A$ with eigenvalue $\lambda$ such that $|\lambda|<1.$ Since $\ell$ is normalized, $y_{J}\neq 0$. Let $\varepsilon=|y_{J}|/2$. Using Lemma 8, we obtain $\varepsilon^{\prime}>0$ and a semilinear set $\mathcal{I}\subseteq\mathbb{C}^{d(J)}$ such that $J\mathcal{I}\subseteq\mathcal{I}$ and $B(0,\varepsilon^{\prime})\subseteq\mathcal{I}\subseteq B(0,\varepsilon)$. Now $(A^{n}x)_{J}\to 0$, so there exists $n_{0}$ such that $(A^{n_{0}}x)_{J}\in B(0,\varepsilon^{\prime})\subseteq\mathcal{I}$. Hence, it is easy to see that

[TABLE]

is a semilinear invariant for $\ell$.

Appendix 0.E Some non-diagonalisable eigenvalue is a root of unity

Theorem 0.E.1

Let $\ell=(A,x,y)$ be a normalized Orbit instance. Assume that $\ell$ is a non-reach instance. If $A$ contains a non-diagonal Jordan block $J$ whose eigenvalue is a root of unity, then there exists a semilinear invariant for $\ell$.

Proof

Let $J$ be a non-diagonal Jordan block of $A$ with eigenvalue $\lambda$ with $\lambda^{m}=1$. We shall use divergence on the coordinate $(J,d(J)-1)$ to construct an invariant. Recall that $x_{J,d(J)}\neq 0$. For any $n\in\mathbb{N}$, we have $(A^{n}x)_{J,d(J)-1}=\lambda^{n}x_{J,d(J)-1}+n\lambda^{n-1}x_{J,d(J)}$, and $(A^{n}x)_{J,d(J)}=\lambda^{n}x_{J,d(J)}$. Hence,

[TABLE]

which goes to infinity when $n$ grows. Note that this condition is quadratic, but since $(A^{n}x)_{J,d(J)}$ takes only a finite number of values, we will be able to state it in a semilinear fashion. Let $n_{0}$ be such that $M=\text{Re}\left(\lambda(A^{n_{0}}x)_{J,d(J)-1}\overline{(A^{n_{0}}x)_{J,d(J)}}\right)>\text{Re}\left(\lambda y_{J,{d(J)-1}}\overline{y_{J,d(J)}}\right)$. Let

[TABLE]

where

[TABLE]

It is clear that $x\in\mathcal{I}$ and $y\notin\mathcal{I}$. Each $\mathcal{I}_{i}$ is semilinear because the second condition is actually semilinear assuming $z_{J,d(J)}=\lambda^{i}x_{J,d(J)}$. Now if $z\in\mathcal{I}_{i}$, we obtain that $(Az)_{J,d(J)}=\lambda z_{J,d(J)}=\lambda^{i+1}x_{J,d(J)}$, and

[TABLE]

so $Az\in\mathcal{I}_{i+1}$ if $i<m$, and $Az\in\mathcal{I}_{0}$ (since $\lambda^{m}=1)$ if $i=m$. Hence $\mathcal{I}$ is stable for $A$.

Appendix 0.F All eigenvalues have modulus 1 and are not roots of unity

We finally deal with the most involved case, namely, when all eigenvalues have modulus 1 and none are roots of unity. In this setting, we will be able to describe the minimal semilinear inviariant for $A$ and $x$, that is, a semilinear invariant which is contained in any semilinear invariant. We say that two eigenvalues are equivalent if their quotient is a root of unity. Intuitively, the only nontrivial semilinear relations that invariants will be able to exploit are the ones that hold among equivalent blocks.

We now give a high-level overview for this section.

• •

We first assume that eigenvalues are pairwise non-equivalent. The aim is to show that in this setting, any semilinear invariant is trivial. This is the object of subsection 0.F.1

• –

It is first shown how to deal with the diagonal case. This makes a crucial use of the Skolem-Mahler-Lech Theorem.

• –

We then extend to general (possibly non-diagonal) blocks by induction on the total dimension. This is the most technical part of the proof.

• •

We then deal with equivalent eigenvalues in subsection 0.F.2: we first treat the case where all equivalent eigenvalues are equal, and then show how to easily reduce to this setting.

0.F.1 All eigenvalues are non-equivalent

The diagonal case

We will make use of the following powerful theorem about linear recurrence sequences. This result is due to Skolem [30], and more general versions were subsequently obtained by Mahler [22, 23] and Lech [21].

Theorem 0.F.1 (Skolem, Mahler, Lech)

Let $(u_{n})_{n\in\mathbb{N}}$ be a real non-degenerate linear recurrence sequence, that is, $u_{n}=\sum_{i=1}^{d}v_{i}\lambda_{i}^{n}$, for some $v\in\mathbb{C}^{d}\setminus\{0\}$, where for any $i\neq j$, $\frac{\lambda_{i}}{\lambda_{j}}\notin\mathbb{U}$. Then $\left\{n\in\mathbb{N}\mid u_{n}=0\right\}$ is finite.

We write $A=\text{Diag}(\lambda_{1},\ldots,\lambda_{d})$ for

[TABLE]

Lemma 9

Let $\lambda_{1},\ldots,\lambda_{d}\in S^{1}$ and $A=\text{Diag}(\lambda_{1},\ldots,\lambda_{d})$. Assume that:

• •

for all $i$, we have $\lambda_{i}\notin\mathbb{U}$, and

• •

for all $i,j$ such that $i\neq j$, we have $\frac{\lambda_{i}}{\lambda_{j}}\notin\mathbb{U}$.

Let $\mathcal{I}$ be a non-empty closed semilinear set stable under $A$, which moreover containes a point $x\in\mathcal{I}$ such that for all coordinate $i$, $x_{i}\neq 0$. Then $\mathcal{I}=\mathbb{C}^{d}$.

Proof

Let $\mathcal{I}$ be such a semilinear set, we show a few facts:

• $(i)$

$\mathcal{I}$ must have even dimension over $\mathbb{R}$,

• $(ii)$

$\mathcal{I}$ must have dimension $>2d-2$ over $\mathbb{R}$ (hence, $\mathcal{I}$ has full dimension thanks to $(i)$),

• $(iii)$

$\partial\mathcal{I}$ is stable under $A$,

• $(iv)$

if it is non-empty (that is, if $\mathcal{I}\neq\mathbb{C}^{d}$), $\partial\mathcal{I}$ contains a point which is nonzero on each coordinate.

This implies the desired result: if towards contradiction we would have that $\mathcal{I}\neq\mathbb{C}^{d}$, then $\partial\mathcal{I}$ would be a non-empty closed semilinear set stable under $A$ thanks to $(iii)$, it would contain a point which is nonzero on each coordinate thanks to $(iv)$, but yet it cannot have full dimension. We now prove the four claims.

• $(i)$

Let $s=\dim_{\mathbb{R}}(\mathcal{I})$. Then $\mathcal{I}$ is contained into the union of finitely many affine subspaces of dimension $s$, write

[TABLE]

where $F_{i}\subseteq\mathbb{C}^{d}\simeq\mathbb{R}^{2d}$ is a real affine space of dimension $s$, of direction $F_{i}-F_{i}=E_{i}\subseteq\mathbb{R}^{2d}$. We first show that for some $i$, $E_{i}$ must be stable for some power of $A$ (seen as a transformation of $\mathbb{R}^{2d}$), and then that this implies that $s$ is even.

Since $\dim_{\mathbb{R}}(\mathcal{I})\geq s$, there must be $\tilde{x}\in\mathcal{I}$ and $\varepsilon>0$ such that

[TABLE]

for some $i$. Then for all $n$, $A^{n}(B(\tilde{x},\varepsilon)\cap F_{i})=B(A^{n}\tilde{x},\varepsilon)\cap A^{n}F_{i}\subseteq\mathcal{I}$, and has dimension $s$ over $\mathbb{R}$, hence there exists $i_{n}$ such that $B(A^{n}\tilde{x},\varepsilon)\cap\mathcal{I}=B(A^{n}\tilde{x},\varepsilon)\cap F_{i_{n}}$. Now let $n_{1}<n_{2}$ be such that $i_{n_{1}}=i_{n_{2}}=i,$ let $n=n_{2}-n_{1}$ and let $x=A^{n_{1}}\tilde{x}$. We show that $E_{i}$ is stable under $A^{n}$.

Let $e\in E_{i}$, and let $\tilde{e}=\varepsilon\frac{e}{2||e||}$. Then $x+\tilde{e}\in B(x,\varepsilon)\cap F_{i}\subseteq\mathcal{I}$ so $A^{n}(x+\tilde{e})=A^{n}x+A^{n}\tilde{e}\in B(A^{n}x,\varepsilon)\cap\mathcal{I}\subseteq F_{i}$ so $A^{n}\tilde{e}=A^{n}x+A^{n}\tilde{e}-A^{n}x\in F_{i}-F_{i}=E_{i}$ and since $E_{i}$ is $\mathbb{R}$-linear, $A^{n}e\in E_{i}$.

Now since the $\lambda_{i}$’s are not roots of $1$, $A^{n}$, when seen as a transformation of $R^{2d}$, is the product of $d$ diagonal irrationnal rotations of $\mathbb{R}^{2}$. Such a map only stabilizes linear spaces of even dimensions, hence $s=\dim_{\mathbb{R}}(E_{i})$ is even.

• $(ii)$

Assume for contradiction that $\dim_{\mathbb{R}}(\mathcal{I})\leq 2d-2$. Let $x\in\mathcal{I}$ be a point with $x_{i}\neq 0$ for all $i\in\{1,\dots,d\}$. Now $\mathcal{I}\subseteq\bigcup_{i=1}^{p}F_{i}$, where the $F_{i}$’s are affine spaces of real dimension $2d-2$, that is, spaces of the form

[TABLE]

for some nonzero $u\in\mathbb{C}^{d}$ and some $a\in\mathbb{C}$. Consider the orbit $\mathcal{O}=\{A^{n}x,n\in\mathbb{N}\}$ of $x$. There must be $i$ such that $F_{i}\cap\mathcal{O}$ is infinite, hence there are infinitely many $n\in\mathbb{N}$ such that

[TABLE]

which contradicts Theorem 0.F.1 applied to eigenvalues $\lambda_{1},\dots,\lambda_{d},1$, since $u\neq 0$ implies $(u_{i}x_{i})_{i\in\{1,\dots,d\}}\neq 0$.

• •

$(iii)$ We argue that $\mathbb{C}^{d}\setminus\mathcal{I}$ is stable under $A$, which together with the fact that $\mathcal{I}$ is stable under $A$ implies that $\partial\mathcal{I}$ is stable under $A$. Equivalently we show that $\mathcal{I}$ is stable under $A^{-1}$: let $x$ in $\mathcal{I}$, we prove that $A^{-1}x$ is in $\mathcal{I}$.

Let

[TABLE]

be the set of all multiplicative relations holding among $\lambda_{1},\ldots,\lambda_{d}$. Notice that $L_{A}$ is an additive subgroup of $\mathbb{Z}^{d}$. Consider the set of diagonal $d\times d$ matrices

[TABLE]

whose diagonal entries satisfy the multiplicative relations in $L_{A}$. Using Kronecker’s Theorem on inhomogeneous simultaneous Diophantine approximation [5], it is shown in [28, Proposition 3.5] that $\left\{A^{n}:n\in\mathbb{N}\right\}$ is a dense subset of ${T}_{A}$. This immediately gives

[TABLE]

Since $x$ is in $\mathcal{I}$ and $\mathcal{I}$ is stable under $A$, we have that $\overline{\left\{A^{n}x\mid n\in\mathbb{N}\right\}}\subseteq\overline{\mathcal{I}}=\mathcal{I}$. Observe furthermore that $A^{-1}=\text{Diag}(\lambda_{1}^{-1},\ldots,\lambda_{d}^{-1})$ is in ${T}_{A}$, so thanks to the previous equality $A^{-1}x$ is in $\mathcal{I}$.

• •

$(iv)$ Let $\mathcal{Q}=\bigcup_{i=1}^{d}\mathbb{C}^{i-1}\times\{0\}\times\mathbb{C}^{d-i}$ be the set of points with at least one zero coordinate. Assume for contradiction that $\partial\mathcal{I}\subseteq\mathcal{Q}$. Let $x\in\mathcal{I}\setminus\mathcal{Q}$ and $y\in\mathcal{I}^{\mathsf{c}}\setminus\mathcal{Q}$, which is non-empty because $\mathcal{I}^{\mathsf{c}}$ is a nonempty open subset of $\mathbb{C}^{d}$ whereas $\mathcal{Q}$ has empty interior. Now $\mathbb{C}^{d}\setminus\mathcal{Q}$ is path connected, so there exists a path from $x$ to $y$ which avoids $\mathcal{Q}\supseteq\partial\mathcal{I}$, a contradiction.

Although $\forall i,x_{i}\neq 0$ holds in a normalized instance, we shall need a slightly stronger result which is a consequence of the previous Lemma.

Theorem 0.F.2

Let $A=\text{Diag}(\lambda_{1},\dots\lambda_{d})$ with $\lambda_{i}\notin\mathbb{U}$ and for $i\neq j,\frac{\lambda_{i}}{\lambda_{j}}\notin\mathbb{U}$. Let $\mathcal{I}\subseteq\mathbb{C}^{d}$ be a closed semilinear set such that $A\mathcal{I}\subseteq\mathcal{I}$. Then $\mathcal{I}$ is a union of sets of the form

[TABLE]

where $\varepsilon_{i}\in\{\{0\},\mathbb{C}\}$.

Proof

We show that for any $x\in\mathcal{I}$, $\mathcal{I}$ must contain $\prod_{i}\varepsilon_{i}$, with $\varepsilon_{i}=\begin{cases}\{0\}\text{ if }x_{i}=0\\ \mathbb{C}\text{ otherwise}\end{cases}$, which implies the wanted result. This is an easy application of the previous Lemma to the projection of $\mathcal{I}\cap\prod_{i}\varepsilon_{i}$ on coordinates $\{i\mid x_{i}\neq 0\}$.

General case

We now work with a general (not necessarily diagonal) matrix $A$, whose eignvenvalues are not roots of unity and pairwise non equivalent. The following theorem is proved by induction on $d=\sum d_{i}$. We write $\mathcal{J}$ for the set of jordan blocks of $A$, and $s=|\mathcal{J}|$.

Theorem 0.F.3

Semilinear invariants for $A$ are unions of sets of the form

[TABLE]

where for each $J$, $p_{J}$ is an integer in $\{0,\dots,d(J)\}$.

Recall that if $S\subseteq\{(J,i),J\in\mathcal{J},i\leq d(J)\}$ is a subset of dimensions, $\pi_{S}:\mathbb{C}^{d}\to\mathbb{C}^{S}$ denotes the projection on the coordinates in $S$. We let $\text{last}=\{(J,d(J)),J\in\mathcal{J}\}$ be the set of last coordinates of each block, and for each $J$, we let $P_{J}=\pi_{\{(J,d(J))\}}^{-1}(\{0\})\subseteq\mathbb{C}^{d}$. Note that any set of the form $\prod_{J}\mathbb{C}^{p_{J}}\times\{0\}^{d(J)-p_{J}}$ which is not $\mathbb{C}^{d}$, is included in $\cup_{J}P_{J}$.

The case $d=1$ is proved in section 0.F.

We start the induction with an intermediate result.

Lemma 10

A semilinear invariant for $A$ is either a union of sets of the form $\prod_{J\in\mathcal{J}}\mathbb{C}^{p_{J}}\times\{0\}^{d(J)-p_{J}}$, or contains $\pi_{last}^{-1}(\{0\})=\prod_{J}\mathbb{C}^{d(J)-1}\times\{0\}=\mathcal{Q}.$

Proof

Let $\mathcal{I}$ be a semilinear invariant for $A$. Consider $\mathcal{I}^{\prime}=\pi_{\text{last}}(\mathcal{I})\subseteq\mathbb{C}^{s}$. If $S^{\prime}\subseteq\mathcal{J}$, we let $\pi^{\prime}_{S^{\prime}}:\mathbb{C}^{s}\to\mathbb{C}^{S^{\prime}}$ denote the projection on the coordinates of $\mathbb{C}^{s}$ corresponding to last coordinates of blocks from $S^{\prime}$. Just like previously, let $P^{\prime}_{J}={\pi^{\prime}}_{J}^{-1}(\{0\})\subseteq\mathbb{C}^{s}$. Since $\mathcal{I}^{\prime}$ is stable for $\text{Diag}(\lambda_{1},\dots,\lambda_{s})$, it must be that $\mathcal{I}^{\prime}$ is either $\mathbb{C}^{s}$, or $\mathcal{I}^{\prime}\subseteq\cup P^{\prime}_{J}$, by Theorem 0.F.2. We reduce to the former case.

Indeed, if $\mathcal{I}^{\prime}\subseteq\cup P^{\prime}_{J}$, we let $\mathcal{I}_{J}=\pi_{\text{last}}^{-1}(P^{\prime}_{J})$, so that $\mathcal{I}=\cup\mathcal{I}_{J}.$ Now, $\mathcal{I}_{J}\subseteq P_{J}$, so $\pi_{\{(J,d(J))\}^{\mathsf{c}}}(\mathcal{I}_{J})$ is stable for the matrix $A^{\prime}$ obtained from $A$ just by diminishing the dimension of block $J$ by 1. By induction, $\pi_{\{(J,d(J))\}^{\mathsf{c}}}(\mathcal{I}_{J})$ is a union of sets of the form $\prod_{J^{\prime}\in\mathcal{J}^{\prime}}\mathbb{C}^{p_{J^{\prime}}}\times\{0\}^{d(J^{\prime})-p_{J^{\prime}}}$ (where $\mathcal{J}^{\prime}$ is the set of Jordan blocks of $A^{\prime}$), so $\mathcal{I}_{J}$ has the wanted form, and so does $\mathcal{I}=\cup I_{J}$.

Hence we assume that $\mathcal{I}^{\prime}=\mathbb{C}^{s}.$ We aim to show that $\mathcal{I}\supseteq\mathcal{Q}$, or equivalentely, $\pi_{\text{last}^{\mathsf{c}}}(\mathcal{I}\cap\mathcal{Q})=\mathbb{C}^{d-s}.$ By induction, since it is stable for the matrix obtained from $A$ by diminishing the dimension of each block by 1, we know that either $\pi_{\text{last}^{\mathsf{c}}}(\mathcal{I}\cap\mathcal{Q})=\mathbb{C}^{d-s},$ or $\pi_{\text{last}^{\mathsf{c}}}(\mathcal{I}\cap\mathcal{Q})\subseteq\cup_{J}\pi_{\{(J,d(J)-1)\}}^{-1}(\{0\}).$ We assume the latter towards contradiction. In plain English, any $z\in\mathcal{I}$ that is [math] on the last coordinate of each block (that is, $z\in\mathcal{I}\cap\mathcal{Q}$) must have one of its prior coordinates (that is, $(J,d(J)-1)$ for some $J$) which is zero. We will now project on only the last two coordinates of each block. Formally, we let

[TABLE]

and consider $\mathcal{I}^{\prime\prime}=\pi_{\text{last-two}}(\mathcal{I})$. Then $\mathcal{I}^{\prime\prime}$ is stable for $A^{\prime\prime}$, the matrix obtained from $A$ by reducing the size of each block of size $\geq 3$ to 2. We let $\mathcal{J}^{\prime\prime}$ denote the set of Jordan blocks of $A^{\prime\prime}$. In particular, any $J^{\prime\prime}\in\mathcal{J}^{\prime\prime}$ is such that $d(J^{\prime\prime})\in\{1,2\}$.

For each $J^{\prime\prime}\in\mathcal{J}^{\prime\prime}$, we let $(z_{J^{\prime\prime},d(J^{\prime\prime})}^{(n)})_{n\in\mathbb{N}}$ be a decreasing sequence of complex numbers that goes to [math], and such that for any given $n$, the moduli of the $z_{J^{\prime\prime},d(J^{\prime\prime})}^{(n)}$ are all equal. Since $\mathcal{I}^{\prime}=\mathbb{C}^{s}$, for all $n\in\mathbb{N}$ and each $J^{\prime\prime}$ such that $d(J^{\prime\prime})=2$ there exists $z_{J^{\prime\prime},1}^{(n)}$ such that $z^{(n)}\in\mathcal{I}^{\prime\prime}$. By Lemma 2, we may pick these values such that $z^{(n)}$ is bounded. Up to extracing a subsequence, we assume without loss of generality that $z^{(n)}$ converges, to, say, $z\in\mathcal{I}^{\prime\prime}$. Since $z_{J^{\prime\prime},d(J^{\prime\prime})}=0$ for all $J^{\prime\prime}\in\mathcal{J}^{\prime\prime}$, $z\in\pi_{\text{last-two}}(\mathcal{I}\cap\mathcal{Q})$, so there must exist $J^{\prime\prime}_{0}$ with $d(J^{\prime\prime}_{0})=2$ such that $z_{J^{\prime\prime}_{0},1}=0$. We let $\lambda_{0}$ be the eigenvalue of block $J^{\prime\prime}_{0}$. We put $\delta=\min\left(1,\min_{\{J^{\prime\prime}\mid d(J^{\prime\prime})=2\text{ and }z_{J^{\prime\prime},1}\neq 0\}}\{|z_{J^{\prime\prime},1}|\}\right)>0$. We let $n$ be large enough so $||z^{(n)}-z||\leq\delta/4$. Consider $({A^{\prime\prime}}^{k}z^{(n)})_{J^{\prime\prime}_{0},1}=\lambda_{0}^{n}(z_{J^{\prime\prime}_{0},1}^{(n)}+k\lambda_{0}^{-1}z_{J^{\prime\prime}_{0},2}^{(n)})$. Let $k(n)=\left\lceil\frac{\delta}{2|z_{J^{\prime\prime}_{0},2}^{(n)}|}\right\rceil$. Note that $k(n)$ does not depend on the choice of $J^{\prime\prime}_{0}$ since the $z_{J^{\prime\prime},d(J^{\prime\prime})}^{(n)}$ all have the same moduli. Then

[TABLE]

Likewise, we may bound away from zero (which is the reason motivating the choice of $\delta$), and also from above, the moduli of $({A^{\prime\prime}}^{k(n)}z^{(n)})_{J^{\prime\prime}_{1},1}$ when $J^{\prime\prime}_{1}$ is such that $z_{J^{\prime\prime}_{1},1}\neq 0$. More precisely,

[TABLE]

Now, $\mathcal{I}^{\prime\prime}$ being stable for $A^{\prime\prime}$, the sequence $({A^{\prime\prime}}^{k(n)}z^{n})_{n}$ has its elements in $\mathcal{I}^{\prime\prime}$, and ultimately lies in the compact

[TABLE]

We may then extract a converging subsequence in $K$, with its limit in $\mathcal{I}^{\prime\prime}$ such that the last coordinate of each block is zero whereas the previous one is nonzero, a contradiction. This concludes the proof of the Lemma.

With Lemma 10 in hands, we now move on to the proof of Theorem 0.F.3.

Proof

Let us assume for contradiction that $\mathcal{I}$ is not in the form of the statement of the Theorem. In particular, $\mathcal{I}\neq\mathbb{C}^{s}$. By Lemma 10, $\mathcal{Q}\subseteq\mathcal{I}.$ The set $\mathcal{I}$ is a finite union of closed polyhedra, write $\mathcal{I}=\bigcup_{\mathcal{P}\in P}\mathcal{P}.$ Each polyhedron $\mathcal{P}$ is a finite intersection of closed half-spaces, write $\mathcal{P}=\bigcap_{\mathcal{H}\in H_{\mathcal{P}}}\mathcal{H}.$ Let $H=\bigcup_{\mathcal{P}\in P}\mathcal{H}_{\mathcal{P}}$.

We start with a restriction: we may restrict to the case where there is a polyhedron $\mathcal{P}_{0}\in P$ such that $\mathcal{P}_{0}\cap\mathcal{Q}$ has dimension (over $\mathbb{R}$) $2(d-s)$, and $\mathcal{P}_{0}$ is not included in $\mathcal{Q}$.

Let $P_{full}$ denote the set of polyhedra $\mathcal{P}$ in $P$ such that $\mathcal{P}\cap\mathcal{Q}$ has dimension $2(d-s)$. Since $\mathcal{Q}\subseteq\mathcal{I},$ $P_{full}\neq\emptyset$. Assume that for each polyhedron $\mathcal{P}$ of $P_{full}$ we have $\mathcal{P}\subseteq\mathcal{Q}$. Let

[TABLE]

Since $\mathcal{I}^{\prime}\cap\mathcal{Q}$ has dimension at most $2(d-s)-1<\dim_{\mathbb{R}}(\mathcal{Q})$, it may not be the case that $\mathcal{Q}\subseteq\mathcal{I}^{\prime}$. Now $\mathcal{Q}^{\mathsf{c}}$ is stable for $A$, so so is $\mathcal{I}^{\prime}$. Hence $\mathcal{I}^{\prime}$ is, by Lemma 10 in the form of the Theorem. Finally, $I=\mathbb{Q}\cup\mathcal{I}^{\prime\prime}$ is in the wanted form. Hence, we now assume the existence of $\mathcal{P}_{0}\in P_{full}$ which is not contained in $\mathcal{Q}$.

Let $H_{general}$ be the family of half-spaces in $H$ which are not of the form $\pi_{\text{last}}^{-1}(\mathcal{H}^{\prime})$ where $\mathcal{H}^{\prime}$ is a half-space of $\mathbb{C}^{s}$ with $0\in\partial\mathcal{H}^{\prime}$. Equivalentely, half-spaces in $H_{general}$ are those which do not contain $\mathcal{Q}$ in their border. Now if $\mathcal{H}\in H_{general}$ then $\partial\mathcal{H}\cap\mathcal{Q}$ has dimension $<2(d-s)$.

It follows that the countable union $\bigcup_{\mathcal{H}\in H_{general}}\bigcup_{k\in\mathbb{N}}A^{-k}\partial\mathcal{H}\cap\mathcal{Q}$ has dimension $<2(d-s)$, so it may not cover $\mathcal{P}_{0}\cap\mathcal{Q}$. Let $z\in\mathcal{P}_{0}\cap\mathcal{Q}$ be out of this union.

Let $k$ in $\mathbb{N}$. We choose $\varepsilon_{k}>0$ such that for each $\mathcal{H}\in H$, the set $B(A^{k}z,\varepsilon_{k})\cap\mathcal{H}$ is either empty, the whole ball $B(A^{k}z,\varepsilon_{k})$, or a half-ball of the form $B(A^{k}z,\varepsilon_{k})\cap\pi_{\text{last}}^{-1}(\mathcal{H}^{\prime})$, where $\mathcal{H}^{\prime}$ is a half-space of $\mathbb{C}^{s}$ such that $0\in\partial\mathcal{H}^{\prime}.$ This is achieved by the following case disctinction:

• •

Either $A^{k}z$ is in ${\kern 0.0pt\mathcal{H}}^{\mathrm{o}},$ then there exists $\varepsilon_{k}>0$ such that $B(A^{k}z,\varepsilon_{k})\cap\mathcal{H}=B(A^{k}z,\varepsilon_{k}).$

• •

Or $A^{k}z$ is in $\partial\mathcal{H}$. Recall that by construction $A^{k}z$ is not in $\partial\mathcal{H}$ for $\mathcal{H}$ in $H_{general}$, so $\mathcal{H}\notin H_{general}$ and we are in the third case.

• •

Or $A^{k}z$ is not in $\mathcal{H}$, in which case there exsits $\varepsilon_{k}>0$ such that $B(A^{k}z,\varepsilon_{k})\cap\mathcal{H}=\varnothing.$

Without loss of generality, we pick $(\varepsilon_{k})_{k}$ to be decreasing.

It follows that for a polyhedron $\mathcal{P}\in P$, its trace on $B(A^{k}z,\varepsilon_{k})$ is either empty or of the form

[TABLE]

where $H_{\mathcal{P}}^{k}$ is a finite set of closed half-spaces $\mathcal{H}$ of $\mathbb{C}^{s}$ such that $0\in\partial\mathcal{H}$. For $\mathcal{P}\in P$, let $C_{\mathcal{P},k}=\bigcap_{\mathcal{H}\in H_{\mathcal{P}}^{k}}\mathcal{H}$ and $C_{k}=\bigcup_{\mathcal{P}\in P}C_{\mathcal{P},k}$. By construction, forall $k\in\mathbb{N}$,

[TABLE]

We make three claims.

• •

$C_{k}$ has full dimension (over $\mathbb{R}$) $2s$. Indeed, since $z$ avoids $\bigcup_{\mathcal{H}\in H_{general}}\partial\mathcal{H}$, and $\dim_{\mathbb{R}}(\mathcal{P}_{0}\cap Q)=2s$, $C_{0}$ has full dimension. Since $\text{Diag}\{\lambda_{1},\dots,\lambda_{s}\}C_{k}\subseteq C_{k+1}$, the claim follows by a easy induction.

• •

$C_{k}$ is not all of $\mathbb{C}^{s}$. For this, let us consider $\overline{\mathcal{I}^{\mathsf{c}}},$ a closed semilinear set which is stable for $A^{-1}$. Under an appropriate diagonal change of basis, which, in particular, stabilizes any set of of form $\prod_{J\in\mathcal{J}}\mathbb{C}^{p_{J}}\times\{0\}^{d(J)-p_{J}}$, $A^{-1}$ rewrites as $\text{Diag}(\mathcal{J}_{d(J)}(\lambda_{J}^{-1}),J\in\mathcal{J}).$ Hence Lemma 10 applies to $\overline{\mathcal{I}^{\mathsf{c}}}$. Since $\mathcal{I}\neq\mathbb{C}^{s}$, $\mathcal{I}^{\mathsf{c}}$ is nonempty, and since it is an open set, it must be fully dimensional. Hence, either $\overline{\mathcal{I}^{\mathsf{c}}}\subseteq\mathcal{Q}$, that is, each point of $Q$ (in particular, $A^{k}z$) has arbitrary close points that are not in $\mathcal{I}$, which implies the claim.

• •

There are finitely many different sets $C_{k}$ for $k$ in $\mathbb{N}$. Indeed, $C_{k}$ is determined by finitely many queries, namely whether $A^{k}z$ is in ${\kern 0.0pt\mathcal{H}}^{\mathrm{o}},\partial\mathcal{H}$ or not in $\mathcal{H}$, for each $\mathcal{H}$ in $H$. Note that on the other hand, $\varepsilon_{k}$ does depend on $k$, and may take arbitrarily small values if $A^{k}z$ gets arbitrarily close to some $\mathcal{H}$ in $H$ when $k$ ranges in $\mathbb{N}$.

As previously stated, $\{(\lambda_{1}^{k},\dots,\lambda_{s}^{k}),k\in\mathbb{N}\}$ is dense in $\{(\lambda_{1}^{t},\dots,\lambda_{s}^{t}),t\in\mathbb{R}\}\subseteq T_{A}$. Hence, there exists an increasing sequence $\varphi:\mathbb{N}\to\mathbb{N}$ and $\varepsilon_{k}/2\leq\mu_{k}\leq\varepsilon_{k}$ such that forall $k$, $(\lambda_{1}^{\varphi(k)},\dots,\lambda_{s}^{\varphi(k)})=(\lambda_{1}^{\mu_{k}},\dots,\lambda_{s}^{\mu_{k}})$. Let $C$ be such that $C=C_{\varphi(k)}$ for infinitely many $k$. Combining the diagonal case from section 0.F, the fact that $C$ has full dimension, and that $C$ is not $\mathbb{C}^{s}$, we know that $C$ cannot stabilize $\text{Diag}(\lambda_{1},\dots,\lambda_{s})$. In particular, there is $\tilde{u}\in C$ such that $\text{Diag}(\lambda_{1},\dots,\lambda_{s})\tilde{u}\notin C$. Let $t_{0}=\inf\{t\leq 1,\text{Diag}(\lambda_{1}^{t},\dots,\lambda_{s}^{t})\tilde{u}\notin C\}\geq 0$, and $u=\text{Diag}(\lambda_{1}^{t_{0}},\dots,\lambda_{s}^{t_{0}})\tilde{u}\in C$, since $C$ is closed. Note that for any small enough $\varepsilon>0,\text{Diag}(\lambda_{1}^{\varepsilon},\dots,\lambda_{s}^{\varepsilon})u\notin C$. We let $N\in\mathbb{N}$ be such that for $n\geq N$, $\varepsilon_{n}$ is small enough in this sense, and $N^{\prime}$ be such that $\varphi(N^{\prime})-\varphi(0)\geq N$. Recall that $C$ is defined using half-spaces which contain [math] in their border, hence it is invariant under multiplication by positive reals (a cone). Hence we may assume that $||u||\leq 2^{-\varphi(N^{\prime})}\varepsilon_{\varphi(N^{\prime})}$.

We may finaly give the last construction. Let $v\in B(A^{\varphi(0)}z,2^{-\varphi(N^{\prime})}\varepsilon_{\varphi(N^{\prime})})\cap\pi_{last}^{-1}(\{u\})\subseteq B(A^{\varphi(0)}z,\varepsilon_{\varphi(0)})\cap\pi_{\text{last}}^{-1}(C)\subseteq\mathcal{I}$. We argue that $A^{\varphi(N^{\prime})-\varphi(0)}v\in B(A^{\varphi(N^{\prime})}z,\varepsilon_{\varphi(N^{\prime})})$. Indeed, $A$ is $2$-lipschitzian, so $A^{\varphi(N^{\prime})-\varphi(0)}$ is $2^{\varphi(N^{\prime})}$-lipschitzian, so

[TABLE]

Hence, $A^{\varphi(N^{\prime})-\varphi(0)}v\in B(A^{\varphi(N^{\prime})}z,\varepsilon_{\varphi(N^{\prime})})\cap\mathcal{I}=B(A^{\varphi(N^{\prime})}z,\varepsilon_{\varphi(N^{\prime})})\cap\pi_{\text{last}}^{-1}(C)$, but $\pi_{\text{last}}(A^{\varphi(N^{\prime})-\varphi(0)}v)=\text{Diag}(\lambda_{1}^{\varphi(N^{\prime})},\dots,\lambda_{s}^{\varphi(N^{\prime})})u=\text{Diag}(\lambda_{1}^{\mu_{N^{\prime}}},...,\lambda_{s}^{\mu_{N^{\prime}}})$, and since $\mu_{N^{\prime}}\leq\varepsilon_{N^{\prime}}\leq\varepsilon_{N},$ we obtain that $\pi_{\text{last}}(A^{\varphi(N^{\prime})-\varphi(0)}v)\notin C,$ a contradiction.

Note that Theorem 0.F.3 gives a minimal semilinear invariant for $A$ which contains a given $x\in\mathbb{C}^{d}$, namely,

[TABLE]

where $p_{J}=\max\{i\leq d(J)\mid x_{J,i}\neq 0\}$. In particular, if the instance is reduced, $x_{J,d(J)}\neq 0$ so the minimal seminlinear invariant is $\mathbb{C}^{d}$.

0.F.2 Some eigenvalues may be equivalent

We will show that this case reduces to the previous one. We first deal with the case where all equivalent eigenvalues are in fact equal, which we then extend to the general case. Let us start with a Lemma.

Lemma 11

Let

[TABLE]

and $x=(x^{\prime\prime},x_{1},x_{2})\in\mathbb{C}^{s}$ with $s=s^{\prime\prime}+d_{1}+d_{2}$, $s^{\prime\prime}$ being the dimension of $A^{\prime\prime}$ (hence $s$ is the dimension of $A$). The $i-th$ coordinate of $x$ in the $\mathcal{J}_{d_{1}}(\lambda)$ block (resp. in the $\mathcal{J}_{d_{2}}(\lambda)$ block) is denoted $x_{1,i}$ (resp. $x_{2,i}$). We assume that $x_{1,d_{1}}\neq 0$ and let

[TABLE]

of size $s^{\prime}=s-1,$ where $E_{d_{2}-1,d_{1}}$ denotes the matrix with $d_{2}-1$ rows and $d_{1}$ columns with a single 1 in the bottom right corner. We let $x^{\prime}=(x^{\prime\prime},x_{1},x^{\prime}_{2})$ be given by $x^{\prime}_{2}=(x_{2,1},x_{2,2}\dots,x_{2,d_{2}-1})$. We assume that $\mathcal{I}^{\prime}\subseteq\mathbb{C}^{s^{\prime}}$ is a minimal semilinear invariant for $A^{\prime}$ and $x^{\prime}$. Then

[TABLE]

is a minimal semilinear invariant for $x,A$.

Before going on to the proof, let us remark that if $d_{2}=1$, $E_{d_{2}-1,d_{1}}$ and $J_{d_{2}-1}(\lambda)$ are both empty matrices (and the Lemma also holds).

Proof

Clearly $x\in\mathcal{I}$. Let us first check that $\mathcal{I}$ is invariant for $A$. Let $z\in\mathcal{I}$. Then

[TABLE]

and $x_{1,d_{1}}(Az)_{2,d_{2}}=x_{1,d_{1}}\lambda z_{2,d_{2}}=x_{2,d_{2}}\lambda z_{1,d_{1}}=x_{2,d_{2}}(Az)_{1,d_{1}}$. Hence $\mathcal{I}$ is invariant for $A$.

We now show minimality. Let $\mathcal{P}$ be a semilinear invariant containing $x$. Consider $\mathcal{P}_{0}=\mathcal{P}\cap\{z\mid x_{1,d_{1}}z_{2,d_{2}}=x_{2,d_{2}}z_{1,d_{1}}\}$, and $\mathcal{P}_{0}^{\prime}\subseteq\mathbb{C}^{s^{\prime}}$ be its projection on all but the last coordinate. We show that $\mathcal{P}_{0}^{\prime}$ is invariant for $A^{\prime}$. Let $z^{\prime}\in\mathcal{P}_{0}^{\prime}$, and let $z$ be $z^{\prime}$ extended with $z_{2,d_{2}}=\frac{x_{2,d_{2}}}{x_{1,d_{1}}}z_{1,d_{1}}$. Then $z\in\mathcal{P}_{0}$, so $Az\in P_{0}$. Now, $A^{\prime}z^{\prime}=(Az)^{\prime}$ (the proof for this is similar as that of $\mathcal{I}$’s stability), and so $A^{\prime}z^{\prime}\in P_{0}^{\prime}$. Hence, $\mathcal{I}^{\prime}\subseteq P_{0}^{\prime}$ by minimality of $\mathcal{I}^{\prime}$, and so $\mathcal{I}\subseteq\mathcal{P}_{0}\subseteq P$.

Through repeated applications of Lemma 11 which reduce the dimension and Lemma 5 which renormalize the reduced instance, we obtain the following Theorem.

Theorem 0.F.4

Let $A$ have its eigenvalues $\lambda_{1},\dots,\lambda_{s}\notin\mathbb{U}$ such that either $\lambda_{i}=\lambda_{j}$ or $\lambda_{i}/\lambda_{j}\notin\mathbb{U}$, and $x\in\mathbb{C}^{s}$ which is nonzero on the last coordinate of each block. Then there exists a minimal semilinear invariant for $A,x$ which can be constructed in polynomial time and has polynomial size.

Proof

If forall $i\neq j$, $\lambda_{i}\neq\lambda_{j}$, then they are pairwise non-equivalent, so by Theorem 0.F.3, $\mathbb{C}^{s}$ is the minimal invariant for $A$ and $x$. Otherwise, we use Lemma 11 on blocks with equal eigenvalues to reduce the dimension, and Lemma 5 to normalize the instance (ensuring that $A$ is in Jordan normal form and $x$ is nonzero on the last coordinate of each bloc), and easily conclude by induction.

We may now finally extend to the general case.

Theorem 0.F.5

Let $A$ have only eigenvalues of modulus 1 which are not roots of unity, and $x\in\mathbb{C}^{s}$ with nonzero last coordinates. Then there is an explicit minimal semilinear invariant $\mathcal{I}$ for $A$ and $x$. In particular, there is a semilinear invariant (namely, $\mathcal{I}$) for $\ell=(A,x,y)$ if and only if $y\notin\mathcal{I}$, which may be decided algorithmically.

Proof

Let $N\in\mathbb{N}$ be such that $A^{N}$ is just like in the statement of Theorem 0.F.4. Let $\mathcal{I}_{0}$ be the minimal semilinear invariant for $A^{N}$ and $x$. Let

[TABLE]

Clearly, $\mathcal{I}$ is semilinear, contains $x$, and invariant for $A$. Let $\mathcal{P}$ be a semilinear invariant for $A$ which contains $x$. Then it is also invariant for $A^{N}$, so $\mathcal{I}_{0}\subseteq\mathcal{P}$. It follows that $A\mathcal{I}_{0},A^{2}\mathcal{I}_{0},\dots\subseteq\mathcal{P}$, which concludes our proof.