hingeEdgesC
plain-language theorem explainer
Defines the two-value complex squared-edge tuple for a (4,1) causal 4-simplex: every timelike edge is set to a complex parameter z, every spacelike edge to 1. Downstream Cayley-Menger cofactor and area-squared closed forms cite this as the canonical hinge-data input along the Wick arc. The body is a one-line pointwise case split on the fourOne timelike predicate.
Claim. For $z \in \mathbb{C}$, the map $e \mapsto z$ on timelike edges of a $(4,1)$ causal 4-simplex and $e \mapsto 1$ on spacelike edges, as a function $\mathrm{Fin}\,10 \to \mathbb{C}$ of squared edge lengths in lexicographic edge order.
background
Module C11 formalizes complex-first 4D Lorentzian Wick continuation of Regge hinge data (Cayley-Menger areas-squared and cofactor dihedral cosines) for the causal 4-simplex classes of CausalSimplex4D. Scope is hinge-data only; full action-level continuation remains open (C12 / ledger gap).
A $(4,1)$ simplex has four vertices on one time slice and one on the next. Squared edge lengths are indexed by $\mathrm{Fin},10$ (lex order). The complex edge table is the type $\mathrm{Fin},10 \to \mathbb{C}$. Timelike vs spacelike edges are classified by the fourOne instance of the causal edge predicate.
The Wick path on the timelike squared length is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian $z(0)=-\alpha a^2$ to Euclidean $z(1)=+\alpha a^2$. This definition freezes spacelike edges at unit value and leaves the single complex timelike value free, matching the physical continuation at $z=z(t)$.
proof idea
Definition, not a proof. Pointwise: on each edge index $e$, if the edge is timelike for the $(4,1)$ type then return $z$, else return $1$. No lemmas; pure case split on the boolean timelike classifier.
why it matters
Canonical two-value input for the entire C11 hinge-data pipeline. Immediate parents: the physical-point identification (continuation at $z=z(t)$ equals this tuple), the explicit Cayley-Menger matrix theorem for the two-value tuple, closed cofactors $C_{pp}=C_{qq}=6z-2$ and $C_{pq}=1-2z$, and the hinge area-squared formula $\mathrm{area}^2=z/4-1/16$. Boundary fourOne spacelike/timelike pair results in the all-hinges module also consume it.
It packages the S1 arc specialization (unit spacelike, free timelike $z$) so every later closed form can unfold against a single named edge table rather than a general continuation. Does not close the ledger gap on action-level continuation; that stays open pending interior-hinge complexes (C12).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.