SqEdges10
plain-language theorem explainer
Squared edge lengths of a 4-simplex are packaged as a 10-tuple of reals, one per edge of the complete graph on five vertices in lexicographic order. Anyone working the CDT (4,1) and (3,2) classes, Wick maps, or Cayley–Menger volume in this module cites this carrier type. It is a pure type abbreviation with no proof content.
Claim. Write $\mathrm{SqEdges}_{10}$ for the type of maps $\{0,\ldots,9\}\to\mathbb{R}$, interpreted as the ten squared edge lengths of a 4-simplex on vertices $\{0,1,2,3,4\}$ in lexicographic edge order $(0,1),(0,2),(0,3),(0,4),(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: the 4D CDT lift of the 3D causal-simplex Wick machinery. Spatial slices are equilateral tetrahedra of squared edge $a^2$; spacetime between slices is filled by (4,1) simplices (6 spacelike + 4 timelike edges) and (3,2) simplices (4 spacelike + 6 timelike). Timelike squared lengths are $-\alpha a^2$ Lorentzian and $+\alpha a^2$ after Wick rotation.
A 4-simplex has $\binom{5}{2}=10$ edges. The module fixes the lexicographic indexing on vertex pairs so every later construction (timelike predicate, Lorentzian/Euclidean edge tuples, Cayley–Menger input) shares one coordinate system. The type is simply real-valued functions on that finite index set.
Upstream geometry supplies the dimension-parametric Cayley–Menger determinant cmDetN; this carrier is the 4D edge-length input that feeds the bordered $6\times 6$ evaluation used for volume and non-degeneracy.
proof idea
No proof: a one-line type abbreviation equating the name to Fin 10 → ℝ. The adjacent comment records the edge-to-vertex-pair dictionary used everywhere downstream; that dictionary is not part of the type itself.
why it matters
Every causal-class and volume construction in the module is typed over this carrier. Downstream, Lorentzian and Euclidean squared-edge maps produce values of this type; the Lorentzian class is a set of such tuples; pentDistances packages one into SimplexSquaredDistances 4; cm4 evaluates the sign-normalized Cayley–Menger determinant on it (cm4 = 9216 V^2 on non-degenerate Euclidean 4-simplices); and NonDegeneratePent requires positive edges and positive cm4.
In the Recognition gravity lane this is the kinematical substrate for the 4D Wick involution and the exact Euclidean non-degeneracy thresholds in $\alpha$ for both CDT types. It sits under the D=3 spatial forcing (T8) once the lattice is built, but the declaration itself is pure indexing infrastructure for the CDT 4-simplex campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.