endpoint_cofactor_on_sqrt_cut
plain-language theorem explainer
At the Lorentzian endpoint of the Wick arc for the (4,1) causal 4-simplex, the traced hinge's diagonal Cayley-Menger cofactor equals exactly -8, which lies on the principal square-root branch cut. Anyone citing the open-interior branch certificate or the product-form FAIL needs this endpoint disclosure. The proof rewrites the cofactor at t=0 to a real polynomial identity, then rules out slit-plane membership by the standard real-part criterion.
Claim. For the complex Cayley-Menger cofactor of the Wick-continued squared edges of the $(4,1)$ causal 4-simplex at arc parameter $t=0$ (Lorentzian endpoint, unit scale), the $(3,3)$ diagonal entry equals $-8$, and $-8\notin\mathbb{C}\setminus(-\infty,0]$ (i.e., $-8$ lies on the principal square-root branch cut).
background
Module C11 formalizes a complex-first 4D Wick continuation of Regge hinge data (complex 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 $z(0)$ Lorentzian and $z(1)$ Euclidean.
The complex cofactor cmCofactorC is the Cayley-Menger minor used to build dihedral cosines; the split denominator dihedralDenomSplitC is mandatory because a single product-form square root hits the cut in the interior. The principal branch domain is the complex slit plane $\mathbb{C}\setminus(-\infty,0]$.
This theorem is the endpoint cut-contact disclosure: the branch certificate is stated only on the open arc interior, while endpoint hinge cosines remain exact via the cut-free Möbius collapse of the split form.
proof idea
Term-mode constructor splits the conjunction.
Left conjunct: rewrite the continued edges at the physical Lorentzian endpoint (continuationEdgesC_physical), specialize the $(3,3)$ cofactor identity (cofactor_pp), and evaluate the arc at $t=0$ (zArc_zero); the resulting real algebraic identity is discharged by ring, giving exactly $-8$.
Right conjunct: assume $-8$ lies in the slit plane, unfold Complex.mem_slitPlane_iff, simplify, and obtain a contradictory real inequality by linarith (negative reals are excluded from the open slit plane).
why it matters
Honest scope for the C11 Wick lane: the open-interior branch certificate cannot cover the Lorentzian endpoint because the diagonal cofactor sits on the csqrt cut. Downstream, product_form_crossing uses the same cut language for the interior FAIL event $C_{pp}C_{qq}=-32\notin$ slit plane, which kills the literal single-sqrt product transcription of the 3D dihedral denominator and forces the split form. The module-level realized theorem packages the path-selected continuation with a proved branch certificate only on the full open arc interior.
Endpoint hinge values stay exact (hingeCosPath_zero) because the split form collapses to a cut-free rational function (hingeCosPath_eq_moebius). This does not close the FullTheoryLedger gap wick_action_continuation_4d; action-level continuation remains the separate C12 question. No T0-T8 forcing step is claimed here; the result is pure complex geometry of the Regge hinge under Wick rotation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.