continuationEdgesC_zero
plain-language theorem explainer
At the Lorentzian endpoint t=0 of the upper-half-plane Wick arc, the complex continued squared-edge 10-tuple of a causal 4-simplex equals the real Lorentzian edge data of CausalSimplex4D, coerced into ℂ. Gravity and CDT workers cite this as the t=0 endpoint identification for the C11 hinge-data continuation. The proof is a pointwise case split on timelike vs spacelike edges plus the arc evaluation at zero.
Claim. For every causal 4-simplex type $\mathrm{ty}\in\{\mathrm{fourOne},\mathrm{threeTwo}\}$ and real parameters $a,\alpha$, the complex continuation of squared edge lengths at parameter $t=0$ equals the real Lorentzian squared-edge assignment of that simplex, viewed in $\mathbb{C}$: $\mathrm{cont}(\mathrm{ty},a,\alpha;0)=e\mapsto\bigl(\ell^2_{\mathrm{Lor}}(\mathrm{ty},a,\alpha;e):\mathbb{R}\hookrightarrow\mathbb{C}\bigr)$.
background
Module C11 builds a complex-first Wick continuation of Regge hinge data (triangular areas-squared and dihedral cosines) for the two causal 4-simplex classes of 4d CDT: four-one and three-two. Squared edges are indexed by $\mathrm{Fin},10$ in lexicographic order. The continuation path on each timelike squared edge is the canonical upper-half-plane arc
$$z(t)=\alpha a^2\exp\bigl(i\pi(1-t)\bigr),\qquad t\in[0,1],$$
so $z(0)=-\alpha a^2$ (Lorentzian) and $z(1)=+\alpha a^2$ (Euclidean), matching the sign convention of the real Lorentzian and Euclidean edge maps in CausalSimplex4D.
Spacelike edges stay real and fixed; only timelike edges ride the arc. The real Lorentzian squared-edge map is the kernel-checked assignment used throughout the SevenGaps gravity stack. This theorem is the $t=0$ endpoint identification of that arc against that real map, after coercion $\mathbb{R}\to\mathbb{C}$.
proof idea
Term-mode proof by functional extensionality on the ten edges. Unfold the complex continuation and the real Lorentzian edge map. Case-split on whether the edge is timelike for the given simplex type.
- Timelike: both sides take the arc branch; rewrite with the positive
ifand apply the elementary evaluation that the arc at $t=0$ is $-\alpha a^2$ (as a complex number equal to the real Lorentzian value). - Spacelike: both sides take the fixed real branch; the two
if_negrewrites make the sides identical after coercion.
No analysis beyond the arc endpoint identity is required.
why it matters
Endpoint glue for the C11 Wick lane: without $t=0$ matching the real Lorentzian tuple, the path-selected continuation cannot be called a continuation of CausalSimplex4D data. Downstream, complex hinge areas-squared are built from the continued edge tuple, and the module-level realization theorem packages the full PATH-SELECTED continuation with a branch certificate on the open arc interior.
Framework role is narrow but mandatory inside the QG Seven-Gaps campaign (panel P1-remainder, flagship C11). It does not close the ledger gap wick_action_continuation_4d: the module explicitly leaves action-level continuation (interior-hinge complexes, C12) open. Landmarks touched are only the 4d causal simplex geometry and the Wick arc endpoints; no claim on $D=3$, $\phi$-ladder masses, or $\alpha$ numerics beyond the formal parameter $\alpha$ in the edge lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.