offArccosCut_slitPlane
plain-language theorem explainer
If a complex cosine value w avoids the classical arccos branch cuts, then both inputs to the principal-branch formula for complex arccos lie in the slit plane: 1−w² and w+I√(1−w²). Anyone building continuous complex dihedral angles along a Wick arc cites this. The proof splits real/imaginary cases for the first claim and obtains the second by contradiction via the product identity L·M=1.
Claim. Let $w\in\mathbb{C}$ lie off the classical arccos cuts (either $\mathrm{Im}\,w\neq 0$, or $\mathrm{Im}\,w=0$ and $-1<\mathrm{Re}\,w<1$). Then $1-w^2$ belongs to the slit plane $\mathbb{C}\setminus(-\infty,0]$, and so does $w+I\sqrt{1-w^2}$ (principal square root).
background
The module freezes the Wick-action continuation schema for a 4D causal simplex and builds the complex arccos lift used for dihedral angles along the arc $t:0\to 1$ (Lorentzian to Euclidean). Complex angle is defined by
$$\mathrm{carccos},w:=-I,\log\bigl(w+I,\mathrm{csqrt}(1-w^2)\bigr),$$
with the repo half-power $\mathrm{csqrt},z=z^{1/2}$ (branch cut on $(-\infty,0]$). Both $\log$ and $\mathrm{csqrt}$ are continuous only on the slit plane, so every input must stay off that ray.
OffArccosCut w is the open set where the classical real arccos cut is avoided: nonzero imaginary part, or real part strictly inside $(-1,1)$. The companion identity carccos_log_arg_mul_conj records that the two conjugate log-arguments multiply to 1 whenever $1-w^2\neq 0$. Upstream, csqrt is the principal branch via cpow, not Mathlib's missing Complex.sqrt.
proof idea
Two membership claims, both rewritten via mem_slitPlane_iff (positive real part, or nonzero imaginary part).
(i) For $1-w^2$: case on $\mathrm{Im},w=0$. On the real band, the real-part formula and $|\mathrm{Re},w|<1$ give $\mathrm{Re}(1-w^2)>0$. If $\mathrm{Re},w=0$ and $\mathrm{Im},w\neq 0$, the same real-part formula is positive by $\mathrm{Im}^2>0$. Otherwise $\mathrm{Im}(1-w^2)=-2,\mathrm{Re},w,\mathrm{Im},w\neq 0$.
(ii) For $L=w+I,\mathrm{csqrt}(1-w^2)$: assume not in the slit plane, so $\mathrm{Im},L=0$ and $\mathrm{Re},L\le 0$. Set $M=w-I,\mathrm{csqrt}(1-w^2)$. The product lemma gives $L\cdot M=1$, hence $M=L^{-1}$ and $\mathrm{Im},M=0$. Comparing imaginary parts forces $\mathrm{Im},w=0$ and $\mathrm{Re}(\mathrm{csqrt}(1-w^2))=0$. OffArccosCut then puts $w$ in the open real band, so $1-w^2$ is a positive real and $\mathrm{csqrt}$ is the positive real square root: contradiction.
why it matters
This is foundation lemma N1a in the Wave C4 R2 freeze: without slit-plane membership, the log/csqrt formula for complex dihedral angle is not even defined on the interior of the Wick path. Downstream, continuousOn_carccos (N1b) applies it pointwise to get continuity of carccos on OffArccosCut, and branchRegularSum_of_causal packages the same membership along the pentagonal hinge cosine path for $\alpha>7/12$.
In the Recognition gravity stack this underwrites the complex angle along the shared all-spacelike hinge of the three-pent object, where the structural collapse gives $\sum\theta=3\cdot\theta(t)$ and constant hinge area. It does not yet close the terminal wick_action_continuation_4d, nor N3 half-plane confinement, N4 cut-boundary, or Schläfli packaging; those remain later gaps. The decoy AND-shell deficitSumBranchOK is explicitly not inhabited here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.