spacelike_count_twoTwo
plain-language theorem explainer
For a 3d CDT tetrahedron of type (2,2), exactly two of the six edges are spacelike. Anyone building Lorentzian edge-length assignments or Wick maps on causal simplices cites this count. The proof is a single decidability check on the finite filter over the six edges.
Claim. For the causal tetrahedron of type $(2,2)$ (two vertices on each adjacent spatial slice), the number of edges among the six that fail the timelike predicate equals $2$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in $D=3$. Prior discrete-gravity results in the stack are Euclidean; here the first certified Lorentzian layer is the CDT-style causal tetrahedron classification of Ambjorn–Jurkiewicz–Loll.
Between adjacent spatial slices, spacetime is filled by two tetrahedron types. Type $(3,1)$ has three vertices on slice $t$ and one on $t+1$ (three spacelike and three timelike edges). Type $(2,2)$ has two vertices on each slice and, by the module conventions, two spacelike and four timelike edges. Vertices are indexed $0,1,2,3$ and edges $0=(0,1),\ldots,5=(2,3)$ as in the Cayley–Menger edge ordering. For $(2,2)$, vertices ${0,1}$ lie on slice $t$ and ${2,3}$ on $t+1$; an edge is spacelike precisely when both endpoints share a slice.
Spacelike edges later carry squared length $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime. The present lemma is purely combinatorial: it only counts which of the six edges are non-timelike for type $(2,2)$.
proof idea
One-line decidability proof. The ambient type is Fin 6, the predicate isTimelike for CausalTetType.twoTwo is a Boolean function on a finite domain, and Lean closes the cardinality claim by decide (exhaustive evaluation of the filtered universe). No algebraic lemmas are invoked.
why it matters
The count is the combinatorial half of the CDT edge-type assignment for type $(2,2)$: two spacelike, four timelike. Together with the matching $(3,1)$ counts and the slice-membership lemmas, it licenses the Lorentzian squared-edge tuple (spacelike $a^2$, timelike $-\alpha a^2$) and the subsequent Wick map $\alpha\mapsto -\alpha$ on the causal class.
That map is the first certified Lorentzian layer in the Seven-Gaps gravity lane; non-degeneracy of the Euclideanized simplices and the deficit-angle reality corollary at $\alpha=1$ sit downstream of the same edge-type bookkeeping. In the broader Recognition stack this is geometry scaffolding for discrete gravity in the forced $D=3$ setting (forcing step T8), not a mass or coupling derivation. No used_by edges are recorded yet; the lemma is infrastructure for the Wick and non-degeneracy block in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.