lorentzianSqEdges
plain-language theorem explainer
Assigns squared edge lengths to a 3d CDT tetrahedron of type (3,1) or (2,2): spacelike edges get $a^2$, timelike edges get $-(\alpha a^2)$. Anyone working the Lorentzian sector of the Seven-Gaps gravity lane cites this as the input tuple to Cayley-Menger and Wick maps. The body is a one-line case split on the combinatorial timelike predicate.
Claim. For a causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$ and real parameters $a,\alpha$, the Lorentzian squared-edge assignment is the map $e\mapsto a^2$ on spacelike edges and $e\mapsto -(\alpha a^2)$ on timelike edges, valued in the six squared lengths of a tetrahedron.
background
This module opens the Lorentzian lane of the QG Seven-Gaps campaign. Prior discrete-gravity work in the repo is Euclidean; here the first certified Lorentzian layer is built for 3d CDT (Ambjørn-Jurkiewicz-Loll). Spatial slices are equilateral triangulations with squared edge length $a^2$. Between slices $t$ and $t+1$ one fills with two tetrahedron types: $(3,1)$ (three vertices on $t$, one on $t+1$: 3 spacelike + 3 timelike edges) and $(2,2)$ (two vertices on each slice: 2 spacelike + 4 timelike).
CausalTetType is the inductive label of those two classes. Timelike vs spacelike is decided combinatorially from slice membership of the endpoints (isTimelike), with fixed vertex indexing from Geometry.CayleyMengerPolynomial: edges $0=(0,1),\ldots,5=(2,3)$. Squared lengths live in SqEdges := Fin 6 \to \mathbb{R}.
Convention: spacelike edges carry $a^2$; timelike edges carry $-\alpha a^2$ with $\alpha>0$ in the Lorentzian regime. Wick rotation is the sign flip on timelike lengths, equivalently the continuation $\alpha\mapsto -\alpha$.
proof idea
Pure definition, not a proof. The body is the function on Fin 6 that cases on isTimelike ty e: if the edge is timelike return $-(alpha * a^2)$, otherwise $a^2$. No lemmas are applied; the combinatorial content is deferred to the decide-able isTimelike predicates and the slice-count lemmas for $(3,1)$ and $(2,2)$.
why it matters
This is the Lorentzian edge-length seed for the whole causal-simplex stack. Downstream, the 4d sister module reuses the same pattern: LorentzianClass is the set of all such tuples with $a>0$, $\alpha>0$; the bordered Cayley-Menger matrices of types $(4,1)$ and $(3,2)$ are identified with the two-parameter families at $p=a^2$, $q=-(\alpha a^2)$; and the closed forms cm4 = -((8\alpha+3)a^8) and cm4 = -((12\alpha+7)a^8) feed the sign theorems lorentzian_cm4_neg_*, which show the Lorentzian tuples fail CM positivity and therefore need Wick rotation to reach the Euclidean sector.
In-module it is the domain object for the Wick involution, the Euclideanized non-degeneracy range, and the deficit-angle reality corollary at the physical point $\alpha=1$. It sits in the Lorentzian-sector lane of Seven-Gaps, not in the T0-T8 forcing chain, but it is the discrete-geometry bridge that lets Regge/CDT kinematics talk to the certified CM polynomial layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.