spacelike_count_threeOne
plain-language theorem explainer
A (3,1) causal tetrahedron has exactly three spacelike edges among its six edges. Discrete-gravity and 3D CDT workers cite this when fixing the Lorentzian edge-type inventory before Wick rotation or deficit-angle work. The proof is a one-line decidability check on the Boolean filter over Fin 6.
Claim. For the causal tetrahedron type with three vertices on slice $t$ and one vertex on slice $t+1$, the number of edges $e \in \{0,\ldots,5\}$ that are not timelike equals $3$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in $D=3$ CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are equilateral triangulations; spacetime between adjacent slices is filled by two tetrahedron classes: type (3,1) (three vertices on slice $t$, one on $t+1$) and type (2,2) (two on each slice).
Edge indexing follows the Cayley–Menger convention: vertices $0,1,2,3$ and edges $0=(0,1),,1=(0,2),,2=(0,3),,3=(1,2),,4=(1,3),,5=(2,3)$. For type (3,1), vertices ${0,1,2}$ lie on slice $t$ and vertex $3$ on $t+1$. An edge is timelike precisely when it joins the two slices; the local predicate marks edges ${2,4,5}$ as timelike (those incident to the apex). Spacelike edges are the complement.
The module doc states the classical inventory: type (3,1) carries 3 spacelike + 3 timelike edges. This theorem certifies the spacelike half of that count combinatorially.
proof idea
One-line decide proof. The universe Finset.univ on Fin 6 is finite, and isTimelike CausalTetType.threeOne is a closed Boolean expression on edge indices. Filtering those edges with value false and asking for cardinality $3$ is a decidable propositional statement; the kernel discharges it by exhaustive evaluation. No algebraic lemmas are invoked.
why it matters
Certified edge-type counts are the combinatorial substrate of the Lorentzian layer: they justify the squared-length assignment (spacelike $a^2$, timelike $-\alpha a^2$) and the subsequent Wick map $\alpha \mapsto -\alpha$ on the causal class. The sibling timelike_count_threeOne supplies the matching count of 3; together they pin the (3,1) multiset before non-degeneracy and deficit-angle reality at $\alpha=1$.
No downstream theorems currently depend on this declaration in the graph, so it functions as a leaf certificate inside the CausalSimplexWick inventory rather than a stepping stone to a named parent. It closes the combinatorial half of the module's first bullet (CDT tetrahedron classes with decide-able edge typing) and aligns with the forcing-chain landmark $D=3$ spatial dimensions by fixing the 3D CDT building blocks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.