cmVertexIndexC
plain-language theorem explainer
Maps each of the five 4-simplex vertices (indices 0..4) to the corresponding row/column of the bordered 6×6 Cayley–Menger matrix (indices 1..5), leaving slot 0 for the bordering ones. Anyone writing complex cofactors, split dihedral cosines, or branch-regularity predicates on hinge data cites it. The body is a five-clause pattern match, the complex-first mirror of the real Geometry.DihedralCayleyMenger indexing.
Claim. The map $v \mapsto v+1$ sending each 4-simplex vertex index $v \in \{0,1,2,3,4\}$ to the corresponding Cayley–Menger matrix index in $\{1,2,3,4,5\}$, so that matrix index $0$ remains the bordering row/column of the $6\times 6$ bordered CM matrix.
background
Module C11 formalizes complex-first 4D Wick continuation of Regge hinge data (complex Cayley–Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The continuation path is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian to Euclidean endpoint.
A bordered Cayley–Menger matrix for five vertices is $6\times 6$: one bordering index (conventionally 0) holds the usual $0/1$ border, and the five geometric vertices occupy indices $1..5$. Squared edge lengths fill the off-diagonal geometric block; cofactors of that matrix yield triangle areas-squared and dihedral cosines.
This definition is the complex-lane copy of the real indexing in Geometry.DihedralCayleyMenger. Downstream split-form objects (cofactors, $c\sqrt{C_{pp}},c\sqrt{C_{qq}}$ denominators, dihedral cosines) all route vertex pairs $(p,q)$ through this map before touching the matrix.
proof idea
Pure definition by exhaustive pattern match on Fin 5: each vertex $k$ is sent to $k+1$ as an element of Fin 6. No lemmas, no tactics; definitional equality cmVertexIndexC k = k+1 is immediate by rfl for each concrete $k$.
why it matters
Every hinge-level object in the C11 lane indexes CM rows through this map. BranchRegularOn requires both diagonal cofactors at cmVertexIndexC p and cmVertexIndexC q to lie in the slit plane; dihedralDenomSplitC and dihedralCosSplitC build the split-sqrt cosine the same way; hingeCosPath_eq_moebius unfolds those definitions and uses the concrete values at vertices 2 and 3. The all-hinges module (WickFourOneAllHinges) reuses it for spacelike and timelike boundary continuation theorems.
Without a fixed vertex-to-CM embedding, the split-form cosine and the S3 branch-regularity certificate on the open arc interior cannot even be stated. The map itself is bookkeeping, but it locks the convention that matches the real DihedralCayleyMenger lane and the hour-0 numeric gate. It does not close the open FullTheoryLedger gap on genuine action-level continuation (C12); that remains outside this module's mandate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.