I am looking for a proof of the following theorem: Given a vector $\textbf{a}$ in an inner product space, the mapping $\sqrt{\langle\textbf{a},\textbf{a}\rangle}$ is a norm of $\textbf{a}$.
This is shown by considering the axioms of the inner product ${\langle\textbf{a},\textbf{a}\rangle}$ and showing that $\sqrt{\langle\textbf{a},\textbf{a}\rangle}$ satisfies the axioms of a norm. The positive definite axiom holds for both norms and inner products. The absolute homogeneity axiom for a norm can also be shown in a few steps.
My problem is with proving that the triangle inequality holds for a function $f(\textbf{a}+\textbf{b})=\sqrt{\langle\textbf{a}+\textbf{b},\textbf{a}+\textbf{b}\rangle}$ such that $f(\textbf{a}+\textbf{b})\leq f(\textbf{a})+f(\textbf{b})$. The proofs I've seen use the Cauchy-Schwarz inequality to prove this step. My problem is that all proofs of Cauchy-Schwarz itself contain a step that assumes that $\sqrt{\langle\textbf{a},\textbf{a}\rangle} = ||\textbf{a}||$. But this is the relation we are trying to prove in the first place.
So is there a general proof of the Cauchy-Schwarz inequality that doesn't assume $\sqrt{\langle\textbf{a},\textbf{a}\rangle} = ||\textbf{a}||$? Or if such a proof doesn't exist: is there a proof of the norm-inner product equivalence theorem that doesn't seem to assume itself in its own proof? Unless I am misunderstanding something.
There's a bit of a logical mixup here.
You want to show, $x\mapsto\sqrt{\langle x,x\rangle}$ is a norm on any inner product space). The only axiom of a norm that is not immediate is the triangle inequality.
So you want to bound: $$\sqrt{\langle x+y,x+y\rangle}\le\sqrt{\langle x,x\rangle+\langle y,y\rangle+2\langle x,y\rangle}\le\sqrt{\langle x,x\rangle+\langle y,y\rangle+2\sqrt{\langle x,x\rangle\cdot\langle y,y\rangle}}$$Using the CBS inequality, and then from there you just observe: $$\sqrt{\langle x,x\rangle+\langle y,y\rangle+2\sqrt{\langle x,x\rangle\cdot\langle y,y\rangle}}=\sqrt{\langle x,x\rangle}+\sqrt{\langle y,y\rangle}$$Concluding the triangle inequality.
Now you object, because the CBS inequality is often stated as: $$\langle a,b\rangle^2\le\|a\|^2\|b\|^2$$Where $\|\cdot\|$ is "already a norm", or something. But really, when stating the CBS inequality and when proving it, the symbol "$\|\cdot\|$" is simply a placeholder for the symbol $\sqrt{\langle,\rangle}$ and the fact that $\|\cdot\|$ - so defined - is a genuine norm is not used.
So there is no problem at all.
The standard proof of the CBS inequality (real case): (this aspect of the post is very much a duplicate, save for the avoidance of norm notation - see here and here)
Fix $a,b$ and consider the map: $$f:\Bbb R\ni t\mapsto\langle a+tb,a+tb\rangle\in\Bbb R$$
We have: $$f(t)=t^2\langle b,b\rangle+2t\langle a,b\rangle+\langle a,a\rangle$$But also: $$f\ge0$$
So the discriminant must be nonpositive, i.e.: $$(2\langle a,b\rangle)^2-4\langle a,a\rangle\cdot\langle b,b\rangle\le0$$And then: $$\langle a,b\rangle^2\le\langle a,a\rangle\cdot\langle b,b\rangle$$Follows. Then: $$|\langle a,b\rangle|\le\sqrt{\langle a,a\rangle\cdot\langle b,b\rangle}$$Follows. This inequality can be used in the above proof that $x\mapsto\sqrt{\langle x,x\rangle}$ is a norm. There is absolutely no problem, and nowhere was the $\|\cdot\|$ notation needed or used.
If the space is a complex inner product space we use a very similar approach. Fix $a,b$ as before and define $f$ in the same way. Let $g:\Bbb C\to\Bbb R$ be the map: $$\lambda\mapsto|\lambda|^2\cdot\langle a,a\rangle+2|\lambda|\cdot|\langle a,b\rangle|+\langle b,b\rangle$$
Because: $$\begin{align}g(\lambda)&\ge|\lambda|^2\cdot\langle a,a\rangle+2\cdot\Re(\lambda\cdot\langle a,b\rangle)+\langle b,b\rangle\\&=\langle \lambda a+b,\lambda a+b\rangle^2\\&=f(|\lambda|)\\&\ge0\end{align}$$
For all $\lambda\in\Bbb C$, we conclude that the polynomial: $$\Bbb R\ni x\mapsto\langle a,a\rangle\cdot x^2+2|\langle a,b\rangle|\cdot x+\langle b,b\rangle\in\Bbb R$$Is nonnegative and so has nonpositive discriminant.
This discriminant is basically the same one as before, except with a modulus sign - you get: $$4|\langle a,b\rangle|^2-4\langle a,a\rangle\cdot\langle b,b\rangle\le0\implies|\langle a,b\rangle|^2\le\langle a,a\rangle\cdot\langle b,b\rangle$$