hingeAreaSq_interior_off_cut
plain-language theorem explainer
On the open Wick arc interior t ∈ (0,1), the complex area-squared of the (0,1,4) triangular hinge of a continued (4,1) causal 4-simplex lies in the complex slit plane, hence off the principal square-root branch cut. C11 Wick-continuation and Regge-hinge workers cite this to license complex square roots of hinge areas along the path. The proof rewrites to the closed form z/4 − 1/16 and uses strict positivity of Im(zArc t).
Claim. For every real $t \in (0,1)$, the complex hinge area-squared of vertices $0,1,4$ evaluated on the Wick-continued squared-edge data of a $(4,1)$ causal $4$-simplex at arc parameter $t$ belongs to the complex slit plane $\mathbb{C}\setminus(-\infty,0]$.
background
Module C11 formalizes a complex-first 4D Lorentzian Wick continuation of Regge hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) for the causal 4-simplex classes of CausalSimplex4D. The path on the timelike squared edge is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ for $t\in[0,1]$, with Lorentzian endpoint at $t=0$ and Euclidean endpoint at $t=1$; the open interior lies strictly in the upper half-plane.
Hinge area-squared is the complex Cayley–Menger quantity for a triangular face of the continued edge 10-tuple. The complex slit plane is the standard domain of the principal square root (complex plane minus the non-positive real axis). The doc-comment records that on the open interior one has $\mathrm{Im}(z/4-1/16)=\mathrm{Im}(z)/4>0$, while at the Lorentzian endpoint the value sits on the cut boundary at $-5/16$ (allowed endpoint contact).
Scope is hinge-data only: action-level continuation of a full interior-hinge complex is the separate C12 question and remains open on the FullTheoryLedger.
proof idea
Tactic proof. Rewrite the continued edges to their physical form and the hinge area-squared to its closed expression (continuationEdgesC_physical, hingeAreaSqC_closed), which reduces the claim to membership of $z(t)/4-1/16$ in the slit plane.
Apply the slit-plane membership criterion and take the right disjunct (nonzero imaginary part). From zArc_im_pos on $t\in(0,1)$ one has $\mathrm{Im}(z(t))>0$. A short imaginary-part calculation gives $\mathrm{Im}(z(t)/4-1/16)=\mathrm{Im}(z(t))/4$. Division by the positive constant 4 preserves positivity, so the imaginary part is nonzero, hence the value lies off the cut.
why it matters
Branch certificate for the area-squared factor along the open Wick arc: without it, complex square roots of hinge areas are not justified on the interior path. Downstream, product_form_crossing uses the same continued edge data to show that at an interior parameter tStar the product of traced diagonal cofactors equals −32, which lies on the csqrt cut; that negative certificate kills the literal single-sqrt product transcription of the 3D dihedral denominator and forces the split form dihedralDenomSplitC.
Together these results underwrite the path-selected boundary-continuation theorem (S4) for split-form cosine data on the closed interval. Framework role is local to the QG Seven-Gaps C11 lane (panel P1-remainder): hinge-data Wick continuation of causal 4-simplex classes, not a claim about continuum Einstein–Hilbert action or the still-open ledger gap wick_action_continuation_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.