realized
plain-language theorem explainer
Path-selected Wick continuation of causal 4-simplex hinge data: complex Cayley–Menger areas-squared and split-denominator dihedral cosines along the upper-half-plane arc from Lorentzian to Euclidean squared edges. QG Seven-Gaps C11 cites it for a full-open-interior branch certificate on the fourOne timelike hinge. The top-level statement is still a sorry stub; sibling hinge lemmas are the intended discharge path. Action-level Regge continuation (C12) is explicitly not claimed.
Claim. Along the arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ for $t\in[0,1]$, with Lorentzian endpoint $z(0)=-\alpha a^2$ and Euclidean endpoint $z(1)=+\alpha a^2$, the complexified hinge data of a causal 4-simplex (triangular areas-squared and cofactor dihedral cosines with split square-root denominator $\sqrt{C_{pp}}\sqrt{C_{qq}}$) admit a path-selected continuation that is branch-regular on the full open interior $(0,1)$ and continuous on the closed interval $[0,1]$ at the traced fourOne timelike hinge (physical point $a=1$, $\alpha=1$).
background
Module setting is the QG Seven-Gaps C11 lane: complex-first 4D Wick continuation of hinge data for the causal 4-simplex classes of CausalSimplex4D, not the full Regge action. Squared edge lengths are the ten complex entries of a 4-simplex; the bordered Cayley–Menger matrix supplies 5×5 minors whose cofactors enter the dihedral cosine.
The continuation path is the canonical upper-half-plane arc $z(t)=\alpha a^2 e^{i\pi(1-t)}$, matching the repo Lorentzian/Euclidean endpoint sign convention. Mathlib supplies no Complex.sqrt; the local square root is $z^{1/2}$ via principal cpow/log, discontinuous on $(-\infty,0]$. Branch regularity therefore means slit-plane membership for every square-root argument and off-cut conditions for any log-based arccos.
Hour-0 numerics killed the product denominator $\sqrt{C_{pp}C_{qq}}$: interior arc points land on the cut (e.g. $C_{pp}C_{qq}=-32$ at $\mathrm{Re},z=1/3$). The split form $\sqrt{C_{pp}}\sqrt{C_{qq}}$ is mandatory. Upstream constants (alpha, spatial $D=3$, RS-native units) fix the physical calibration point; they do not supply the complex analysis.
proof idea
Declared proof style is a sorry stub: the top-level certificate is not yet discharged in-kernel.
Intended shape, from the module receipts and sibling names: (1) complexify edges, CM matrix, minors, cofactors, and the split dihedral denominator; (2) specialize to the fourOne timelike hinge (triangle $(0,1,4)$, opposite pair $(2,3)$) at $a=\alpha=1$, where closed forms $C_{pp}=C_{qq}=6z-2$, $C_{pq}=1-2z$, area-squared $z/4-1/16$ are available; (3) prove branch regularity on all of $(0,1)$ by slit-plane and arccos-cut avoidance from $\mathrm{Im},z>0$; (4) identify the split cosine with the cut-free rational $(1-2z)/(6z-2)$ and obtain continuity on $[0,1]$ with endpoint values $-3/8$ (Lorentzian, including the documented split-vs-real sign factor) and $-1/4$ (Euclidean). Supporting lemmas named in-module include the product-form crossing counterexample and the Lorentzian endpoint sign factor.
why it matters
Fills the C11 hinge-data Wick lane under the panel mandate PROCEED-WITH-MANDATE: a path-selected continuation with an interior branch certificate, rather than an untracked numeric animation. It records why split square roots are forced and memorializes exact cut-crossing failures of the product form.
Downstream graph edges touch alpha-band and regular-neighborhood surface packages, but the scientific parent obligation is the still-open FullTheoryLedger gap wick_action_continuation_4d / action-level continuation status. That gap is C12: interior-hinge complexes, deficit angles, and the continued Regge action itself. Nothing here flips that ledger flag.
Relative to the Recognition forcing chain, this is gravity/Regge infrastructure in $D=3$ spatial dimensions with calibrated $\alpha$, not a T5–T8 uniqueness step. It constrains how Lorentzian hinge cosines may be reached from Euclidean data without crossing Mathlib's principal branch cuts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.