cmMatrixC
plain-language theorem explainer
Defines the bordered 6×6 complex Cayley–Menger matrix for a 4-simplex given ten complex squared edge lengths. Anyone computing complex hinge areas or dihedral cosines along the Wick arc cites this matrix. The construction is a direct case split on the border index map: 0 at the double-border entry, 1 on the border, and complex squared distances in the bulk.
Claim. Given a 10-tuple $x$ of complex squared edge lengths of a 4-simplex, form the bordered $6\times 6$ Cayley–Menger matrix $M(x)\in M_6(\mathbb{C})$ by $M_{00}=0$, $M_{0j}=M_{i0}=1$ for $i,j\ge 1$, and $M_{ij}=d^2(v_i,v_j)$ (complex) for the five simplex vertices when both indices are bulk.
background
This module carries out the complex-first 4D Wick continuation of Regge hinge data (lane C11): dihedral cosines and areas-squared of triangular hinges of a single causal 4-simplex, continued along the upper-half-plane arc from Lorentzian to Euclidean squared edges. It is hinge-data continuation only; full action-level continuation remains open (C12).
A 4-simplex has five vertices and ten edges. Here the edge data are complexified: SqEdges10C is a map from ten lexicographic edge slots to $\mathbb{C}$. The classical real Cayley–Menger matrix for an $n$-simplex is the bordered $(n+2)\times(n+2)$ array with $0$ in the corner, $1$s on the border, and squared distances in the bulk; its minors encode volumes and (via cofactors) dihedral cosines. The real 3-simplex minor construction cmMinor3 is the template being complexified at $n=4$.
Index map cmIndexVertexC sends the six matrix indices to either the border slot (none) or one of the five vertices (some v). Squared distances between vertices are read from the edge tuple by pentDistSqC.
proof idea
Pure definition by cases on the pair of index images under cmIndexVertexC. Both border: entry $0$. Exactly one border: entry $1$. Both vertices: entry equal to the complex squared distance pentDistSqC x vi vj. No lemmas; the body is the matrix-valued function itself.
why it matters
This is the complex CM matrix that all C11 hinge-data continuations factor through. Downstream, cmMinorC deletes a row and column and takes the $5\times 5$ determinant (complex mirror of cmMinor3), feeding cofactor dihedral cosines and area-squared formulas. Explicit two-value hinge tuples are identified with closed-form matrices via cmMatrixC_hingeEdges and cmMatrixC_hingeEdges32. Symmetry cmMatrixC_symm (and the induced minor symmetry) is proved by finite case analysis on this definition.
In the Recognition gravity stack this sits inside the QG Seven-Gaps Wick arc: path-selected continuation of hinge data with a branch certificate on the open arc interior. It does not close the ledger gap wick_action_continuation_4d; that remains the separate C12 question about an interior-hinge simplicial complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.