OffArccosCut
plain-language theorem explainer
Predicate on a complex number that holds exactly when it lies off the classical real arccos cuts (−∞,−1] and [1,∞). Anyone tracking continuity of principal complex arccos (or of split dihedral cosines along the Wick arc) cites it. The body is a one-line Prop: nonzero imaginary part, or real part strictly inside (−1,1).
Claim. A complex number $w$ is off the arccos cut when either $\operatorname{Im}(w) \neq 0$, or $-1 < \operatorname{Re}(w) < 1$. Equivalently, $w$ avoids the closed real rays $(-\infty,-1]$ and $[1,\infty)$, the classical branch cuts of principal $\arccos$.
background
Module C11 formalizes a complex-first 4D Wick continuation of Regge hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The path is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian to Euclidean squared edge length; interior points stay in the open upper half-plane.
Dihedral cosines appear as split ratios of complex cofactors. Continuity of any principal log-based arccos requires the argument to stay off the real cuts $(-\infty,-1]$ and $[1,\infty)$. Mathlib has no Complex.arccos, so the safe open set is encoded directly as this predicate.
Related branch control uses the principal square root csqrt z = z^{1/2} with cut on $(-\infty,0]$ (complement of Complex.slitPlane). Both cuts feed the S3 branch-regularity model for the hinge continuation.
proof idea
Pure definition: a Prop on $w:\mathbb{C}$ equal to the disjunction “imaginary part nonzero, or real part strictly between $-1$ and $1$.” No lemmas, no tactics. It is the exact open set complementary to the classical real arccos cuts, written without naming a complex arccos function.
why it matters
Feeds BranchRegularOn, the S3 model predicate for branch regularity of the split-form hinge continuation: both diagonal Cayley–Menger cofactors stay in the slit plane (safe for csqrt), and the split cosine ratio satisfies this off-cut condition. That regularity is the branch certificate on the open arc interior for the path-selected hinge-data continuation.
Scope is deliberately hinge-data only (dihedral cosines and areas-squared). Full action-level continuation (wick_action_continuation_4d) remains open in the C12 lane; this predicate does not close that ledger gap. It is local analytic hygiene for the C11 Wick arc, not a gravity dynamics theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.