Constructive proof of a rational version of Perron-Frobenius? 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.
 A: A course in constructive algebra by Mines, Richman & Ruitenburg, covers the constructive development of discrete fields and their algebraic completion, and even their valuation-metric completion.
This is a very direct and clear development, showing that for discrete fields (such as $\mathbb{Q}$), the algebraic closure (in this case $\mathbb{A}$) is again a discrete field. In other words, for your situation, the characteristic polynomial of $A$ can be constructively factored over $\mathbb{A}$, which should give you enough constructive traction to prove a constructive analogue of the two theorems you give above.
However, given that you speak of non-negative matrices (not necessarily irreducible for theorem 1), I wonder if  thms. 1 and 2 are true constructively.
For both theorems, since you do not restrict to positive matrices, approximation with positive matrices is necessary. Usually, we then cannot conclude sharply things like: "$Av \geq v$ or $Av < v$" (thm. 1), "$Av > v$ or $Av = v$ or $Av < v$" (thm. 2), and even "$v \in \mathbb{Q}^n$" (both thms.).
So I would advise to first prove the weaker versions where $A$ is a positive matrix, and then study where approximations come in for proving your constructive analogues.

[update to reflect the comments below:]
Constructive Perron-Frobenius for positive matrices follows easily from the above, since (obviously) once we split the characteristic polynomial $p(A)$ over $\mathbb{A}$, we will find its roots, which have decidable equality as well as decidable membership of $\mathbb{R}$. From the classical theory and KG (the Kleene Getaway, see below), it follows constructively that we find exactly one positive real zero $s$ of $p(A)$ such that $s$ has strictly the largest absolute value of all the zeros of $p(A)$. 
[In essence KG boils down to this: we know that we find exactly one positive real zero $s$ with these properties, because a) we can factor $p(A)$ constructively, b) positivity and largest absolute value are decidable properties for roots of $p(A)$, and c) it is impossible that there is no positive root having the largest absolute value, since that would contradict classical mathematics.]
The $s$-corresponding eigenvector can now be found using compactness and uniform continuity (of the linear function given by $A$ on $\mathbb{R}^n$). There most likely is a more elegant algebraic way, but I'm more a lazy topologist so I use brute topological force... 
[second update:]
On a more elegant note, notice that the field of the algebraic reals $^r\mathbb{A}:= \mathbb{A}\cap\mathbb{R}$ gives rise to the discrete $n$-dimensional vector space $(^r\mathbb{A})^n$ (over $^r\mathbb{A}$). That means that we can actually calculate the Perron-Frobenius eigenvector $v$ by simple linear algebra, since the rank of $A-sI$ is $n-1$ and $A-sI$ is a matrix over a discrete field (the eigenvector spans the one-dimensional kernel of $A-sI$). So we easily find $v\in (^r\mathbb{A})^n$, and then, because of the classical theory and because $^r\mathbb{A}$ is discrete, by KG (see below) we immediately (and constructively!) deduce the positivity of $v$.  
[In essence KG boils down to this: the eigenvector v is positive, because a) we can find v constructively, b) positivity is decidable for vectors in $(^r\mathbb{A})^n$, and c) it is impossible that v is not positive, since that would contradict classical mathematics.]
This then proves:

Theorem (Constructive Perron-Frobenius for positive algebraic matrices): 
Let $A$ be a a positive $n\times n$ matrix with entries in the real algebraic field $^r\mathbb{A}$. Then: 
a) there is a positive real algebraic number $s$, called the Perron–Frobenius eigenvalue, such that $s$ is an eigenvalue of $A$ and any other eigenvalue $\lambda$ (possibly complex) is strictly smaller than $s$ in absolute value. Moreover, $s$ is a simple root of the characteristic polynomial of A. Consequently, the eigenspace associated to $s$ is one-dimensional.
b) there is an $s$-eigenvector $v$ of $A$ such that all components of $v$ are positive algebraic.

[third update:]
Yet even for positive $A$, I don't see how theorem 1 above would constructively follow immediately. The difficulty lies in the case where the Perron-Frobenius eigenvalue is $1$. When we then try to approximate the eigenvector by rational vectors, we cannot assume (I think) that we can do so in an order-positively or order-negatively consequent way (regarding $A(u)$ vs $u$, for approximating rational vector $u$).
What we do have is an interesting almost-generalization to the algebraic reals:

Theorem 1$^*$ 
Let $A$ be a positive $n\times n$ matrix with entries in the real algebraic field $^r\mathbb{A}$. Then at least one of the following two statements is true:
a) there is a vector $w$ in $\mathbb{Q}^n$ such that either $A(w)<w$ or $w<A(w)$ 
b) for every $\epsilon>0$ there is a vector $z$ in $\mathbb{Q}^n$ such that $|A(z)-z|<\epsilon$.

Proof
Case a) corresponds to the case where the Perron-Frobenius eigenvalue $s$ is apart from $1$. Case b) corresponds to $s=1$. We can decide in which case we find ourselves sinds $s$ is in $^r\mathbb{A}$.
In both cases we can approximate the Perron-Frobenius eigenvector by rational vectors, which then gives the theorem. (end of proof).
Of course, a very nice alternative is a direct corollary of the constructive algebraic version of Perron-Frobenius itself, as explained above:

Theorem 1$^{**}$ (corollary of the constructive Perron-Frobenius thm. for positive algebraic matrices)
Let $A$ be a positive $n\times n$ matrix with entries in the real algebraic field $^r\mathbb{A}$. Then there is a vector $w$ in $(^r\mathbb{A})^n$ such that either $A(w)<w$ or $w<A(w)$ or $A(w)=w$.

I will leave other analogues to the OP. 

[fourth update:]
KG (the Kleene Getaway) is a constructive principle which enables the direct constructive use of a classical result in the following situation:
Suppose T is a classical theorem of analysis/topology/... provable in a formal system $\mbox{F}$ which is constructively 'sound' in the sense that $\mbox{F}$ is constructively equiconsistent with its constructive subsystem $\mbox{F}$$_\mbox{c}$, obtained by leaving out LEM. 
Now suppose that we have an $x$ and a property $P$ such that: 
a) $P(x)$ is constructively decidable (so we can decide $P(x)$ or $\neg(P(x)$)
b) $P(x)$ holds classically by T
Then KG states that $P(x)$ holds constructively as well.
Proof: The proof is actually quite simple, on the proof-level of the formal system, since $\neg (P(x))$ is impossible by b) and the equiconsistency of $\mbox{F}$ and $\mbox{F}$$_\mbox{c}$
[fifth update: Matt F. pointed out in this question on MO that KG is proved (but unnamed) in Michael Beeson, “Some Relations between Classical and Constructive Mathematics”, Journal of Symbolic Logic 1978, see here on JStor.]
One of Kleene's highest achievements in my opinion is one of the least known: his seminal work The Foundations of Intuitionistic Mathematics - especially in relation to recursive functions (usually abbreviated FIM).
In FIM Kleene developed a formal system (also called FIM...) and 4 years later, through function realizability methods, he showed equiconsistency of the classical extension of a basis theory of FIM and the intuitionistic extension of that basic system.
So, unnoticed by many: intuitionistic mathematics is as sound as classical mathematics, in the comparative realm of say separable analysis, topology, etc.
