(I have now also asked this on mathoverflow.)
Let $\langle F,\hspace{-0.04 in}+,\hspace{-0.03 in}\cdot \rangle$ be a field, let $E$ be a non-zero strict subring of $F$, let $\leq$ be
a total order on $E$ that makes $\langle E,\hspace{-0.04 in}+,\hspace{-0.03 in}\cdot,\hspace{-0.03 in}\leq \rangle$ into an ordered ring, and let
$|\hspace{-0.05 in}\cdot \hspace{-0.05 in}| : F\to E$ be such that for all elements $x$ of $E$, for all elements $y$ and $z$ of $F\hspace{-0.02 in}$,
$0\leq x \; \implies \; |x| = x$
and
$0\leq |z| \;\;\;\;$ and $\;\;\;\; |\hspace{.02 in}y\hspace{-0.04 in}\cdot \hspace{-0.04 in}z| \; = \; |y|\cdot |z| \;\;\;\;$ and $\;\;\;\; |\hspace{.02 in}y\hspace{-0.03 in}+\hspace{-0.03 in}z| \; \leq \; |y|+|z|$
.
Does it follow that there exists an element $i$ of $F$ such that
$i^{\hspace{.03 in}2} = -1$
and
for all elements $z$ of $F$, there exist elements $a$ and $b$ of $E$
such that $\;\;\;\;\;\;\; z \; = \; a\hspace{-0.03 in}+\hspace{-0.03 in}(b\hspace{-0.05 in}\cdot \hspace{-0.05 in}i\hspace{.02 in}) \;\;\;$ and $\;\;\; |z|^{\hspace{.02 in}2} \; = \; a^{\hspace{.02 in}2} + b^{\hspace{.02 in}2}$
?
One can verify that the implication and the multiplicativity
force $E$ to be a sub$field$ of $F$ and force $|\hspace{-0.05 in}\cdot \hspace{-0.05 in}|$ to satisfy
for all non-zero elements $y$ of $F$, $\;\;\; |\hspace{.02 in}y| \neq 0 \;$ and $\; \left|\hspace{.03 in}y^{-1}\right| = |\hspace{.02 in}y|^{-1} \;\;\;$.
Accordingly, a necessary condition for $i$ to satisfy the conditions of my question
is that $\{\hspace{-0.03 in}1,\hspace{-0.03 in}i\}$ be a basis for $F$ as a vector space over $E$.
I now see how to prove that letting $F$ be a subfield of $\mathbb{C}$ and letting $|\hspace{-0.05 in}\cdot \hspace{-0.05 in}|$
agree with the usual absolute value on $\mathbb{C}$ cannot yield a counterexample.
Lemma: For all such structures, all real elements of $F$ are in $E$.
Proof: Fix any such structure and let $z$ be any real element of $F$. $|z| = \pm z$ and $|z|\in E$ ,
so at least one of $\{z\hspace{.02 in},\hspace{-0.04 in}-z\}$ is in $E$. Since $E$ is a subring, that means $z\in E$ .
Result: Such structures cannot be counterexamples.
Proof:
Let $z$ be any element of $F$ that's not in $E$. By the contrapositive of the lemma, $|z|\not\in \mathbb{R}$ .
In other words, $\operatorname{Im}(z) \neq 0$ , so in particular $z\neq 0$ .
$|z|^2 \; = \; \overline{z} \cdot z \qquad \qquad \overline{z} \; = \; |z|\hspace{-0.03 in}\cdot \hspace{-0.03 in}|z|\hspace{.04 in}/\hspace{.04 in}z \; \in \; F \qquad \qquad 2\cdot \operatorname{Im}(z) \cdot i \; = \; \overline{z}-z \; \in \; F$
$\operatorname{Im}(z) \cdot i \: = \: 2\hspace{-0.03 in}\cdot \hspace{-0.03 in}\operatorname{Im}(z)\hspace{-0.03 in}\cdot \hspace{-0.03 in}i\hspace{.04 in}/\hspace{.04 in}2 \: \in \: F \quad \quad \quad i \: = \: \operatorname{Im}(z)\hspace{-0.03 in}\cdot \hspace{-0.03 in}i\hspace{.04 in}/\operatorname{Im}(z) \: = \: \operatorname{Im}(z)\hspace{-0.03 in}\cdot \hspace{-0.03 in}i\hspace{.06 in}/\hspace{.04 in}|\hspace{-0.04 in}\operatorname{Im}(z)\hspace{-0.03 in}\cdot \hspace{-0.03 in}i| \: \in \: F$
$\operatorname{Im}(z) \; = \; \operatorname{Im}(z)\hspace{-0.03 in}\cdot \hspace{-0.03 in}i\hspace{.04 in}/\hspace{.04 in}i \; \in \; F \qquad \qquad \operatorname{Re}(z) \; = \; z-(\operatorname{Im}(z)\hspace{-0.03 in}\cdot \hspace{-0.03 in}i) \; \in \; F$
By the lemma, $\operatorname{Re}(z)$ and $\operatorname{Im}(z)$ are both in $E$.
$\DeclareMathOperator{\id}{id}$ I am editing my message yet again to bring you if not an answer, a few ideas.
What I was trying to find as a counter example was an ordered field $F$ equipped with its absolute value $| \ |_F$, a proper subfield $E$ and a morphism $\varphi: F_{>0} \rightarrow E_{>0}$ fixing $E_{>0}$ (we would then define $\varphi(0) := 0$ and $\forall x \in F_{>0}, \varphi(-x):= -\varphi(x)$) satisfying $\forall x,y \in F^{\times}, |\varphi(x+y)|_F \leq |\varphi(x)|_F + |\varphi(y)|_F$. The reason I thought this probably existed is that if $E^{\times},F^{\times}$ being abelian groups without torsion, there are plenty of morphisms $F_{>0} \rightarrow E_{>0}$ defined by choosing a rationally independant basis* of $E_{>0}$ and completing it into a rationally independant basis of $F_{>0}$, then taking projections or other sorts of endomorphisms. However, this does not insure the condition $\forall x,y \in F^{\times}, |\varphi(x+y)|_F \leq |\varphi(x)|_F + |\varphi(y)|_F$, and we even know that this condition can never hold in some cases, for instance if $E$ is dense in $F$, because it forces $\varphi$ to be continuous with respect to the order topology, and so $\varphi$ should be $\id_F$.
So I tried findind concrete examples rather than choice-based ones and I couldn't. It would be interesting to understand whether this type of method can work or not.
*it's like a basis over $\mathbb{Q}$ (every element is a unique linear combination in this basis with coefficients in $\mathbb{Q})$) except not every linear $\mathbb{Q}$-combination need have a meaning in the group because not every element need have a $n$-th root for every $n$. It exists (and can be completed like a regular basis can) for any abelian group without torsion, assuming AC.