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 \leq 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.)

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. 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 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, 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) (official solution) on an exam.

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.)

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. 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 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, 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) (official solution) on an exam.