pentDistSq
plain-language theorem explainer
Unpacks a 10-component squared-edge tuple into the symmetric 5-by-5 squared-distance table of a 4-simplex on vertices 0..4, using the fixed lexicographic edge order. Anyone wiring Cayley-Menger, causal edge typing, or Wick maps on CDT 4-simplices cites this table. The body is a pure case split on vertex pairs, returning the matching edge component or zero on the diagonal.
Claim. Given a 10-tuple $x$ of real squared edge lengths for a 4-simplex (lexicographic order on pairs among vertices $\{0,1,2,3,4\}$), define the squared-distance table $d^2(i,j)$ by $d^2(i,j)=x_e$ when $\{i,j\}$ is the $e$-th edge in that order, $d^2(i,j)=d^2(j,i)$, and $d^2(i,i)=0$.
background
This module is the 4D Lorentzian (CDT) lift in the QG Seven-Gaps campaign: causal 4-simplex classes of types (4,1) and (3,2), Wick rotation on the ten squared edge lengths, and the bordered Cayley-Menger determinant cm4. Spatial slices are equilateral tetrahedra of squared length $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime.
Squared edge data live in SqEdges10, the type Fin 10 → ℝ, ordered lexicographically as edges $(0,1),(0,2),(0,3),(0,4),(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)$. Geometry consumers (Cayley-Menger, symmetry lemmas, complex Wick action) need the full vertex-pair table rather than the flat 10-vector, so this definition is the canonical unpacking.
The table is the real precursor of the complex edge table used in the Wick-action lane and of the SimplexSquaredDistances 4 package that feeds determinant and non-degeneracy arguments.
proof idea
Definition by exhaustive match on (i.val, j.val). Each unordered edge pair is listed twice (both orientations) and routed to the corresponding component of the Fin 10 tuple; the catch-all branch returns 0, covering the diagonal and any impossible index pair. No lemmas are invoked; the construction is pure pattern matching aligned with the module's lexicographic edge list.
why it matters
This is the bridge from flat edge data to the matrix interface required by 4-simplex geometry. Downstream, pentDistSq_edge proves that reading the table along pentEdgeVertices recovers the original tuple, and pentDistances packages the table into SimplexSquaredDistances 4 (with symmetry and zero-diagonal proofs). The complex-first Wick lane complexifies the same layout as SqEdges10C.
In the Recognition gravity stack this sits in Phase 3a of the Lorentzian sector: causal class combinatorics, Wick involution $\alpha \mapsto -\alpha$, and exact cm4 thresholds for Euclidean non-degeneracy versus Lorentzian negativity. Without a single agreed distance table, those determinant and class-action theorems cannot share edge indexing with the 3D kernel-checked simplex machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.