pentMatrix32
plain-language theorem explainer
Bordered 6×6 Cayley–Menger matrix for a causal (3,2) 4-simplex, with free squared lengths p (spacelike) and q (timelike). CDT and discrete-gravity workers cite it when specializing the 4-simplex CM determinant to the (3,2) edge pattern under Euclidean or Lorentzian assignments. The body is an explicit index case-split encoding lower-slice, upper-slice, and cross-slice blocks.
Claim. For $p,q\in\mathbb{R}$, let $M(p,q)$ be the bordered $6\times 6$ real matrix with $M_{00}=0$, first row/column otherwise equal to $1$, zero diagonal on the five geometric indices, value $p$ on the three lower-slice pairs and the single upper-slice pair, and value $q$ on all six cross-slice positions (indices $1,2,3$ = lower vertices; $4,5$ = upper vertices).
background
In the QG Seven-Gaps Lorentzian-sector lane (Phase 3a), spacetime between successive 3D spatial slices is filled by CDT-style 4-simplices of two combinatorial types. Type (3,2) places three vertices on the lower slice and two on the upper: four spacelike edges (the lower triangle plus the upper edge) and six timelike cross edges. Spacelike squared lengths are written $p$; timelike squared lengths are written $q$ (later specialized to $a^2$ and $\pm\alpha a^2$).
The 4-simplex volume (and non-degeneracy) is controlled by the Cayley–Menger determinant, realized as $\det$ of a bordered $6\times 6$ matrix of squared distances. This definition freezes that matrix to the two-value (3,2) pattern so later theorems can evaluate the determinant symbolically and match Euclidean or Lorentzian edge tuples onto it.
proof idea
Definition only: a function on $\mathrm{Fin},6\times\mathrm{Fin},6$ by matching on the underlying natural indices. Index $0$ is the CM border ($0$ on the diagonal, $1$ off-diagonal). Geometric diagonal entries are $0$. The three lower-slice pairs $(1,2),(1,3),(2,3)$ and the upper pair $(4,5)$ receive $p$; every other off-diagonal geometric entry receives $q$. No lemmas or tactics are used.
why it matters
Parent results identify the Euclidean and Lorentzian (3,2) CM matrices with this form at $(p,q)=(a^2,\alpha a^2)$ and $(a^2,-\alpha a^2)$, and compute $\det M(p,q)=p^3(7p-12q)$. Those feed the exact cm4 non-degeneracy thresholds and the sign of the Lorentzian determinant for the (3,2) class, which close the kinematical Wick-rotation story ($\alpha\mapsto -\alpha$) in 4D. The same matrix pattern is reused when matching physical-point continuation edges in the three-two hinge analysis. It is the (3,2) counterpart of the (4,1) bordered matrix in the same module, inside the discrete-geometry stack that assumes $D=3$ spatial slices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.