csqrt
plain-language theorem explainer
Principal-branch complex square root, defined as $z^{1/2}$ via Mathlib's complex power. Every split-form dihedral denominator and branch-regularity predicate in the C11 Wick hinge continuation cites it. The body is a one-line wrapper of `Complex.cpow`; the nontrivial content is the documented branch cut on $(-\infty,0]$.
Claim. For $z \in \mathbb{C}$, set $\sqrt{z} := z^{1/2}$ using the principal complex power (equivalently $\exp(\Log z / 2)$ when $z \neq 0$). The branch cut is the nonpositive real axis $(-\infty, 0]$, i.e. the complement of the slit plane.
background
The ambient module is the complex-first 4D Wick continuation of Regge hinge data (QG Seven-Gaps lane C11). It continues Cayley–Menger areas-squared and cofactor dihedral cosines of a single causal 4-simplex along the upper-half-plane arc $z(t) = \alpha a^2 \exp(i\pi(1-t))$ from the Lorentzian endpoint $t=0$ to the Euclidean endpoint $t=1$.
Mathlib (this pin) has no Complex.sqrt. The substitute is the principal branch of complex power: $z^{1/2} = \exp(\log z / 2)$ off zero, continuous precisely on the slit plane (complement of $(-\infty,0]$). The module mandates the split denominator $\sqrt{C_{pp}}\cdot\sqrt{C_{qq}}$ rather than $\sqrt{C_{pp}C_{qq}}$, because the product form crosses the cut mid-arc.
Downstream, branch regularity requires both diagonal cofactors to stay in the slit plane so this square root remains continuous along the open arc interior.
proof idea
Pure definition: unfold to the Mathlib complex power $z^{(1/2:\mathbb{C})}$. No tactics, no lemmas. The companion identity $\mathrm{csqrt},z\cdot\mathrm{csqrt},z = z$ (for $z\neq 0$) is proved separately by cpow_add and cpow_one; that identity, not the definition itself, is what produces the Lorentzian endpoint sign factor $-1$.
why it matters
This is the primitive square-root atom for the entire C11 hinge continuation. It is the building block of the split dihedral denominator $\mathrm{csqrt}(C_{pp})\cdot\mathrm{csqrt}(C_{qq})$, of the branch-regularity predicate (both cofactors off the cut), and of the proved identity that $\mathrm{csqrt},z\cdot\mathrm{csqrt},z = z$ rather than $|z|$. That last fact is exactly the documented Lorentzian endpoint sign factor: at $C_{pp}=C_{qq}=-8$ the split denominator is $-8$, not $+8$, so the hinge cosine picks up a factor $-1$ relative to the real product-form value.
The module is deliberately hinge-data only; the FullTheoryLedger gap on genuine action-level continuation (C12) stays open. Within C11 this definition closes the Mathlib gap and locks the branch convention used by the hour-0 numeric gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.