timelike_count_twoTwo
plain-language theorem explainer
In 3D CDT, a type-(2,2) tetrahedron has exactly four timelike edges among its six edges. Discrete-gravity and Lorentzian Regge workers cite this when locking the causal edge-type table before Wick rotation or deficit-angle work. The proof is a one-line decidability check on the Boolean filter over the six edges.
Claim. For a causal tetrahedron of type $(2,2)$ (two vertices on each of two adjacent spatial slices), exactly four of the six edges are timelike: $\#\{e\in\{0,\ldots,5\}: e\text{ is timelike}\}=4$.
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 causal layer is built for $D=3$ CDT (Ambjørn–Jurkiewicz–Loll conventions).
Between adjacent spatial slices one fills spacetime with two tetrahedron classes. Type $(3,1)$ puts three vertices on slice $t$ and one on $t+1$; type $(2,2)$ puts two vertices on each slice. Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ with $\alpha>0$. Edge indices follow the Cayley–Menger convention: edges $0=(0,1),,1=(0,2),,2=(0,3),,3=(1,2),,4=(1,3),,5=(2,3)$. For $(2,2)$, vertices ${0,1}$ lie on slice $t$ and ${2,3}$ on $t+1$.
Timelike means the edge joins the two slices. The local assignment marks edges ${1,2,3,4}$ as the four cross edges of type $(2,2)$, matching the combinatorial count $2$ spacelike $+,4$ timelike stated in the module conventions.
proof idea
The claim is pure finite combinatorics on Fin 6. Filter the universe of six edges by the Boolean predicate that marks type-$(2,2)$ edges as timelike, then ask for the cardinality of that filter. Lean discharges the equality to $4$ by decide: the predicate is a closed Boolean combination of equality tests on edge indices, so the filtered finset is computable and the card check is a decidable proposition. No geometric lemmas are invoked.
why it matters
The count is a load-bearing kinematical fact for the Lorentzian layer: every later statement that assigns squared lengths, runs the Wick map $\alpha\mapsto -\alpha$, or proves Euclideanized non-degeneracy and real deficit angles at $\alpha=1$ needs a certified spacelike/timelike partition. The module doc fixes type $(2,2)$ as "$2$ spacelike $+,4$ timelike"; this theorem is the machine-checked half of that partition (the companion spacelike-count lemma closes the other half).
It sits in the same decide-able edge-type family as the $(3,1)$ counts and the cross-slice characterizations. Downstream Wick-involution and non-degeneracy results in this file rely on that table being correct. In the broader Recognition stack this is geometry scaffolding for discrete gravity, not a forcing-chain (T0–T8) step, but it is the combinatorial gate into Lorentzian simplicial gravity in $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.