Can Hilbert spaces be defined over fields other than $\mathbb R$ and $\mathbb C$?
Let us assume for convenience that the embedding $K_\mathbb{R}\to\mathbb{R}$ is actually the inclusion map of a subfield of $\mathbb{R}$. Suppose $V$ is any nontrivial $K$-Hilbert space and let $x\in V$ be nonzero. For any $a\in K_\mathbb{R}$, we then have $\|ax\|^2=aa^*\|x\|^2$. It follows that $a^*\in K_\mathbb{R}$ and $a^*$ has the same sign as $a$. Thus $a\mapsto a^*$ is an order-preserving embedding of $K_\mathbb{R}$ into itself and therefore must be the identity (since it is the identity on $\mathbb{Q}$, which is order-dense in $K_\mathbb{R}$). That is, $a^*=a$ for all $a\in K_\mathbb{R}$. Now if $(a_n)$ is a sequence in $K_\mathbb{R}$ which converges to some $r\in\mathbb{R}$, the sequence $(a_nx)$ is Cauchy (since $\|a_nx-a_mx\|^2=(a_n-a_m)^2\|x\|^2$) and so converges to some $y\in V$. By continuity of the distance function on $V$, we must have $\|y\|^2=\lim_n \|a_nx\|^2=r^2\|x\|^2$. Since $r\in\mathbb{R}$ here is arbitrary, we have shown that the function $y\mapsto \langle y,y\rangle$ takes every nonnegative real value. Thus in fact $K_\mathbb{R}$ must be all of $\mathbb{R}$.
Now our field $K$ is an extension of $\mathbb{R}$ with an involutive automorphism $a\mapsto a^*$ which fixes $\mathbb{R}$ pointwise. Conversely, for any $a\in K$ such that $a=a^*$, we have $\|ax\|^2=a^2\|x\|^2\geq 0$ and thus $a^2\geq 0$, which implies $a\in\mathbb{R}$. That is, $\mathbb{R}$ is exactly the fixed field of the automorphism $a\mapsto a^*$. Thus $K$ is an extension of $\mathbb{R}$ of degree at most $2$ (specifically, of degree equal to the size of the group of automorphisms generated by $a\mapsto a^*$), and so it can only be $\mathbb{R}$ or $\mathbb{C}$.