cmMatrixN_lorentzian_threeTwo
plain-language theorem explainer
The bordered Cayley-Menger matrix of a Lorentzian type-(3,2) 4-simplex, with spacelike squared lengths a² and timelike squared lengths −α a², equals the explicit two-parameter matrix at p = a², q = −α a². Anyone computing the (3,2) Lorentzian cm4 determinant cites this identification. The proof is pure entrywise definitional equality on the 6×6 indices.
Claim. For all real $a$ and $\alpha$, the bordered Cayley-Menger matrix built from the squared edge lengths of a Lorentzian type-$(3,2)$ causal 4-simplex (spacelike edges $a^2$, timelike edges $-\alpha a^2$) equals the explicit two-parameter $(3,2)$ matrix evaluated at $p = a^2$ and $q = -(\alpha a^2)$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: CDT-style causal 4-simplex classes in D = 4, with Wick rotation as the algebraic continuation α ↦ −α on squared edge lengths. Spatial slices are equilateral tetrahedra of squared edge a². Type (3,2) places three vertices on slice t and two on t+1, giving four spacelike and six timelike edges; Lorentzian timelike squared lengths are −α a² with α > 0.
The bordered Cayley-Menger matrix cmMatrixN is the full (n+2)×(n+2) matrix from squared pairwise distances (here n = 4, so 6×6), grounded in Geometry.CayleyMengerN. The ten edges are ordered lexicographically on vertices 0..4. The two-parameter matrix for type (3,2) packages those entries at parameters p (spacelike) and q (timelike).
Upstream, cmMatrixN is the dimension-parametric construction used for exact cm4 evaluation on both causal classes.
proof idea
Term-level matrix equality by extensionality: extend over indices i, j of the 6×6 bordered matrix, then exhaust both Fin 6 indices by fin_cases. Each of the 36 entries reduces by rfl once the Lorentzian (3,2) edge assignment and the two-parameter matrix definition are unfolded. No algebraic lemmas; pure definitional match of the distance tuple into the Cayley-Menger border pattern.
why it matters
This is the matrix-level bridge from the combinatorial Lorentzian (3,2) edge data to an evaluable closed form. The sole downstream consumer is cm4_lorentzian_threeTwo, which rewrites the 4-simplex Cayley-Menger determinant through this identification and det_pentMatrix32 to obtain the exact formula cm4 = −((12α + 7) a⁸).
That determinant feeds the module's Euclidean non-degeneracy thresholds and the strict cm4 negativity on the Lorentzian side (item 4 of the module program). In the broader Seven-Gaps campaign it anchors the kinematical Wick rotation for type (3,2), parallel to the (4,1) lane, so both CDT 4-simplex classes have exact volume/sign control before dynamical coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.