pentDistSqC
plain-language theorem explainer
Builds the symmetric 5×5 complex squared-distance table of a 4-simplex from a packed Fin-10 edge tuple. Anyone assembling complex Cayley–Menger matrices or triangular hinge areas in the C11 Wick lane cites it. The body is a pure case table: each unordered vertex pair maps to one edge slot, diagonal entries are zero.
Claim. Given a 10-tuple $x$ of complex squared edge lengths of a 4-simplex (lexicographic order on pairs among five vertices), define the symmetric table $d^2 : \{0,\ldots,4\}^2 \to \mathbb{C}$ by sending each unordered pair $\{i,j\}$ to the corresponding component of $x$, and $d^2(i,i)=0$.
background
Module C11 formalizes a complex-first 4D Wick continuation of Regge hinge data (areas-squared and dihedral cosines) for causal 4-simplices. Honest scope: hinge-data only; full action-level continuation remains the open C12 / ledger gap.
A 4-simplex has five vertices and $\binom{5}{2}=10$ edges. SqEdges10C is the type of maps $\mathrm{Fin},10\to\mathbb{C}$ packing those squared lengths in the same lexicographic order as the real CausalSimplex4D edge list. This definition is the complex mirror of the real squared-distance table: it unpacks the 10-tuple into a full $5\times 5$ matrix of $d^2(i,j)$.
Upstream, the Cayley–Menger index map treats matrix index 0 as the border row/column and index $k+1$ as vertex $k$. Downstream matrix and area constructions read distances only through this table.
proof idea
Definition by exhaustive match on the pair of vertex values. The ten off-diagonal unordered pairs are wired, symmetrically, to slots $x_0,\ldots,x_9$ in lex order; every remaining case (the diagonal, and any unmatched pattern) returns $0$. No lemmas, no arithmetic: pure structural unpacking of the edge packing.
why it matters
Local plumbing for the entire complex Cayley–Menger stack in this module. cmMatrixC fills the bordered $6\times 6$ complex CM matrix from these distances; hingeAreaSqC feeds three table lookups into the complex triangle area-squared; the closed-form theorem hingeAreaSqC_closed unfolds those lookups on the model hinge edges. The path-selected Wick realization theorem sits on the same hinge-data spine.
In the Seven-Gaps campaign this is panel-locked lane C11: upper-half-plane arc on the timelike squared edge, split-sqrt denominator mandatory. It does not close the ledger gap wick_action_continuation_4d; it only supplies the distance table the hinge continuation needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.