A real norm on C that is not a complex norm

Uniqueness of coordinates in [F1] makes the formula for $N$ well-defined. By [F4], $\mathrm{\mid }0{\mathrm{\mid }}_{\mathbb{R}}=0$, and since $2=1+1$, distributivity and the identity law give $N(0)=\mathrm{\mid }0{\mathrm{\mid }}_{\mathbb{R}}+2\mathrm{\mid }0{\mathrm{\mid }}_{\mathbb{R}}=0+(1+1)\mathrm{\mid }0{\mathrm{\mid }}_{\mathbb{R}}=0+0=0$. If $z\mathrm{\ne }0$, then [F1] gives $x\mathrm{\ne }0$ or $y\mathrm{\ne }0$. By [F4] and totality of the order in [F8], $\mathrm{\mid }x{\mathrm{\mid }}_{\mathbb{R}}\ge 0$ and $\mathrm{\mid }x{\mathrm{\mid }}_{\mathbb{R}}>0$ when $x\mathrm{\ne }0$; likewise $\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}\ge 0$ and $\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}>0$ when $y\mathrm{\ne }0$. Since $2=1+1>0$ by [F8] and [F9], distributivity and the identity law give $2\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}=(1+1)\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}=\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}+\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}$. By [F4], this is $0$ when $y=0$; when $y\mathrm{\ne }0$, [F4] and totality in [F8] give $\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}>0$, so closure under addition in [F8] makes the sum positive. Thus $2\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}\ge 0$, with strict positivity when $y\mathrm{\ne }0$. At least one of the two summands in $N(z)$ is therefore positive and the other is nonnegative. By trichotomy [F8], a nonnegative summand is either zero or positive; in the zero case adding it leaves the positive summand unchanged, and in the positive case [F8] makes their sum positive. Hence $N(z)>0$ for $z\mathrm{\ne }0$, while $N(0)=0$, proving separation in [F6].

For $r\in \mathbb{R}$ and $z=x+iy$, [F1] and [F2] give $r{\cdot }_{{\mathbb{C}}_{\mathbb{R}}}z=(rx)+i(ry)$. Hence $N(rz)=\mathrm{\mid }rx{\mathrm{\mid }}_{\mathbb{R}}+2\mathrm{\mid }ry{\mathrm{\mid }}_{\mathbb{R}}=\mathrm{\mid }r{\mathrm{\mid }}_{\mathbb{R}}\mathrm{\mid }x{\mathrm{\mid }}_{\mathbb{R}}+2\mathrm{\mid }r{\mathrm{\mid }}_{\mathbb{R}}\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}=\mathrm{\mid }r{\mathrm{\mid }}_{\mathbb{R}}N(z)$ by [F4] and field algebra; this is absolute homogeneity in [F6].

For $z=x+iy$ and $w=u+iv$, [F1] and [F5] give $\mathrm{\mid }x+u{\mathrm{\mid }}_{\mathbb{R}}\le \mathrm{\mid }x{\mathrm{\mid }}_{\mathbb{R}}+\mathrm{\mid }u{\mathrm{\mid }}_{\mathbb{R}}$ and $\mathrm{\mid }y+v{\mathrm{\mid }}_{\mathbb{R}}\le \mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}+\mathrm{\mid }v{\mathrm{\mid }}_{\mathbb{R}}$. Since $2>0$ by [F8] and [F9], the second inequality gives $2\mathrm{\mid }y+v{\mathrm{\mid }}_{\mathbb{R}}\le 2\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}+2\mathrm{\mid }v{\mathrm{\mid }}_{\mathbb{R}}$: equality remains equality after scaling, while a strict inequality remains strict by [F10]. By totality in [F8], each of these two weak inequalities is either equality or strict; if both are strict [F11] gives a strict inequality after addition, if exactly one is strict translation invariance in [F11] gives a strict inequality after addition, and if both are equal their sums are equal. Therefore $N(z+w)=\mathrm{\mid }x+u{\mathrm{\mid }}_{\mathbb{R}}+2\mathrm{\mid }y+v{\mathrm{\mid }}_{\mathbb{R}}\le \mathrm{\mid }x{\mathrm{\mid }}_{\mathbb{R}}+\mathrm{\mid }u{\mathrm{\mid }}_{\mathbb{R}}+2\mathrm{\mid }y{\mathrm{\mid }}_{\mathbb{R}}+2\mathrm{\mid }v{\mathrm{\mid }}_{\mathbb{R}}=N(z)+N(w)$. Together separation in step 1.1, homogeneity in step 1.2, and this triangle inequality verify the real norm axioms [F6].

The coordinates in [F1] and real absolute value in [F4] give $N(1)=\mathrm{\mid }1\mathrm{\mid }+2\mathrm{\mid }0\mathrm{\mid }=1$ and $N(i)=\mathrm{\mid }0\mathrm{\mid }+2\mathrm{\mid }1\mathrm{\mid }=2$. By [F3], $\mathrm{\mid }i{\mathrm{\mid }}_{\mathbb{C}}=\sqrt{1}=1$, since $1\ge 0$ and $1^2=1$. On the original complex vector space $\mathbb{C}$, complex homogeneity [F7] with $\lambda =i$ and $z=1$ would give $N(i)=\mathrm{\mid }i{\mathrm{\mid }}_{\mathbb{C}}N(1)=1$, contradicting $N(i)=2$ (indeed $2>1$ by translating $0<1$ using [F11] and [F9]). Thus the same function on the original complex structure is not complex homogeneous.