Krdytkyu

$DeclareMathOperator{lad}{Lad}$Let $(K,<)$ be an ordered field, and $(R,<)$ be the real closure of $(K,<)$. Let $lad(K)$ denote the ladder of $(K,<)$ (for the definition of the ladder, see the link given below). Then the canonical injection $iota colon lad(K) to lad(R)$ is induced. My first question is the following.

Question 1. Is $iota colon lad(K) to lad(R)$ an isomorphism?

I came up with this question when I read https://mathoverflow.net/a/23529/131576. According to the answer, Question 1 is true in the following case.

Proposition. Let $L$ be a linear order. Write $F = bar{mathbb{Q}} cap mathbb{R}$. Suppose $(K,<)$ be the ordered field $F(x_l : l in L)$ as in the answer. Then $iota$ is an isomorphism.

In fact, $(R,<)$ is contained in the field of Hahn series $F[[t^G]]$, where $G$ is the group $mathbb{Q}^{{oplus} L}$ with a suitable order. However, this proof seems a little bit hard in that it uses Hahn series. Then my second question is the following.

Question 2. Are there any easier proofs of the Proposition?

Any help would be appreciated.

I don't know if there is an easy proof of $1$, but there is a somewhat elementary one using valuation theory and more specifically the natural valuation on an ordered field. The idea is that the value group of $R$ is the divisible hull of that of $K$, but here I only prove what's necessary for your result.

So let $v$ denote the generic function of natural valuation on an ordered field, and let $operatorname{Lad}$ denote the generic function of comparability class on an ordered field. Notice that if $K$ is an ordered field and $x in K$ is positive infinite, then $operatorname{Lad}(y)=operatorname{Lad}(x)$ for all $y in v x$.
(in fact, the Ladder functor is naturally isomorphic to the composition of the natural valuations functors on the categories of ordered fields and ordered groups).

Claim: if $A$ is an algebraic (ordered field) extension of $K$ and $x in A$, we have $d_x:=[v K[x]: v K] <infty$.

It is no secret that $R$ is an algebraic extension of $A$ so we may apply the claim. Let $x in R^{times}$ be positive infinite. We have $d_x.vK[x] subseteq v K$ so $d_x. v x =v x^{d_x}=v y$ for some element $y in K^{times}$ which must be infinite. We have $operatorname{Lad}(x)=operatorname{Lad}(x^{d_x})=operatorname{Lad}(y) in operatorname{Lad}(K)$, hence $operatorname{Lad}(R)=operatorname{Lad}(K)$.

Proof of the claim: notice that every finite family $(gamma_i)_{1leq ileq n}$ in $Gamma_{K[x]}$ such that for $ineq j$ we have $gamma_i - gamma_j notin Gamma_K$, and for $x_1,...,x_n in K[x]^{times}$ with $forall 1 leq i leq n,gamma_i= v x_i$, the family $(x_1,...,x_n)$ is free in the $K$-vector space $K[x]$. Indeed for $(0,...,0)neq (a_1,...,a_n) in K^n$ and $1leq i neq j leq n$, we have $gamma_j - gamma_inotin v K ni v a_i - v a_j$ so $v a_i x_i =v a_i + gamma_ineq v a_j + gamma_j =v a_j x_j$. By standard properties of valuations, we have $v sum limits_{i=1}^n a_i x_i=min_{i=1}^n v a_i x_i$, and in particular the element $sum limits_{i=1}^n a_i x_i$ is non zero. The extension $K[x] / K$ is finite, so $[v K[x]: vK]$ must be finite.