timelike_count_threeOne
plain-language theorem explainer
A type-(3,1) causal tetrahedron has exactly three timelike edges among its six edges. Anyone building the Lorentzian CDT layer (Wick map, edge-length assignments, deficit angles) cites this count. The proof is a one-line finite decision on the Boolean edge filter.
Claim. For a causal tetrahedron of type $(3,1)$ (three vertices on spatial slice $t$, one apex on slice $t+1$), the number of timelike edges among the six edges is exactly $3$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign. Prior discrete-gravity work in the monolith is Euclidean; here the first certified CDT-style layer in $D=3$ is built: causal tetrahedron classes, a Wick map on squared edge lengths, and non-degeneracy of the Euclideanized simplices.
Spatial slices are equilateral triangulations with squared length $a^2$. Between slices $t$ and $t+1$ one fills with two tetrahedron types. Type $(3,1)$ places vertices ${0,1,2}$ on slice $t$ and vertex $3$ on $t+1$; type $(2,2)$ splits two-and-two. Edge indexing follows the Cayley–Menger convention: edges $0=(0,1),,1=(0,2),,2=(0,3),,3=(1,2),,4=(1,3),,5=(2,3)$.
An edge is timelike precisely when it joins the two slices. For type $(3,1)$ that means the three edges incident to the apex, coded as indices ${2,4,5}$. Spacelike edges keep squared length $a^2$; timelike edges carry $-\alpha a^2$ ($\alpha>0$) in the Lorentzian regime.
proof idea
The statement is a pure finite-cardinality claim on Fin 6. Filter the universe by the Boolean predicate that marks type-$(3,1)$ edges as timelike (true on indices $2,4,5$), then ask for the card. Lean discharges the equality to $3$ by decide: the predicate is decidable, the set is finite, and no arithmetic or geometry is required.
why it matters
The count is the combinatorial half of the CDT convention that a $(3,1)$ tetrahedron carries three spacelike and three timelike edges (the time-reflected $(1,3)$ shares the same multiset). It anchors the Lorentzian edge-length assignment and the Wick involution $\alpha\mapsto -\alpha$ developed in the same module, and it pairs with the sibling spacelike-count lemma. In the broader Recognition gravity lane this is kinematical scaffolding for deficit-angle reality at the physical point $\alpha=1$ and for any later Regge action in Lorentzian signature. No downstream theorem currently depends on it in the graph, so it is a leaf certificate rather than a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.