det_pentMatrix41
plain-language theorem explainer
The bordered 6×6 Cayley–Menger matrix for a CDT (4,1) 4-simplex with spacelike squared length p and timelike squared length q has determinant p³(3p−8q). Gravity and CDT workers cite it to evaluate Euclidean and Lorentzian cm4 volumes exactly. The proof unfolds the matrix and expands the determinant by the first row, then finishes by ring.
Claim. For all real $p,q$, the determinant of the bordered Cayley–Menger matrix of a type-$(4,1)$ causal 4-simplex with spacelike squared edge length $p$ and timelike squared edge length $q$ equals $p^3(3p-8q)$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: CDT-style 4-simplex classes in $D=4$, with spacelike edges of squared length $a^2$ and timelike edges of squared length $-\alpha a^2$ ($\alpha>0$). Type $(4,1)$ places four vertices on one spatial slice and one apex on the next (six spacelike, four timelike edges); type $(3,2)$ is the complementary class.
The 4-simplex volume criterion is the Cayley–Menger determinant cm4, realized as the bordered $6\times 6$ matrix from Geometry.CayleyMengerN.cmDetN. The matrix pentMatrix41 p q is that border for a pure $(4,1)$ length assignment: border row/column of ones, diagonal zeros on the five vertices, off-diagonal entries $-p$ on spacelike pairs and $-q$ on timelike pairs (apex at index 4).
Wick rotation acts as $\alpha\mapsto -\alpha$ on the causal class. Exact closed forms for $\det$ on both Euclideanized and Lorentzian length assignments are the algebraic input to non-degeneracy thresholds and Lorentzian negativity.
proof idea
Unfold pentMatrix41 to the explicit $6\times 6$ entry function. Expand the determinant along the border via Matrix.det_succ_row_zero, with Fin.sum_univ_succ and Fin.succAbove handling the $5\times 5$ cofactor sums. Bare simp is intentional: an explicit simp only list timed out, while the default numeric simprocs keep the $6\times 6$ expansion tractable (heartbeats and recursion depth raised). The resulting polynomial identity is closed by ring, yielding $p^3(3p-8q)$.
why it matters
This is the kernel-honest symbolic determinant for the $(4,1)$ class. Downstream, cm4_euclidean_fourOne rewrites through it to obtain $\mathrm{cm4}=(8\alpha-3)a^8$, matching the AJL volume $V(4,1)=(a^4/96)\sqrt{8\alpha-3}$ via $9216 V^2$. Likewise cm4_lorentzian_fourOne gives $\mathrm{cm4}=-((8\alpha+3)a^8)$, the strict negativity used for Lorentzian non-embedding. The sibling det_pentMatrix32 uses the same expansion pattern for type $(3,2)$; WickActionComplexFirst.det_minorPPC cites this proof style for a complex $5\times 5$ minor. Status flags record that cm4 thresholds and Lorentzian negativity are certified, while action-level continuation remains open. In the RS gravity lane this pins the 4D causal simplex kinematics behind the Wick map, parallel to the 3D CausalSimplexWick machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.