isTimelike_threeOne_eq_crossSlice
plain-language theorem explainer
For a 3d CDT tetrahedron of type (3,1), an edge is timelike exactly when its two endpoints sit on different spatial slices. Anyone checking the combinatorial edge-type table against the AJL slice assignment will cite this. The proof is a pure finite case split discharged by `decide`.
Claim. For every edge $e \in \{0,\ldots,5\}$ of a causal tetrahedron of type $(3,1)$, the edge is timelike if and only if the two endpoints of $e$ (under the standard edge-to-vertex map) lie on different slices.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign. All prior discrete-gravity results in the repo are Euclidean; here one builds certified CDT-style tetrahedron classes in $D=3$ and a kinematical Wick rotation on squared edge lengths.
In 3d CDT (Ambjørn–Jurkiewicz–Loll), spacetime between adjacent spatial slices is filled by two tetrahedron types. Type $(3,1)$ places vertices ${0,1,2}$ on slice $t$ and vertex $3$ on slice $t+1$, giving three spacelike and three timelike edges. Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ with $\alpha>0$.
Slice membership is the Boolean map sending a vertex to false on slice $t$ and true on $t+1$. The edge-to-vertex convention is the standard Cayley–Menger indexing: edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$. Timelike means the edge joins the two slices.
proof idea
One-line proof by decide. Both sides of the equality are Boolean-valued functions of a finite index $e:\mathrm{Fin},6$, built from the explicit lookup tables for slice membership, edge endpoints, and the hardcoded timelike mask for type $(3,1)$. Lean exhausts the six cases and checks Boolean equality in each.
why it matters
This is the first certified check that the combinatorial timelike mask for type $(3,1)$ agrees with the geometric cross-slice criterion. The module doc lists it under item 1 of the Lorentzian layer: spacelike/timelike edge-type assignment verified combinatorially from the slice structure by decide-able lemmas. The sibling statement for type $(2,2)$ and the subsequent slice-count and timelike-count lemmas rest on the same convention. Downstream, the Wick map on squared lengths and the non-degeneracy theorems for Euclideanized simplices inherit a consistent causal class. In the broader Recognition gravity lane this anchors the discrete Lorentzian sector before continuum or continuum-limit claims; it does not yet touch the forcing chain T0–T8 or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.