csqrt_mul_self
plain-language theorem explainer
Principal-branch complex square root satisfies √z · √z = z (not |z|) for every nonzero z. Gravity and Wick-continuation proofs cite this when collapsing split-form dihedral denominators and when certifying arccos log-arguments. The proof unfolds the cpow definition, adds the half-exponents, and reduces to z^1 = z.
Claim. For every $z \in \mathbb{C}$ with $z \neq 0$, if $\sqrt{z}$ denotes the principal-branch square root $z^{1/2}$, then $\sqrt{z}\cdot\sqrt{z}=z$ (equality to $z$, not to $|z|$).
background
The ambient module builds a complex-first 4D Wick continuation of Regge hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) along the upper-half-plane arc from the Lorentzian to the Euclidean squared-edge endpoint. Honest scope is hinge-data continuation only; full action-level continuation remains open.
The local square root is the principal branch via complex power: $\mathrm{csqrt},z := z^{1/2}=\exp(\log z/2)$ for $z\neq 0$, with the usual cut on $(-\infty,0]$. Mathlib in this pin has no Complex.sqrt, so this is the faithful substitute. The hour-0 gate forces a split denominator $\sqrt{C_{pp}}\cdot\sqrt{C_{qq}}$ rather than $\sqrt{C_{pp}C_{qq}}$, because the product form hits the cut mid-arc (the negative certificate is the companion crossing theorem at an interior parameter where $C_{pp}C_{qq}=-32\notin$ the slit plane).
The identity proved here is the algebraic glue that lets the two split roots multiply back to the cofactor itself, and it is the documented source of the Lorentzian endpoint sign factor (equality to $z$, not modulus).
proof idea
Short tactic proof. Unfold the definition to $z^{1/2}$. Rewrite the product via Complex.cpow_add (valid because $z\neq 0$) as $z^{1/2+1/2}$. Discharge $1/2+1/2=1$ by norm_num, then apply Complex.cpow_one to obtain $z^1=z$. No case splits on the cut and no continuity argument.
why it matters
This is the elementary branch identity that every split-form cosine collapse in the C11 Wick lane rests on. Downstream, the hinge cosine path equals the cut-free Möbius rational $(1-2z)/(6z-2)$ because the two split square roots multiply back to the non-vanishing cofactor $6z-2$; the same pattern appears for the pent-hinge and four-one/three-two class collapses. Interior-hinge work uses it to show $(w+i\sqrt{1-w^2})(w-i\sqrt{1-w^2})=1$ for the complex arccos log argument. Cut-limit theorems that keep $\mathrm{Im},\log$ nonnegative near the Lorentzian end also invoke the same multiplication.
In the Seven-Gaps campaign this closes the algebraic half of the split-sqrt mandate: the product form is killed by the crossing certificate, while the split form is justified precisely because $\sqrt{z}\cdot\sqrt{z}=z$ restores the cofactor without re-entering the cut. It does not touch the still-open ledger gap on genuine action-level interior-hinge continuation (C12).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.