In the following, we work with vectors and matrices whose entries are rational numbers. Inequalities between such vectors are understood to be coordinatewise: e.g., two vectors $a = \left(a\_1,a\_2,\ldots,a\_n\right)^T$ and $b = \left(b\_1,b\_2,\ldots,b\_n\right)^T$ are said to satisfy $a > b$ if and only if each $i \in \left\{1,2,\ldots,n\right\}$ satisfies $a\_i > b\_i$.



> 
> **Theorem 1.** Let $n$ be a positive integer. Let $A$ be an $n\times n$-matrix whose entries are nonnegative rational numbers. Then, there exists a nonzero vector $v \in \mathbb{Q}^n$ with nonnegative coordinates such that either $Av \geq v$ or $Av < v$.
> 
> 
> 


The next theorem concerns a more restricted class of matrices. If $A$ is an $n\times n$-matrix whose entries are nonnegative rational numbers, then we define $D\_A$ to be the directed graph whose vertices are the numbers $1,2,\ldots,n$, and which has an arc from vertex $i$ to vertex $j$ if and only if the $\left(i,j\right)$-th entry of $A$ is positive. We say that the matrix $A$ is *irreducible* if and only if this digraph $D\_A$ is strongly connected. (Other equivalent definitions of irreducibility appear [on the Wikipedia page for Perron-Frobenius](https://en.wikipedia.org/wiki/Perron%E2%80%93Frobenius_theorem#Classification_of_matrices).)



> 
> **Theorem 2.** Let $n$ be a positive integer. Let $A$ be an irreducible $n\times n$-matrix whose entries are nonnegative rational numbers. Then, there exists a nonzero vector $v \in \mathbb{Q}^n$ with **positive** coordinates such that either $Av > v$ or $Av = v$ or $Av < v$.
> 
> 
> 


These two theorems can both be derived (with some nontrivial but not too hard work) from the [Perron-Frobenius theorem](https://en.wikipedia.org/wiki/Perron%E2%80%93Frobenius_theorem). The latter constructs a Perron-Frobenius eigenvector of $A$ with real coordinates; one just needs to approximate its coordinates by rational numbers (unless it has eigenvalue $1$, in which case we have to make sure the approximation happens in the $1$-eigenspace).



> 
> **Question.** How can Theorem 1 and Theorem 2 be proven in constructive logic?
> 
> 
> 


(Roughly speaking, this is probably tantamount to not using real numbers in the proof -- or building up the theory of real algebraics in constructive logic, which seems to have been done but I haven't seen it properly written up, and even then I don't know if Perron-Frobenius still applies and how you would prove it. [Simon Henry's approximate version of Brouwer's fixed point theorem](https://mathoverflow.net/a/202875/) might help, but I don't know how it is proven.)


I'm asking partly because of [recent uses of Theorems 1 and 2 in combinatorics](https://arxiv.org/abs/1804.03322), but this question has been in the back of my mind for many years, ever after I solved [a restricted version of the $n = 3$ case (IMO Shortlist 2003 problem A1)](https://artofproblemsolving.com/community/c6h5784p19085) ([official solution](https://anhngq.files.wordpress.com/2010/07/imo-2003-shortlist.pdf)) on an exam.



Constructive proof of a rational version of Perron-Frobenius?
Yes, both Theorem 1 and Theorem 2 have constructive proofs.


In the following, I will work with rational numbers, but the same arguments
work for any ordered field. (Note that in constructive logic, fields are
automatically discrete -- i.e., any two elements of a field are either equal
or not. Therefore, I don't think that $\mathbb{R}$ is a field for any
reasonable constructive definition of $\mathbb{R}$. Perhaps $\mathbb{R}$ is
some sort of "pro-field" in the same way as Laurent series over a field are;
to be frank, I don't care enough about $\mathbb{R}$ to find out.)


I set $\mathbb{N}=\left\{ 0,1,2,\ldots\right\} $.


Nonnegative matrices
--------------------


My main tool will be the following result from linear optimization:



> 
> **Theorem 3.** Let $n\in\mathbb{N}$, $n^{\prime}\in\mathbb{N}$ and
>  $m\in\mathbb{N}$. Let $A$ be an $m\times n$-matrix. Let $A^{\prime}$ be an
>  $m\times n^{\prime}$-matrix. Then, exactly one of the following two assertions holds:
> 
> 
> * *Assertion L1:* There exist two vectors $x\in\mathbb{Q}^{n}$ and $x^{\prime
> }\in\mathbb{Q}^{n^{\prime}}$ such that $x>0$, $x^{\prime}\geq0$ and
>  $Ax+A^{\prime}x^{\prime}=0$.
> * *Assertion L2:* There exists a vector $y\in\mathbb{Q}^{m}$ such that
>  $y^{T}A\geq0$, $y^{T}A^{\prime}\geq0$ and $y^{T}A\neq0$.
> 
> 
> 


Theorem 3 is Theorem 2.5l in [my *Elementary derivations of some results of
linear optimization*](http://www.cip.ifi.lmu.de/~grinberg/algebra/linopt.pdf) (where I prove it for $\mathbb{R}$ instead of
$\mathbb{Q}$, but the proof works over any ordered field). It seems to be due to Motzkin; it is actually a particular case of what is called "solvability of f)" on the [EoM page for the Motzkin transposition theorem](https://www.encyclopediaofmath.org/index.php/Motzkin_transposition_theorem) (note that the general case is easily seen to follow from this particular case). It is one of several results that are roughly equivalent to Farkas's lemma or the duality of linear programming. Its constructive proof (there are probably much better sources than my notes -- perhaps Motzkin's thesis?) is more or less based on Fourier-Motzkin elimination.


Recall that if $a=\left( a\_{1},a\_{2},\ldots,a\_{n}\right) ^{T}\in
\mathbb{Q}^{n}$ and $b=\left( b\_{1},b\_{2},\ldots,b\_{n}\right) ^{T}
\in\mathbb{Q}^{n}$ are two vectors of the same size, then $a<b$ means
"$a\_{i}<b\_{i}$ for each $i\in\left\{ 1,2,\ldots,n\right\}
$", whereas $a\leq b$ means "$a\_{i}\leq
b\_{i}$ for each $i\in\left\{ 1,2,\ldots,n\right\} $". Thus,
saying "$a<b$" is not the same as saying
"$a\leq b$ and $a\neq b$". The pedant in me
wants to add that it isn't even stronger, because the vector $0\_{0}=\left(
{}\right) ^{T}\in\mathbb{Q}^{0}$ (with no entries at all) satisfies
$0\_{0}<0\_{0}$ but not $0\_{0}\neq0\_{0}$.


Note also that if two vectors $a$ and $b$ satisfy $a\geq b$, then $a^{T}\geq
b^{T}$. The same holds for $\leq$, $>$ and $<$.


With this out of our way, let's state a few simple lemmas:



> 
> **Lemma 4.** Let $n\in\mathbb{N}$ and $m\in\mathbb{N}$. Let $A\in
> \mathbb{Q}^{n\times m}$ be a matrix whose entries are nonnegative. Let
>  $v\in\mathbb{Q}^{m}$ be such that $v\geq0$. Then, $Av\geq0$.
> 
> 
> 


*Proof of Lemma 4.* Clear from the definition of $Av$.



> 
> **Lemma 5.** Let $n$ be a positive integer. Let $A\in\mathbb{Q}^{n\times n}$
>  be a matrix whose entries are nonnegative. Let $y\in\mathbb{Q}^{n}$ and
>  $z\in\mathbb{Q}^{n}$ be such that $y\geq0$, $z\geq0$, $Ay\geq y$ and $Az<z$.
>  Then, $y=0$.
> 
> 
> 


*Proof of Lemma 5.* Assume the contrary. Thus, $y\neq0$.


From $Az<z$, we obtain $z>Az\geq0$ (by Lemma 4). Write $y$ as $y=\left(
y\_{1},y\_{2},\ldots,y\_{n}\right) ^{T}$, and write $z$ as $z=\left(
z\_{1},z\_{2},\ldots,z\_{n}\right) ^{T}$. The coordinates $z\_{1},z\_{2}
,\ldots,z\_{n}$ of $z$ are positive (since $z>0$), while the coordinates
$y\_{1},y\_{2},\ldots,y\_{n}$ of $y$ are nonnegative (since $y\geq0$), and at
least one of them is positive (since $y\neq0$). Hence, $\max\left\{
y\_{i}/z\_{i}\ \mid\ i\in\left\{ 1,2,\ldots,n\right\} \right\} $ is a
well-defined positive rational number. Denote this number by $\mu$. Thus, for
each $j\in\left\{ 1,2,\ldots,n\right\} $, we have $y\_{j}/z\_{j}\leq\mu$, so
that
\begin{equation}
y\_{j}\leq z\_{j}\mu.
\tag{1} \label{pf.l5.0}
\end{equation}


Now, write the $n\times n$-matrix $A$ in the form $A=\left( a\_{i,j}\right)
\_{1\leq i\leq n,\ 1\leq j\leq n}$. Then, $a\_{i,j}\geq0$ for all $i$ and $j$
(since all entries of $A$ are nonnegative). We have $Ay\geq y$; in other
words,
\begin{equation}
\sum\_{j=1}^{n}a\_{i,j}y\_{j}\geq y\_{i}\ \ \ \ \ \ \ \ \ \ \text{for each }
i\in\left\{ 1,2,\ldots,n\right\} .
\tag{2} \label{pf.l5.1}
\end{equation}
Also, $Az<z$; in other words,
\begin{equation}
\sum\_{j=1}^{n}a\_{i,j}z\_{j}<z\_{i}\ \ \ \ \ \ \ \ \ \ \text{for each }
i\in\left\{ 1,2,\ldots,n\right\} .
\tag{3} \label{pf.l5.2}
\end{equation}
Hence, for each $i\in\left\{ 1,2,\ldots,n\right\} $, we have
\begin{align\*}
y\_{i} & \leq\sum\_{j=1}^{n}a\_{i,j}\underbrace{y\_{j}}\_{\substack{\leq z\_{j}
\mu\\\text{(by \eqref{pf.l5.0})}}}\ \ \ \ \ \ \ \ \ \ \left( \text{by
\eqref{pf.l5.1}}\right) \\
& \leq\underbrace{\sum\_{j=1}^{n}a\_{i,j}z\_{j}}\_{\substack{<z\_{i}\\\text{(by
\eqref{pf.l5.2})}}}\mu<z\_{i}\mu\ \ \ \ \ \ \ \ \ \ \left( \text{since }
\mu\text{ is positive}\right) .
\end{align\*}
Thus, $y\_{i}/z\_{i}<\mu$ for each $i\in\left\{ 1,2,\ldots,n\right\} $. Hence,
$\max\left\{ y\_{i}/z\_{i}\ \mid\ i\in\left\{ 1,2,\ldots,n\right\} \right\}
<\mu$. This contradicts $\mu=\max\left\{ y\_{i}/z\_{i}\ \mid\ i\in\left\{
1,2,\ldots,n\right\} \right\} $. This completes the proof of Lemma 5.


*Proof of Theorem 1.* The entries of the matrix $A$ are nonnegative; thus, the
same holds for the matrix $A^{T}$.


As usual, let $I\_{n}$ denote the $n\times n$ identity matrix. Theorem 3
(applied to $n$, $n$, $I\_{n}$ and $A-I\_{n}$ instead of $m$, $n^{\prime}$, $A$
and $A^{\prime}$) yields that we are in one of the following two cases:


* *Case 1:* There exist two vectors $x\in\mathbb{Q}^{n}$ and $x^{\prime}
\in\mathbb{Q}^{n}$ such that $x>0$, $x^{\prime}\geq0$ and $I\_{n}x+\left(
A-I\_{n}\right) x^{\prime}=0$.
* *Case 2:* There exists a vector $y\in\mathbb{Q}^{n}$ such that $y^{T}
I\_{n}\geq0$, $y^{T}\left( A-I\_{n}\right) \geq0$ and $y^{T}I\_{n}\neq0$.


Let us first consider Case 1. In this case, there exist two vectors
$x\in\mathbb{Q}^{n}$ and $x^{\prime}\in\mathbb{Q}^{n}$ such that $x>0$,
$x^{\prime}\geq0$ and $I\_{n}x+\left( A-I\_{n}\right) x^{\prime}=0$. Consider
these $x$ and $x^{\prime}$. The vector $x^{\prime}$ has nonnegative
coordinates (since $x^{\prime}\geq0$). From $I\_{n}x+\left( A-I\_{n}\right)
x^{\prime}=0$, we obtain $0=I\_{n}x+\left( A-I\_{n}\right) x^{\prime
}=x+Ax^{\prime}-x^{\prime}$, so that $Ax^{\prime}-x^{\prime}=-x<0$ (since
$x>0$). In other words, $Ax^{\prime}<x^{\prime}$. Hence, $x^{\prime}\neq0$.
Thus, there exists a nonzero vector $v\in\mathbb{Q}^{n}$ with nonnegative
coordinates such that $Av<v$ (namely, $v=x^{\prime}$). Hence, Theorem 1 is
proven in Case 1.


Let us now consider Case 2. In this case, there exists a vector $y\in
\mathbb{Q}^{n}$ such that $y^{T}I\_{n}\geq0$, $y^{T}\left( A-I\_{n}\right)
\geq0$ and $y^{T}I\_{n}\neq0$. Denote this vector $y$ by $u$. Thus,
$u\in\mathbb{Q}^{n}$ satisfies $u^{T}I\_{n}\geq0$, $u^{T}\left( A-I\_{n}
\right) \geq0$ and $u^{T}I\_{n}\neq0$. We have $u^{T}=u^{T}I\_{n}\geq0$ and
thus $u\geq0$. Also, $u^{T}=u^{T}I\_{n}\neq0$ and thus $u\neq0$. Moreover,
$u^{T}A-u^{T}=u^{T}\left( A-I\_{n}\right) \geq0$ and thus $u^{T}A\geq u^{T}$.
Taking transposes, we find $\left( u^{T}A\right) ^{T}\geq\left(
u^{T}\right) ^{T}=u$, so that $u\leq\left( u^{T}A\right) ^{T}=A^{T}u$. In
other words, $A^{T}u\geq u$.


Next, Theorem 3 (applied to $n$, $n$, $I\_{n}$ and $A^{T}-I\_{n}$ instead of
$m$, $n^{\prime}$, $A$ and $A^{\prime}$) yields that we are in one of the
following two subcases:


* *Subcase 2.1:* There exist two vectors $x\in\mathbb{Q}^{n}$ and $x^{\prime
}\in\mathbb{Q}^{n}$ such that $x>0$, $x^{\prime}\geq0$ and $I\_{n}x+\left(
A^{T}-I\_{n}\right) x^{\prime}=0$.
* *Subcase 2.2:* There exists a vector $y\in\mathbb{Q}^{n}$ such that
$y^{T}I\_{n}\geq0$, $y^{T}\left( A^{T}-I\_{n}\right) \geq0$ and $y^{T}
I\_{n}\neq0$.


Let us first consider Subcase 2.1. In this subcase, there exist two vectors
$x\in\mathbb{Q}^{n}$ and $x^{\prime}\in\mathbb{Q}^{n}$ such that $x>0$,
$x^{\prime}\geq0$ and $I\_{n}x+\left( A^{T}-I\_{n}\right) x^{\prime}=0$.
Consider these $x$ and $x^{\prime}$. From $I\_{n}x+\left( A^{T}-I\_{n}\right)
x^{\prime}=0$, we obtain $0=I\_{n}x+\left( A^{T}-I\_{n}\right) x^{\prime
}=x+A^{T}x^{\prime}-x^{\prime}$, so that $A^{T}x^{\prime}-x^{\prime}=-x<0$
(since $x>0$). In other words, $A^{T}x^{\prime}<x^{\prime}$. Hence, Lemma 5
(applied to $A^{T}$, $u$ and $x^{\prime}$ instead of $A$, $y$ and $z$) yields
$u=0$. This contradicts $u\neq0$. This contradiction shows that Subcase 2.1
cannot happen.


Hence, we are in Subcase 2.2. Thus, there exists a vector $y\in\mathbb{Q}^{n}$
such that $y^{T}I\_{n}\geq0$, $y^{T}\left( A^{T}-I\_{n}\right) \geq0$ and
$y^{T}I\_{n}\neq0$. Consider this $y$. We have $y^{T}=y^{T}I\_{n}\geq0$, so that
$y\geq0$. We have $y^{T}=y^{T}I\_{n}\neq0$, so that $y\neq0$. Thus, $y$ is a
nonzero vector in $\mathbb{Q}^{n}$ with nonnegative coordinates (since
$y\geq0$). We have $y^{T}A^{T}-y^{T}=y^{T}\left( A^{T}-I\_{n}\right) \geq0$,
so that $y^{T}A^{T}\geq y^{T}$. Taking transposes, we obtain $\left(
y^{T}A^{T}\right) ^{T}\geq\left( A^{T}\right) ^{T}$. This rewrites as
$Ay\geq y$. Hence, there exists a nonzero vector $v\in\mathbb{Q}^{n}$ with
nonnegative coordinates such that $Av\geq v$ (namely, $v=y$). Hence, Theorem 1
is proven in Case 2.


We have now proven Theorem 1 in both Cases 1 and 2; thus we are done.


Irreducible nonnegative matrices
--------------------------------


Next, we take aim at Theorem 2.


For any $n\times m$-matrix $A\in\mathbb{Q}^{n\times m}$ and any $i\in\left\{
1,2,\ldots,n\right\} $ and $j\in\left\{ 1,2,\ldots,m\right\} $, we let
$A\_{i,j}$ denote the $\left( i,j\right) $-th entry of $A$.


We will need the following equivalent conditions for irreducibility:



> 
> **Theorem 6.** Let $n$ be a positive integer. Let $A\in\mathbb{Q}^{n\times n}$
>  be an $n\times n$-matrix whose entries are nonnegative. Then, the following
>  statements are equivalent:
> 
> 
> *Statement 1:* The matrix $A$ is irreducible.
> 
> 
> *Statement 2:* For any $i\in\left\{ 1,2,\ldots,n\right\} $ and $j\in\left\{
> 1,2,\ldots,n\right\} $, there exists some $k\in\mathbb{N}$ such that $\left(
> A^{k}\right) \_{i,j}>0$.
> 
> 
> *Statement 3:* There exists some $m\in\mathbb{N}$ such that all entries of the
>  matrix $A^{0}+A^{1}+\cdots+A^{m}$ are positive.
> 
> 
> *Statement 4:* If $\left\{ U,V\right\} $ is a partition of $\left\{
> 1,2,\ldots,n\right\} $ into two nonempty subsets $U$ and $V$, then there
>  exist $u\in U$ and $v\in V$ satisfying $A\_{u,v}>0$.
> 
> 
> 


Theorem 6 is well-known (it is the algebraic analogue of the equivalence of
different definitions of "strong connectivity" for a directed graph), and the
proof you will find in the literature (e.g., on Markov chains, I believe) is
already constructive. All I will need is the implication from Statement 1 to
Statement 3.


We will also need the following simple lemma:



> 
> **Lemma 7.** Let $n\in\mathbb{N}$ and $m\in\mathbb{N}$. Let $A\in
> \mathbb{Q}^{n\times m}$ be a matrix whose entries are **positive**. Let
>  $v\in\mathbb{Q}^{m}$ be such that $v\geq0$ and $v\neq0$. Then, $Av>0$.
> 
> 
> 


*Proof of Lemma 7.* This is similar to Lemma 4, except that each coordinate of
$Av$ is a sum of nonnegative addends containing at least one **positive**
addend, and thus is positive.


*Proof of Theorem 2.* The matrix $A$ is irreducible. Thus, by Theorem 6 (more
precisely, by the implication $\left( \text{Statement 1}\right)
\Longrightarrow\left( \text{Statement 3}\right) $), there exists some
$m\in\mathbb{N}$ such that all entries of the matrix $A^{0}+A^{1}+\cdots
+A^{m}$ are positive. Consider this $m$, and set $B=A^{0}+A^{1}+\cdots
+A^{m}\in\mathbb{Q}^{n\times n}$. Then, all entries of the matrix $B$ are positive.


Theorem 1 shows that there exists a nonzero vector $v\in\mathbb{Q}^{n}$ with
nonnegative coordinates such that either $Av\geq v$ or $Av<v$. Consider such a
$v$, and denote it by $w$. Thus, $w\in\mathbb{Q}^{n}$ is a nonzero vector with
nonnegative coordinates and satisfies either $Aw\geq w$ or $Aw<w$.


Define a vector $v\in\mathbb{Q}^{n}$ by $v=Bw$. We shall show that $v$ is a
nonzero vector with **positive** coordinates such that either $Av>v$ or $Av=v$
or $Av<v$. This will clearly prove Theorem 2.


We have $w\geq0$ (since the vector $w$ has nonnegative coordinates) and
$w\neq0$ (since $w$ is nonzero). Hence, Lemma 7 (applied to $n$, $B$ and $w$
instead of $m$, $A$ and $v$) yields that $Bw>0$. Thus, $v=Bw>0$. In other words,
$v$ is a vector with **positive** coordinates. Hence, $v$ is nonzero (since
$n>0$).


We have $B=A^{0}+A^{1}+\cdots+A^{m}$. Thus, $AB=A^{1}+A^{2}+\cdots+A^{m+1}
=BA$. Now, recall that either $Aw\geq w$ or $Aw<w$. Hence, we are in one of
the following three cases:


* *Case 1:* We have $Aw\geq w$ and $Aw\neq w$.
* *Case 2:* We have $Aw=w$.
* *Case 3:* We have $Aw<w$.


Let us first consider Case 1. In this case, we have $Aw\geq w$ and $Aw\neq w$.
In other words, $Aw-w\geq0$ and $Aw-w\neq0$. Hence, Lemma 7 (applied to $n$, $B$
and $Aw-w$ instead of $m$, $A$ and $v$) yields $B\left( Aw-w\right) >0$. From
$v=Bw$, we obtain
\begin{equation}
Av-v=\underbrace{AB}\_{=BA}w-Bw=BAw-Bw=B\left( Aw-w\right) >0.
\end{equation}
In other words, $Av>v$. Thus, in Case 1, we have proven on our goal (namely,
that either $Av>v$ or $Av=v$ or $Av<v$).


Let us next consider Case 2. In this case, we have $Aw=w$. Now, from $v=Bw$,
we obtain $Av=\underbrace{AB}\_{=BA}w=B\underbrace{Aw}\_{=w}=Bw=v$. Thus, in
Case 2, we have proven on our goal (namely, that either $Av>v$ or $Av=v$ or
$Av<v$).


Let us finally consider Case 3. In this case, we have $Aw<w$. Hence, $w-Aw>0$.
Therefore, $w-Aw\geq0$ and $w-Aw\neq0$. Hence, Lemma 7 (applied to $n$, $B$ and
$w-Aw$ instead of $m$, $A$ and $v$) yields $B\left( w-Aw\right) >0$. From $v=Bw$,
we obtain
\begin{equation}
v-Av=Bw-\underbrace{AB}\_{=BA}w=Bw-BAw=B\left( w-Aw\right) >0.
\end{equation}
In other words, $Av<v$. Thus, in Case 3, we have proven on our goal (namely,
that either $Av>v$ or $Av=v$ or $Av<v$).


We have now proven our goal in each of the three Cases 1, 2 and 3. Thus, we
always have either $Av>v$ or $Av=v$ or $Av<v$. As we have said, this proves
Theorem 2.


