isTimelike
plain-language theorem explainer
Boolean edge classifier for 3D CDT tetrahedra: marks which of the six edges are timelike under the two causal classes (3,1) and (2,2). Anyone assigning Lorentzian squared lengths or building the Wick map on a tetrahedron cites it. Pure pattern-match definition on the causal type, encoding the standard AJL edge tables.
Claim. For a causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$ and edge index $e\in\{0,\ldots,5\}$, return true precisely when $e$ is timelike. On type $(3,1)$ the timelike edges are $\{2,4,5\}$ (those incident to the apex); on type $(2,2)$ they are $\{1,2,3,4\}$ (the four cross-slice edges).
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in $D=3$. Prior discrete-gravity results in the repo are Euclidean; here the first certified Lorentzian layer is the CDT-style causal tetrahedron between adjacent spatial slices, following Ambjørn–Jurkiewicz–Loll conventions.
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$; three spacelike + three timelike edges) and $(2,2)$ (two vertices on each slice; two spacelike + four timelike). Spacelike edges carry $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$).
Vertex/edge indexing is the Cayley–Menger convention from edgeVertices: edges $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$. Slice assignment: for $(3,1)$, vertices ${0,1,2}$ on $t$ and $3$ on $t+1$; for $(2,2)$, ${0,1}$ on $t$ and ${2,3}$ on $t+1$. The companion inductive CausalTetType names the two classes.
proof idea
Definition by cases on the causal type, not a proved theorem. On threeOne the Boolean is the disjunction of edge indices $2,4,5$; on twoTwo it is the disjunction of $1,2,3,4$. No tactics or upstream lemmas are invoked; the tables are the combinatorial content. Separate decide lemmas (siblings such as the cross-slice equivalences) later certify that these tables match the geometric criterion "endpoints lie on different slices" via edgeVertices and sliceOf.
why it matters
This is the edge-type kernel of the 3D Lorentzian layer. Every squared-length assignment (Lorentzian and Euclideanized), the Wick map as $\alpha\mapsto -\alpha$ on the causal class, non-degeneracy of Euclideanized tets, and the deficit-angle reality corollary at $\alpha=1$ branch on it. Downstream 4D work in CausalSimplex4D mirrors the same pattern (euclideanSqEdges, positivity/scale lemmas, and the decide-verified cross-slice identities), so the 3D table is the prototype for the higher-dimensional edge-type assignment.
In the Recognition gravity program this closes the first combinatorial gap between Euclidean Regge data and a CDT-style Lorentzian sector in $D=3$, before any dynamical measure is introduced. It does not itself force $D=3$ (that is T8 upstream); it assumes the 3D CDT setting and supplies the edge typing that the Wick and non-degeneracy theorems consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.