triCMMatrixC
plain-language theorem explainer
Defines the bordered 4×4 complex Cayley–Menger matrix for a triangle with squared edge lengths u, v, w. Gravity and Regge analysts cite it as the complex input to triangle area-squared along the Wick arc. The body is a pure case-match on matrix indices: border of ones, zero diagonal blocks, and the three edge squares off-diagonal.
Claim. For complex squared edge lengths $u,v,w\in\mathbb{C}$, the bordered $4\times 4$ Cayley–Menger matrix of the triangle is the symmetric matrix with first row/column $(0,1,1,1)$, zero diagonal on the remaining $3\times 3$ block, and off-diagonal entries $u$, $v$, $w$ in positions corresponding to the three edges.
background
Module C11 complexifies hinge data (areas-squared and dihedral cosines) of causal 4-simplex classes along a path-selected Wick arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian to Euclidean endpoints. Only hinge-level continuation is claimed; full action-level continuation remains open (C12).
The classical Cayley–Menger formula for squared $n$-volume is $V_n^2=(-1)^{n+1}\det(\mathrm{CM})/(2^n(n!)^2)$. For a triangle ($n=2$) this reduces to $-\det(\mathrm{CM}_{4\times4})/16$. The present definition supplies the complex $4\times4$ CM matrix whose determinant feeds that formula.
Squared lengths $u=d(1,2)^2$, $v=d(1,3)^2$, $w=d(2,3)^2$ are allowed to be complex so that timelike edges can travel the upper-half-plane arc while spacelike edges stay real.
proof idea
Pure definition by pattern match on Fin 4 indices: entry $(0,0)$ is $0$; the rest of the border row and column is $1$; the geometric diagonal is $0$; positions $(1,2)$ and $(2,1)$ hold $u$, $(1,3)$ and $(3,1)$ hold $v$, $(2,3)$ and $(3,2)$ hold $w$; all other entries are $0$. No lemmas are invoked.
why it matters
This matrix is the sole geometric input to triangleAreaSqC, the complex area-squared $-\det(\mathrm{CM})/16$. Downstream closed forms include the regular unit triangle equaling $3/16$, and the timelike hinge shapes triangleAreaSqC 1 z z = z/4 - 1/16 and triangleAreaSqC z z 1 = z/4 - 1/16, which feed hingeAreaSqC_closed on hinge $(0,1,4)$.
Those identities are the algebraic backbone of the C11 Wick continuation of Regge hinge areas along the four-one causal simplex classes. They do not close the ledger gap wick_action_continuation_4d; that remains an open C12 question about interior-hinge complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.