spacelike_count_threeTwo
plain-language theorem explainer
A type-(3,2) causal 4-simplex has exactly four spacelike edges among its ten edges. CDT edge-type bookkeeping and the 4D Wick-rotation lane cite this count. The proof is a pure finite decision over Fin 10.
Claim. For the causal 4-simplex class with three vertices on the lower spatial slice and two on the upper slice, exactly four of the ten edges fail the timelike predicate (equivalently: the spacelike edge count is $4$).
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a). Between adjacent spatial slices one fills spacetime with two CDT 4-simplex classes: type (4,1) (four vertices on slice $t$, one on $t+1$) and type (3,2) (three on $t$, two on $t+1$). Vertices are $0..4$; the ten edges are the lexicographic pairs, indexed by $\mathrm{Fin},10$.
Spacelike edges live inside a single slice and carry squared length $a^2$; timelike edges cross slices and carry $-\alpha a^2$ in the Lorentzian regime. For type (3,2) the module conventions fix the split as $3+1=4$ spacelike and $6$ timelike. The predicate isTimelike marks cross-slice edges for a given CausalPentType; spacelike edges are exactly those for which it returns false.
Sibling counts (slice_count_threeTwo, timelike_count_threeTwo, and the (4,1) analogues) pin the same combinatorial assignment before any metric or Cayley-Menger analysis begins.
proof idea
One-line finite decision: filter the universe of ten edges by the Boolean isTimelike threeTwo e = false, then ask Lean to compute the cardinality. Everything in sight (Fin 10, Boolean equality, Finset card) is decidable, so decide closes the goal with no lemmas and no arithmetic.
why it matters
The count is the combinatorial half of the type-(3,2) edge multiset used throughout the module: Lorentzian squared-edge tuples, the Wick map $\alpha\mapsto -\alpha$ on those tuples, and the exact evaluation of the bordered Cayley-Menger determinant cm4 on both causal classes. Module doc states the target split explicitly (4 spacelike + 6 timelike for (3,2)); this theorem is the machine-checked witness for the spacelike side.
It sits in the Lorentzian-sector lane that lifts the already kernel-checked 3D causal-simplex machinery. Downstream the same edge typing feeds Euclidean non-degeneracy thresholds in $\alpha$ and the strict cm4 negativity on the Lorentzian side. No parent theorem currently lists it in used_by, but every later construction that builds the (3,2) length tuple depends on this split being correct. Framework landmark: $D=3$ spatial slices (T8) with the 4D CDT fill between them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.