carccos
plain-language theorem explainer
Complex principal arccos via the log-lift formula arccos(w) = -i log(w + i √(1-w²)), with the repo principal square root applied only to 1-w². Gravity and Regge-calculus workers cite it as the angle map on the three-pent hinge cosine path under Wick rotation. The body is a one-line noncomputable definition; no proof obligations.
Claim. For $w \in \mathbb{C}$, define the complex principal arccos by $\operatorname{arccos}_{\mathbb{C}}(w) := -i \, \log\bigl(w + i \, \sqrt{1-w^{2}}\bigr)$, where $\sqrt{\cdot}$ is the principal branch (cut on $(-\infty,0]$) and $\log$ is the principal logarithm.
background
This module freezes the Wave C4 R2 schema for four-dimensional Wick action continuation: definitions, the certificate structure, and the named terminal proposition, without inhabiting that terminal. Arc convention is binding: $t=0$ Lorentzian, $t=1$ Euclidean. On the three-pent object the shared hinge is the all-spacelike triangle ${0,1,2}$; structural collapse makes all three dihedral cosine paths definitionally the same chart pair, so the angle sum is three times a single path angle and hinge area squared is the constant $3/16$.
The complex angle convention is fixed here: never apply the half-power to cofactor products, only to $1-w^{2}$, respecting the product-form-crossing kill. Upstream, csqrt is the principal-branch substitute $z^{1/2}=\exp(\log z/2)$ with cut on $(-\infty,0]$, and the hinge face is the Finset ${0,1,2}$ of the glued-pent witness.
proof idea
Pure definition: the body is the single term $(-I)\cdot\log(w+I\cdot\mathrm{csqrt}(1-w^{2}))$. No tactics, no lemmas applied at the definition site. Downstream continuity and evaluation lemmas expand this formula and invoke properties of principal log and csqrt.
why it matters
This is the binding complex-angle primitive for the frozen Wick-action path. Downstream assembly uses it for the pointwise Lorentzian cut value (equals $\pi-i,\mathrm{arcosh}(11/8)$), the decisive mismatch between that principal value and the one-sided cut limit, continuity of the composed path on $(0,1]$, and continuity of the full Wick action path (three times the angle times hinge area). Cut-limit lemmas also quote it for the $t\to 0^{+}$ anchor. It lands foundation pieces N1/N2 (off-cut slit plane and real-arccos agreement) without flipping any action-level Bool or attempting N3/N4, Schläfli, or packaging. In the broader RS gravity stack it supplies the complex dihedral angle needed before any Lorentzian action identity can be certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.