isTimelike_twoTwo_eq_crossSlice
plain-language theorem explainer
For the (2,2) CDT tetrahedron, an edge is timelike exactly when its endpoints lie on opposite spatial slices. Combinatorial gravity and Regge/CDT workers cite this to certify the 2-spacelike/4-timelike edge multiset from the slice assignment alone. The proof is a pure `decide` over the six edges.
Claim. For every edge $e$ among the six edges of a tetrahedron, the edge is timelike in the causal type $(2,2)$ if and only if the two endpoints of $e$ lie on different spatial slices (one on slice $t$, one on slice $t+1$).
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign. Prior discrete-gravity results in the stack are Euclidean; here the first certified Lorentzian layer is built for 3D CDT (Ambjørn–Jurkiewicz–Loll). Between adjacent spatial slices one fills spacetime with two tetrahedron classes: type $(3,1)$ (three vertices on $t$, one on $t+1$) and type $(2,2)$ (two vertices on each slice).
Slice membership is the Boolean map sending each of the four vertices to slice $t$ or $t+1$. For $(2,2)$ the convention is vertices ${0,1}$ on $t$ and ${2,3}$ on $t+1$. Edges are indexed as in the Cayley–Menger setup: edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$. An edge is declared timelike precisely when it joins the two slices; spacelike edges stay inside one slice and carry squared length $a^2$, while timelike edges carry $-\alpha a^2$ ($\alpha>0$).
The companion statement for type $(3,1)$ is the same cross-slice identity. Together they pin the edge-type assignment used by the Wick map $\alpha\mapsto -\alpha$ and by later non-degeneracy and deficit-angle results.
proof idea
One-line proof by the decide tactic. Both sides are Boolean-valued functions of a finite index $e:\mathrm{Fin},6$: the left-hand side is the hardcoded timelike predicate for type $(2,2)$, the right-hand side compares slice labels of the two endpoints returned by edgeVertices. Exhaustive evaluation on the six edges discharges the universal quantifier with no lemmas and no arithmetic.
why it matters
The identity is the combinatorial certificate that type $(2,2)$ really has two spacelike and four timelike edges, matching the CDT dictionary in the module header. It sits in the first block of the Lorentzian layer: causal tetrahedron classes with spacelike/timelike assignment verified from slice structure by decidable lemmas, before the Wick involution, Euclideanized non-degeneracy, and the deficit-angle reality corollary at $\alpha=1$.
No downstream theorem currently depends on it (used-by count is zero), so it is infrastructure rather than a cited lemma in a longer chain. In the broader Recognition stack it supports the gravity lane’s move from Euclidean Regge data to a Lorentzian sector in $D=3$, consistent with the forcing-chain landmark that spatial dimension is three. It does not itself touch mass ladders, $\alpha$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.