det_pentMatrix32
plain-language theorem explainer
The bordered 6×6 Cayley–Menger matrix for a CDT (3,2) 4-simplex, written in two squared-length parameters p and q, has determinant p³(7p−12q). Anyone certifying Euclidean or Lorentzian 4-simplex volumes in the Seven-Gaps gravity lane cites this identity. The proof unfolds the matrix, expands the determinant by the first row, and finishes by ring.
Claim. For all real $p,q$, the determinant of the two-parameter bordered Cayley–Menger matrix attached to the causal $(3,2)$ 4-simplex equals $p^3(7p-12q)$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: CDT-style 4-simplices in $D=4$, with spacelike edges of squared length $a^2$ and timelike edges of squared length $\pm\alpha a^2$. Type $(3,2)$ places three vertices on slice $t$ and two on $t+1$ (four spacelike and six timelike edges). The Wick map is the algebraic continuation $\alpha\mapsto -\alpha$ on those squared lengths.
Volumes are read from the dimension-parametric bordered Cayley–Menger determinant cmDetN (a $6\times 6$ matrix on five vertices). The two-parameter matrix pentMatrix32 p q is the symbolic form of that border for the $(3,2)$ edge multiset, with $p$ the common spacelike squared length and $q$ the cross-slice parameter. The sibling identity for type $(4,1)$ already gives $\det=p^3(3p-8q)$; this theorem is the matching expansion for $(3,2)$.
proof idea
Unfold the definition of the $(3,2)$ two-parameter matrix. Expand the $6\times 6$ determinant along the first (border) row via Matrix.det_succ_row_zero, with the finite sums written out by Fin.sum_univ_succ and Fin.succAbove. The resulting multivariate polynomial identity is discharged by ring. Same deliberate bare-simp style as the $(4,1)$ companion det_pentMatrix41 (an explicit simp only list timed out in whnf).
why it matters
Exact CM determinants are the gate to non-degeneracy thresholds and Lorentzian sign control for both causal classes. Downstream, cm4_euclidean_threeTwo rewrites through this identity to obtain $\mathrm{cm}_4=(12\alpha-7)a^8$, matching the AJL volume formula $V(3,2)=(a^4/96)\sqrt{12\alpha-7}$ via $9216 V^2=(12\alpha-7)a^8$. The Lorentzian twin cm4_lorentzian_threeTwo yields $\mathrm{cm}_4=-((12\alpha+7)a^8)$, so the Euclidean side is positive precisely above the threshold $\alpha>7/12$ while the Lorentzian side stays strictly negative. Those facts feed the module status flags (classes defined, thresholds certified, Lorentzian negativity proved). Action-level continuation remains open; this lemma is pure kinematics on the bordered matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.