timelike_count_threeTwo
plain-language theorem explainer
In 4D CDT, a type-(3,2) 4-simplex has exactly six timelike edges among its ten edges. Anyone fixing the combinatorial edge census of Lorentzian building blocks, or wiring squared-length data for Wick rotation and Cayley-Menger checks, cites this count. The proof is a pure finite decision over Fin 10 against the fixed timelike mask for type (3,2).
Claim. For a causal 4-simplex of type $(3,2)$ (three vertices on spatial slice $t$, two on slice $t+1$), exactly six of the ten edges are timelike: $\#\{e\in\{0,\ldots,9\}: e\text{ is timelike}\}=6$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4D CDT lift of the 3D causal-simplex machinery. Between adjacent spatial slices one fills spacetime with two 4-simplex classes. Type $(4,1)$ puts four vertices on slice $t$ and one on $t+1$; type $(3,2)$ puts three on $t$ and two on $t+1$. Edges within a slice are spacelike (squared length $a^2$); edges that cross slices are timelike (squared length $-\alpha a^2$ in the Lorentzian regime).
The ten edges of the 4-simplex are indexed lexicographically by Fin 10. The predicate isTimelike marks an edge as timelike precisely when it joins the two slices. For type $(3,2)$ the mask is the six cross edges with indices ${2,3,5,6,7,8}$, matching the module convention that $(3,2)$ has $3+1=4$ spacelike and $6$ timelike edges (and likewise for the time reflection $(2,3)$).
The sibling count for type $(4,1)$ and the matching spacelike counts sit beside this lemma; together they lock the combinatorial input to the Wick map and to the exact Cayley-Menger evaluations cm4 on both classes.
proof idea
One-line proof by decide. The universe Finset.univ on Fin 10 is finite, isTimelike CausalPentType.threeTwo is a closed Boolean combination of equality tests on edge indices, and Lean’s decidable instance enumerates the six true cases and checks that the filtered cardinality equals 6. No algebraic lemmas are invoked.
why it matters
The lemma is a kinematical census step in the 4D causal-simplex stack: it certifies that type $(3,2)$ really carries six timelike edges, as required by the Ambjørn–Jurkiewicz–Loll conventions stated in the module header. That fixed count feeds the squared-length assignment (spacelike $a^2$, timelike $-\alpha a^2$), the Wick involution $\alpha\mapsto -\alpha$, and the exact cm4 positivity/negativity thresholds on both causal classes.
It sits in the same decide-able edge-type layer as the $(4,1)$ timelike and spacelike counts and the cross-slice characterizations. Downstream the module uses these counts only implicitly (no named used_by edges yet), but any proof that the Lorentzian side has strictly negative Cayley-Menger determinant, or that Euclidean non-degeneracy holds above a sharp $\alpha$ threshold, rests on this combinatorial partition being correct. Framework-wise it is pure 4D CDT kinematics inside the Seven-Gaps gravity lane, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.