hingeEdges32C
plain-language theorem explainer
Complex edge-length 10-tuple for the (3,2) causal 4-simplex: every timelike cross-edge carries value z, every spacelike edge carries unit length. Wick-continuation and hinge-cofactor proofs in the Seven-Gaps campaign cite it as the canonical complex-first edge data at unit spacelike scale. The body is a one-line case split on the threeTwo timelike predicate.
Claim. For $z \in \mathbb{C}$, the squared edge-length assignment on the ten edges of the $(3,2)$ causal $4$-simplex with unit spacelike edges and common timelike value $z$: each edge $e$ is sent to $z$ if $e$ is timelike for type $(3,2)$, and to $1$ otherwise.
background
In 4d causal dynamical triangulations the two simplex types between adjacent time slices are $(4,1)$ and $(3,2)$. The $(3,2)$ type has three vertices on the lower slice and two on the upper; its six cross-slice edges are exactly the timelike ones (CausalSimplex4D.isTimelike), while the four edges inside each slice are spacelike.
This module runs lane B2 of the QG Seven-Gaps campaign: complex-first Wick continuation of all ten triangular hinges of the $(3,2)$ simplex at the physical point $a=1$, $\alpha=1$, along the canonical upper-half-plane arc. Edge data are packaged as a 10-tuple of complex squared lengths (SqEdges10C), indexed in lexicographic edge order.
The definition freezes spacelike squared lengths at $1$ and puts a single complex parameter $z$ on every timelike edge. Per the doc-comment it is the specialization of the general continuation tuple at unit spacelike values with $z$ equal to the arc coordinate.
proof idea
Pure definition, not a proof. The body is the function that, on each of the ten edges, returns $z$ when the edge is timelike for CausalPentType.threeTwo and returns $1$ otherwise. No lemmas are applied; noncomputable only because the ambient complex edge type is noncomputable.
why it matters
This is the shared edge-data spine for the entire $(3,2)$ hinge analysis. Downstream, continuationEdgesC_threeTwo identifies the physical-point continuation tuple with this definition at $z = \mathrm{arcZ},1,\alpha,t$. Branch-regularity and boundary-continuation theorems for mixed pairs and upper pairs (branchRegular_threeTwo_mixed_pair, boundary_threeTwo_mixed_pair, and the upper-pair analogues) take closed-form cofactor hypotheses stated directly in terms of cofactors of this edge tuple.
It also feeds the Cayley-Menger matrix construction (cmMatrixC_hingeEdges32) and the complete area-squared closed-form theorem across both causal types. In the Recognition gravity stack this is the concrete complex-first input that lets the Wick arc certificates close for all ten hinges of the $(3,2)$ simplex, including the honest Lorentzian endpoint contact on the spacelike hinge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.