pentDistSq_edge
plain-language theorem explainer
For any 10-tuple of squared edge lengths on a 4-simplex, reading the squared-distance table at the two endpoints of lexicographic edge e recovers the e-th entry of the tuple. Anyone wiring Cayley–Menger data from edge arrays cites this agreement lemma. The proof is a ten-way case split with definitional equality.
Claim. Let $x:\{0,\ldots,9\}\to\mathbb{R}$ be a squared-edge-length assignment on the 4-simplex (lexicographic edge order). For every edge index $e$, if $(i,j)$ is the ordered vertex pair of edge $e$, then the squared-distance table built from $x$ satisfies $d^2(i,j)=x(e)$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: causal (CDT-style) 4-simplex classes in $D=4$, with spacelike squared length $a^2$ and timelike squared length $-\alpha a^2$, plus the Wick map $\alpha\mapsto -\alpha$ and the bordered Cayley–Menger determinant cm4.
Squared edge data live as SqEdges10 ($\mathrm{Fin},10\to\mathbb{R}$) in lexicographic order on pairs among vertices ${0,1,2,3,4}$: $(0,1),(0,2),\ldots,(3,4)$. The map pentEdgeVertices sends each edge index to that ordered pair. The table pentDistSq x is the symmetric $5\times5$ squared-distance function assembled by matching on vertex indices against those ten slots (diagonal zero, off-diagonal from $x$).
Upstream, SimplexSquaredDistances 4 packages any such table with symmetry and zero diagonal for the dimension-parametric Cayley–Menger machinery. This lemma is the bridge that says the table construction is faithful on the edge set.
proof idea
Purely definitional. Case-split on the ten values of $e:\mathrm{Fin},10$ via fin_cases; each goal is rfl against the corresponding clause of pentDistSq and the matching constructor of pentEdgeVertices. No arithmetic or external lemmas.
why it matters
Without edge-table agreement, every later identity that feeds a 10-tuple into cm4 or into the Euclidean/Lorentzian non-degeneracy thresholds would have an indexing gap. The module aims at exact cm4 evaluations on the $(4,1)$ and $(3,2)$ classes and at the $\alpha$-thresholds for Euclidean positivity versus Lorentzian negativity; those calculations presuppose that the squared lengths placed on edges are exactly the ones the determinant reads.
No downstream users are recorded yet in the graph, so this is infrastructure for the causal-simplex and Wick-rotation development rather than a cited parent theorem. It sits in the gravity/CDT lane (Ambjørn–Jurkiewicz–Loll conventions), not in the T0–T8 forcing chain, but it is the bookkeeping step that makes 4D Cayley–Menger evaluations honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.