[proofplan]
We derive the polarisation formula by expanding $q(v + w)$ using bilinearity and symmetry, then dividing by $2$ (which requires $\mathrm{Char}\,\mathbb{F} \neq 2$).
Existence is verified by defining $\psi$ via the polarisation formula and checking it is bilinear, symmetric, and recovers $q$.
Uniqueness follows because any symmetric bilinear form satisfying $q(v) = \phi(v, v)$ must be given by the same formula.
[/proofplan]
[step:Derive the polarisation formula from bilinearity and symmetry]
Suppose $\phi: V \times V \to \mathbb{F}$ is a bilinear form with $q(v) = \phi(v, v)$.
Expanding $q(v + w)$:
\begin{align*}
q(v + w) &= \phi(v + w, v + w) \\
&= \phi(v, v) + \phi(v, w) + \phi(w, v) + \phi(w, w) \\
&= q(v) + \phi(v, w) + \phi(w, v) + q(w).
\end{align*}
If $\phi$ is symmetric, $\phi(v, w) + \phi(w, v) = 2\phi(v, w)$, so:
\begin{align*}
\phi(v, w) = \frac{1}{2}\bigl(q(v + w) - q(v) - q(w)\bigr).
\end{align*}
Division by $2$ requires $\mathrm{Char}\,\mathbb{F} \neq 2$.
[guided]
The derivation uses a standard trick: expand the quadratic form at $v + w$ to "extract" the cross-term.
Starting from $q(v + w) = \phi(v + w, v + w)$ and distributing by bilinearity:
\begin{align*}
q(v + w) = \phi(v, v) + \phi(v, w) + \phi(w, v) + \phi(w, w) = q(v) + \phi(v, w) + \phi(w, v) + q(w).
\end{align*}
The cross-terms $\phi(v, w)$ and $\phi(w, v)$ appear as a sum.
If $\phi$ is symmetric, $\phi(w, v) = \phi(v, w)$, so the sum equals $2\phi(v, w)$.
Rearranging:
\begin{align*}
\phi(v, w) = \frac{1}{2}\bigl(q(v + w) - q(v) - q(w)\bigr).
\end{align*}
The hypothesis $\mathrm{Char}\,\mathbb{F} \neq 2$ is consumed here: we need $2 \neq 0$ in $\mathbb{F}$ to divide.
This formula shows that if a symmetric bilinear form $\phi$ exists with $q(v) = \phi(v, v)$, it must be given by this expression.
This already proves uniqueness; existence requires verifying the formula actually defines a bilinear form.
[/guided]
[/step]
[step:Verify existence by checking the polarisation formula defines a symmetric bilinear form recovering $q$]
Define $\psi: V \times V \to \mathbb{F}$ by
\begin{align*}
\psi(v, w) = \frac{1}{2}\bigl(q(v + w) - q(v) - q(w)\bigr).
\end{align*}
**Symmetry:** The expression is symmetric in $v$ and $w$ since $q(v + w) = q(w + v)$.
So $\psi(v, w) = \psi(w, v)$.
**Bilinearity:** Since $q$ is a quadratic form, there exists a (not necessarily symmetric) bilinear form $\phi$ with $q(v) = \phi(v, v)$.
From the derivation in the previous step, $\psi(v, w) = \frac{1}{2}(\phi(v, w) + \phi(w, v))$.
This is a sum of bilinear maps scaled by $\frac{1}{2}$, hence bilinear.
**Recovery of $q$:** We compute $\psi(v, v) = \frac{1}{2}(q(2v) - 2q(v))$.
Since $q(2v) = \phi(2v, 2v) = 4\phi(v, v) = 4q(v)$:
\begin{align*}
\psi(v, v) = \frac{1}{2}(4q(v) - 2q(v)) = q(v).
\end{align*}
[guided]
We must verify that the formula $\psi(v, w) = \frac{1}{2}(q(v + w) - q(v) - q(w))$ actually defines a symmetric bilinear form that recovers $q$.
Symmetry is immediate: swapping $v$ and $w$ does not change $q(v + w)$, and the subtracted terms are also symmetric.
For bilinearity, note that $q$ is a quadratic form, so by definition there exists some bilinear form $\phi$ (possibly not symmetric) with $q(v) = \phi(v, v)$.
The derivation in the previous step shows that the polarisation formula applied to $q$ yields $\psi(v, w) = \frac{1}{2}(\phi(v, w) + \phi(w, v))$.
Both $(v, w) \mapsto \phi(v, w)$ and $(v, w) \mapsto \phi(w, v)$ are bilinear, so their average $\psi$ is bilinear.
To check $\psi$ recovers $q$:
\begin{align*}
\psi(v, v) = \frac{1}{2}\bigl(q(v + v) - q(v) - q(v)\bigr) = \frac{1}{2}\bigl(q(2v) - 2q(v)\bigr).
\end{align*}
Now $q(2v) = \phi(2v, 2v) = 4\phi(v, v) = 4q(v)$, so $\psi(v, v) = \frac{1}{2}(4q(v) - 2q(v)) = q(v)$.
[/guided]
[/step]
[step:Establish uniqueness from the forced polarisation formula]
If $\psi_1$ and $\psi_2$ are both symmetric bilinear forms with $\psi_1(v, v) = \psi_2(v, v) = q(v)$ for all $v$, then the derivation in Step 1 shows both must satisfy
\begin{align*}
\psi_k(v, w) = \frac{1}{2}\bigl(q(v + w) - q(v) - q(w)\bigr)
\end{align*}
for $k = 1, 2$.
Since the right-hand side depends only on $q$, $\psi_1 = \psi_2$.
[/step]
