Lemma: Conditional polarization of the root identity

Suppose (eq:root-identity) holds for every metric in a real vector space of smooth inputs, with fixed $f,g,\varphi$ and root. Suppose $J_D$ is homogeneous quadratic there.

Polarization of the diagonal insertion then equals the root paired with the polarized source. Its complex bilinear extension satisfies, on the witness,

provided the real cosine and sine inputs and their required sums belong to that real domain.

Proof. Apply (eq:root-identity) to ${\gamma }_1+{\gamma }_2$, ${\gamma }_1$, and ${\gamma }_2$. Subtract and divide by two. Linearity of the integral gives the polarized source (eq:polarization).

For real inputs $a,b,c,d$, complex bilinear extension has the unique four-term form

Apply the same expansion to the polarized source and use Proposition prop:pair.