Ordering on $R[\sqrt{n}]$ for an ordered ring $R$ I'm interested in showing that if $R$ is an ordered ring (with ordering $\leq$), and $n \geq 0$, then $R[\sqrt{n}]$ is also an ordered ring.
In the reals, $0 \leq a_1 + a_n\sqrt n$ iff either (1) $0 \leq a_1$ and $na_n^2 \leq a_1^2$, or (2) $0 \leq a_n$ and $a_1^2 \leq na_n^2$.  So it seems natural to define the set $P$ of nonnegative elements of $R[\sqrt{n}]$ by the rule

*

*$a_1 + a_n\sqrt{n} \in P$ iff (1) or (2) above hold

However, I'm having trouble proving that $x \in P$ and $y \in P$ implies $x + y \in P$.  It seems like it should be elementary, but I'm finding myself running around in circles.
I've been trying to split the proof into cases, depending on whether $x$ and $y$ satisfy rules (1) or (2).  The cases where they both satisfy (1) or both satisfy (2) are easy, but the casework is getting overwhelming when $x$ satisfies (1) and $y$ satisfies (2).
I wonder if anyone can suggest something I'm missing, or maybe point me to a more general theorem that would help (although I'd like to avoid getting too esoteric since my eventual goal is to formulate the proof in coq).
Thanks!
Update: I’ve made progress but am still stuck.  Unless I’m mistaken, the only case I need is to show that $0 \leq (x_1 + x_n\sqrt{n}) + (y_1 + y_n\sqrt{n})$ when the following conditions all hold:

*

*$0 \leq x_1$

*$0 \leq -x_n$

*$nx_n^2 \leq x_1^2$

*$0 \leq -y_1$

*$0 \leq y_n$

*$y_1^2 \leq ny_n^2$

*$0 \leq x_1 + y_1$

*$0 \leq -x_n - y_n$
Combining these assumptions gives $0 \leq y_1^2 \leq ny_n^2 \leq n x_n^2 \leq x_1^2$.
In this case I need to show that $n(x_n + y_n)^2 \leq (x_1 + y_1)^2$.
I’ve tried playing with fractions, derivatives, absolute values, and just can’t solve this case.  Any help would be appreciated.
 A: There are scores of details to check, but the following seems to handle the most difficult cases.
Below $a,b,c,d$ will always denote arbitrary positive elements of $R$, so for example $-a<0$.

Assuming that $R$ is an integral domain we can extend its ordering to its field of fractions $F$. Next I define that a fraction $a/b$, both $a,b$ positive elements of $R$, is $>\sqrt n$ if and only if $a^2>n b^2$ in $R$. Obviously the negative fractions are all $<\sqrt n$. It is trivial to show that equal fractions behave compatibly.
At this point we have, in a sense, defined where $\sqrt{n}$ lies on the number line of $F$. We still need to check that this is compatible with the ordering of $F$. To that end we prove the result.
Lemma 1. If $c/d>\sqrt n$ and $a/b>c/d$ then $a/b>\sqrt n$.
Proof. We have $c^2/d^2>n$ and $a^2/b^2>c^2/d^2$ so $a^2/b^2>n$ and the claim follows.
Next we define the set of positive elements of $R[\sqrt n]$ by declaring that

$a+b\sqrt n$ is always positive, $-a-b\sqrt n$ is always negative,
and then in the mixed cases
$$
\begin{aligned}
a-b\sqrt n>0&\Longleftrightarrow a/b>\sqrt n,\\
-a+b\sqrt n>0&\Longleftrightarrow a/b<\sqrt n.
\end{aligned}
$$
Handle the cases $a=0$ and $b=0$ in the obvious way. I think this is equivalent to the OP's definition of positive elements of $R[\sqrt n]$, but I choose to work in $F$, so rephrase it this way.

The goal is to show that the set of positive numbers thus defined is closed under addition. I will only handle the mixed case numbers, for I think those are the most delicate ones.

Remembering that the mediant $(a+c)/(b+d)$ lies between $a/b$ and $c/d$ will play a key role. We also need to look at what happens with $(a-c)/(b-d)$ when $b>d$.
The model I kept in mind is to compare the following rationals with $\sqrt3$:
$$
\frac21>\frac74>\sqrt 3>\frac{17}{10}>\frac53.
$$

*

*Here the mediant $(7+2)/(1+4)=9/5$ will automatically be $>\sqrt3$ as the mediant is $>7/4$. Similarly the mediant $(17+5)/(10+3)$ will automatically be $<\sqrt 3$ as it is below $17/10$.

*With $a/b=7/4$ and $c/d=5/3$, so $b>d$, we see that $(a-c)/(b-d)=2/1$ is actually above $a/b$. This is also because $7/4$ is the mediant of $2/1$ and $5/3$.

*Similarly with $a/b=17/10$ and $c/d=7/4$ (again $b>d$) the fraction
$(a-c)/(b-d)=10/6=5/3$ is below $a/b$. This is because $17/10$ is below $7/4$, and also the mediant of $7/4$ and $10/6$.

These inequalities generalize easily in the indicated way and give us the claim. Behold.

Lemma 2. If $x$ and $y$ are positive elements of $R[\sqrt n]$, so is $x+y$.
My proof only covers the mixed cases for I think the rest are easier. I split it into cases according to what types of mixed cases we have.
Case I. $x=a-b\sqrt n, y=c-d\sqrt n$.
In this case we have $a/b>\sqrt n$ and $c/d>\sqrt n$. The mediant
$$
\frac{a+c}{b+d}=\alpha \frac ab+\beta \frac cd
$$
with $\alpha=b/(b+d)$, $\beta=d/(b+d)$ both positive. Furthermore $\alpha+\beta=1$. These imply that $(a+b)/(c+d)$ is between $a/b$ and $c/d$. By Lemma 1 we can conclude that
$(a+b)/(c+d)>\sqrt n$. Consequently $x+y=(a+b)-(c+d)\sqrt n$ is positive.
Case II. $x=a-b\sqrt n$, $y=-c+d\sqrt n$.
This time we know that $a/b>\sqrt n$ and $c/d<\sqrt n$.
Here $x+y=(a-c)-(b-d)\sqrt n$, so we need to compare $(a-c)/(b-d)$ with $\sqrt n$. We need to further split this into two cases according to which denominator, $b$ or $d$, is larger (the case $b=d$ is trivial).
Assume first that $b>d$. Our goal is to show that $(a-c)/(b-d)>\sqrt n$. We can reuse the result about the mediant from Case I simply by observing that $a/b$ is the mediant of $(a-c)/(b-d)$ and $c/d$. Therefore $a/b$ lies in between the other two fractions. As $a/b>c/d$ we can conclude that $(a-c)/(b-d)>a/b$.
Again, by Lemma 1, we have $(a-c)/(b-d)>\sqrt n$ proving the claim.
On the other hand when $d>b$ we have $x+y=-(c-a)+(d-b)\sqrt n$, and thus we need to show that $(c-a)/(d-b)<\sqrt n$. This follows similarly by observing that $c/d$ is the mediant of $a/b$ and $(c-a)/(d-b)$. This time the conclusion is that $(c-a)/(d-b)<c/d$.
As $c/d<\sqrt n$ the obvious counterpart of Lemma 1 implies that also $(c-a)/(d-b)<\sqrt n$.
A: Welcome to MSE!
I'm sure your method can be made to work, but like you said, the casework is rather tedious. Another approach might be to try the following. Working backwards, we should have
$$0 < a+b\sqrt{n} \iff -a < b \sqrt{n}$$
Now our dream is to "square both sides" in order to kill off the $\sqrt{n}$ and get left with something in $R$. The issue, of course, is that squaring kills all of our sign information! The clever trick, then? Without loss of generality, we want $\sqrt{n}$ to be positive, and for positive numbers $x$ and $|x|$ agree. But $|x|$ preserves sign information for negative numbers.
This observation might clue us in to look at the function $x \mapsto |x| \cdot x$. With this in mind, we can "square both sides" with our new and improved squaring function, to find
$$-a < b \sqrt{n} \iff -|a| \  a < |b| \ bn \iff 0 < |a|\ a + |b|\ bn$$
but this new condition is entirely checkable inside $R$. Can you show that it works as a good definition of the positive elements of $R[\sqrt{n}]$ whenever $n > 0$ in $R$?

I hope this helps ^_^
