cmIndexVertexC
plain-language theorem explainer
Index map from the six rows of a bordered Cayley–Menger matrix to the five simplex vertices: row 0 is the border (returns none), and row k+1 is vertex k. Anyone assembling the complex 6×6 CM matrix for 4-simplex hinge data cites this. The body is a one-line Fin-case split with an omega bounds check.
Claim. For $i \in \{0,1,\ldots,5\}$, send the border index $i=0$ to $\mathsf{none}$ and each vertex index $i=k+1$ ($k\in\{0,\ldots,4\}$) to $\mathsf{some}(k)$. This is the complexified index map for the bordered $6\times 6$ Cayley–Menger matrix of a 4-simplex ($n=4$).
background
The module formalizes complex-first 4D Wick continuation of Regge hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) for causal 4-simplices. Scope is hinge-data continuation only; full action-level continuation remains open (C12).
A Cayley–Menger matrix for an $n$-simplex is the bordered $(n+2)\times(n+2)$ matrix of squared edge lengths: the first row and column are the border (zeros on the diagonal entry, ones off-diagonal), and the remaining block holds squared distances among the $n+1$ vertices. Upstream, cmMatrixN builds that matrix over $\mathbb{R}$ by matching on an index-to-vertex map of the same shape.
Here $n=4$, so the matrix is $6\times 6$ and vertices are indexed by $\mathrm{Fin},5$. The complex edge tuple lives in $\mathbb{C}^{10}$; this definition only supplies the combinatorial indexing used when filling matrix entries over $\mathbb{C}$.
proof idea
Definition by cases on the underlying natural number of $i:\mathrm{Fin},6$. If $i.val=0$, return $\mathsf{none}$ (border). Otherwise return $\mathsf{some}\langle i.val-1,_\rangle$, with the $\mathrm{Fin},5$ bound discharged by omega. No lemmas; pure index arithmetic mirroring the real cmIndexVertex at $n=4$.
why it matters
Feeds directly into the complex bordered matrix cmMatrixC, which matches on this map for every entry: border–border is $0$, border–vertex is $1$, and vertex–vertex is the corresponding complex squared edge. That matrix is the starting point for complex CM minors, cofactors, and dihedral cosines along the Wick arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian to Euclidean endpoints.
In the Seven-Gaps C11 lane this is scaffolding for hinge-data continuation, not a physics claim by itself. It closes the complexification of the real geometry layer so later branch certificates and split-sqrt denominators can be stated over $\mathbb{C}$. The ledger gap on full action-level 4D continuation stays open and is untouched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.