pentDistances
plain-language theorem explainer
Packages a ten-component squared-edge-length tuple into the squared-distance structure of a 4-simplex on five vertices, with symmetry and vanishing diagonal. Anyone evaluating 4D Cayley-Menger volumes or bordered CM matrices in the causal-simplex lane routes through this adapter. Structure obligations are discharged by exhaustive case analysis on vertex indices.
Claim. Given a map $x$ from the ten lexicographic edges of a 4-simplex (vertices $0..4$) to $\mathbb{R}$, produce squared distances $d^2:\mathrm{Fin}\,5\times\mathrm{Fin}\,5\to\mathbb{R}$ with $d^2(i,j)=d^2(j,i)$ and $d^2(i,i)=0$ for all $i,j$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: causal (CDT) 4-simplex classes in $D=4$, with types $(4,1)$ and $(3,2)$ fixed by slice occupancy, and a kinematical Wick rotation acting as $\alpha\mapsto -\alpha$ on squared timelike lengths. Spacelike edges carry $a^2$; timelike edges carry $\pm\alpha a^2$ according to signature.
Edge data are ten real squared lengths in lexicographic order on pairs among five vertices. The geometry layer expects a squared-distance package for an $n$-simplex: a map on $\mathrm{Fin}(n+1)\times\mathrm{Fin}(n+1)$ that is symmetric and zero on the diagonal. The dimension-parametric Cayley-Menger determinant consumes exactly that package.
Here $n=4$, so five vertices and a bordered $6\times 6$ CM matrix. The adapter is the typed bridge from the CDT ten-edge parameterization to that matrix.
proof idea
Definitional construction, not a deep lemma. The squared-distance field is the sibling expansion of the ten-edge tuple onto vertex pairs. Symmetry is proved by nested finite case splits on both $\mathrm{Fin},5$ indices, each subgoal closing by reflexivity against the edge table. Diagonal vanishing is the same pattern on a single index. No algebraic identities beyond the table lookup are used.
why it matters
The sign-normalized 4-simplex Cayley-Menger determinant is defined by feeding this package into the dimension-parametric determinant and flipping sign, so that the value is positive on non-degenerate Euclidean 4-simplices and equals $9216,V^2$. The matching theorem states that the repo's formal squared 4-volume is exactly that determinant divided by $9216=2^4(4!)^2$.
All four bordered-matrix identification theorems (Euclidean and Lorentzian, for both $(4,1)$ and $(3,2)$) apply the package to the corresponding edge tuples and match the two-parameter model matrices at $(a^2,\pm\alpha a^2)$. Those identities underwrite the exact Euclidean non-degeneracy thresholds in $\alpha$ and the strict CM negativity on the Lorentzian side. Without the adapter, Phase 3a volume and Wick-rotation kinematics have no typed input to the geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.