spacelike_count_fourOne
plain-language theorem explainer
In 4D CDT, a causal 4-simplex of type (4,1) has exactly six spacelike edges among its ten edges. Anyone checking the Lorentzian edge census, Wick map, or Cayley–Menger thresholds for the (4,1)/(1,4) class would cite this. The proof is a pure `decide` on the Boolean edge-type table for that class.
Claim. Among the ten edges of a causal 4-simplex of type $(4,1)$ (four vertices on slice $t$, one on slice $t+1$), the number of spacelike edges is exactly six: $\#\{e\in\{0,\ldots,9\}: e\text{ is not timelike for type }(4,1)\}=6$.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a): CDT-style causal 4-simplex classes between adjacent spatial slices, plus an explicit Wick map on the ten squared edge lengths. Spatial slices are equilateral 3-tetrahedra of squared length $a^2$; spacetime is filled by type $(4,1)$ (four vertices on $t$, one on $t+1$) and type $(3,2)$ (three on $t$, two on $t+1$), with time reflections sharing the same edge-length multisets.
Edges are indexed lexicographically as Fin 10. Spacelike edges carry $a^2$; timelike edges carry $-\alpha a^2$ ($\alpha>0$) in the Lorentzian regime. The predicate isTimelike marks cross-slice edges: for type $(4,1)$ the four edges touching the apex (indices $3,6,8,9$). Spacelike means the complement of that Boolean table. The 3D Wick module supplies the analogous tet-edge convention; this 4D file is import-independent but mirrors those conventions.
proof idea
One-line decidability proof. The edge set is finite (Fin 10), and isTimelike on CausalPentType.fourOne is a closed Boolean combination of equality tests on edge indices. Filtering the universe by isTimelike _ e = false and taking cardinality is therefore a decidable proposition; decide evaluates it to $6$ (equivalently $10-4$, matching the four apex-touching timelike edges).
why it matters
Fixes the combinatorial edge census for the $(4,1)$ class that the module doc states up front: six spacelike plus four timelike. That census is the kinematical input for the Wick involution ($\alpha\mapsto -\alpha$ on timelike squared lengths), for evaluating the bordered Cayley–Menger determinant cm4 on both causal classes, and for the exact Euclidean non-degeneracy thresholds in $\alpha$. It sits in the Lorentzian-sector lane of the Seven-Gaps gravity campaign and parallels the already-checked 3D causal-simplex edge counts. No downstream Lean users are wired yet; the lemma is infrastructure for those cm4 and Wick theorems in the same module. Landmark contact is T8 ($D=3$ spatial slices) lifted one dimension to 4D CDT simplices, not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.