continuationEdgesC_one
plain-language theorem explainer
At the Euclidean endpoint t = 1 of the upper-half-plane Wick arc, the complex continued squared-edge 10-tuple of a causal 4-simplex equals the real Euclideanized edge tuple of CausalSimplex4D, coerced into ℂ. Anyone matching the complex-first C11 continuation against the kernel-checked Euclidean data cites this endpoint identity. The proof is a pointwise case split on timelike vs spacelike edges plus the arc evaluation at t = 1.
Claim. For every causal 4-simplex type $\mathrm{ty}\in\{\mathrm{4+1},\mathrm{3+2}\}$ and real parameters $a,\alpha$, the complex continued squared-edge map at arc parameter $t=1$ equals the function $e\mapsto (\ell_E^2(\mathrm{ty},a,\alpha;e):\mathbb{C})$, where $\ell_E^2$ is the real Euclideanized (Wick-rotated) squared edge length from the causal 4-simplex edge table.
background
Module C11 builds a complex-first Wick continuation of hinge data (triangular areas-squared and dihedral cosines) for the two CDT causal 4-simplex classes fourOne and threeTwo. Squared edges are indexed by Fin 10 in lexicographic order. The canonical arc on each timelike squared edge is $z(t)=\alpha a^2\exp(i\pi(1-t))$ for $t\in[0,1]$, so $z(0)=-\alpha a^2$ (Lorentzian) and $z(1)=+\alpha a^2$ (Euclidean), matching the repo sign convention for lorentzianSqEdges / euclideanSqEdges.
continuationEdgesC assembles the complex 10-tuple along that path: timelike edges follow the arc, spacelike edges stay at their real Euclidean values. isTimelike selects which edges of the given causal type are continued. The companion endpoint lemma at $t=0$ identifies the Lorentzian side; this lemma is the Euclidean side.
Scope is deliberately hinge-data only. Full action-level continuation on an interior-hinge complex is the separate C12 question and remains open in the FullTheoryLedger.
proof idea
Term-mode proof by functional extensionality on the edge index $e$. Unfold both continuationEdgesC and euclideanSqEdges, then case on whether the edge is timelike for the given causal type.
If timelike, both sides take the if_pos branch; the complex arc at $t=1$ reduces by arcZ_one to the real Euclidean squared length coerced to $\mathbb{C}$. If not timelike, both sides take the if_neg branch and agree immediately (spacelike edges are never rotated). No further algebraic identities are needed.
why it matters
Endpoint identification is the Euclidean half of the S1 arc contract in the C11 mandate: the complex path must land exactly on the kernel-checked real Euclidean edge tuple of CausalSimplex4D. Downstream, hingeAreaSqC consumes complex edge 10-tuples, so this lemma lets Euclidean hinge areas-squared be read as the $t=1$ specialization of the continued data. The module-level realized theorem packages the path-selected continuation with a branch certificate on the open arc interior; both endpoints must match before that story is closed.
In the QG Seven-Gaps campaign this is panel-locked flagship lane C11 (hinge-data Wick continuation), not a claim that the full Regge action continues. The ledger gap wick_action_continuation_4d stays open. Framework-wise it is pure gravitational scaffolding on causal simplices, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.