lorentzianSqEdges
plain-language theorem explainer
Assigns the ten squared edge lengths of a 4D CDT causal simplex: spacelike edges get a², timelike edges get −α a². Anyone working the Lorentzian Cayley–Menger lane or the Wick map cites this as the canonical edge tuple. The body is a one-line pointwise conditional on the combinatorial timelike predicate.
Claim. For a causal 4-simplex type $\mathrm{ty}\in\{(4,1),(3,2)\}$ and real parameters $a,\alpha$, the Lorentzian squared-edge assignment on the ten lexicographic edges is $s_e=a^2$ if $e$ is spacelike for $\mathrm{ty}$, and $s_e=-\alpha a^2$ if $e$ is timelike.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a): CDT-style causal 4-simplices between adjacent spatial slices, with Wick rotation as an explicit map on squared edge lengths and exact Cayley–Menger evaluation via the bordered determinant cmDetN.
Spatial slices are equilateral 3-complexes with squared edge $a^2$. Between slices one fills with type $(4,1)$ (four vertices on $t$, one on $t+1$: six spacelike + four timelike) or type $(3,2)$ (three + two: four spacelike + six timelike). The inductive type CausalPentType names these two classes; SqEdges10 is the type of real 10-tuples indexed by lexicographic edges on five vertices.
Timelike vs spacelike is decided combinatorially from the slice partition (isTimelike). In the Lorentzian regime $\alpha>0$, spacelike edges carry $a^2$ and timelike edges carry $-\alpha a^2$; the Euclideanized twin flips the timelike sign (continuation $\alpha\mapsto -\alpha$).
proof idea
Pure definition: a function on Fin 10 that branches on isTimelike ty e. If the edge is timelike for the given causal type, emit $-(alpha * a^2)$; otherwise emit $a^2$. No lemmas, no tactics.
why it matters
This is the seed data for the entire Lorentzian sector of the module. Downstream, LorentzianClass is exactly the set of such tuples with $a>0$ and $\alpha>0$. The bordered CM matrices specialize as cmMatrixN_lorentzian_fourOne / threeTwo to the two-parameter pent matrices at $p=a^2$, $q=-\alpha a^2$, and the closed forms cm4_lorentzian_fourOne ($=-(8\alpha+3)a^8$) and cm4_lorentzian_threeTwo ($=-(12\alpha+7)a^8$) feed the strict negativity theorems lorentzian_cm4_neg_*.
Those sign facts are the kinematical reason a Wick rotation (continuation $\alpha\mapsto -\alpha$) is required to reach the Euclidean non-degeneracy thresholds. The construction sits in the gravity/CDT lane of Recognition Science, with $D=3$ spatial slices forced upstream (T8) and the eight-tick/octave structure elsewhere; here the content is pure 4-simplex kinematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.