cmMatrixN_lorentzian_fourOne
plain-language theorem explainer
For a Lorentzian (4,1) causal 4-simplex with spacelike squared length a² and timelike squared length −α a², the bordered Cayley-Menger matrix equals the explicit two-parameter matrix at p=a² and q=−α a². CDT and RS gravity workers cite this when reducing the 4-simplex volume determinant to a closed form. The proof is entrywise Fin-case analysis: every 6×6 entry holds by definitional equality.
Claim. For all real $a$ and $\alpha$, the bordered Cayley-Menger matrix of the squared edge lengths of a Lorentzian type-$(4,1)$ causal 4-simplex (six spacelike edges of squared length $a^2$, four timelike edges of squared length $-\alpha a^2$) equals the two-parameter matrix evaluated at $p = a^2$ and $q = -(\alpha a^2)$.
background
In 4D causal dynamical triangulations (Ambjørn–Jurkiewicz–Loll), spacetime between adjacent spatial slices is filled by two 4-simplex classes. Type (4,1) has four vertices on slice $t$ and one on $t+1$ (six spacelike edges, four timelike); its time reflection (1,4) shares the same edge-length multiset. Spacelike squared lengths are $a^2$; Lorentzian timelike squared lengths are $-\alpha a^2$ with $\alpha > 0$.
The bordered Cayley-Menger matrix is the full $(n+2)\times(n+2)$ matrix of squared distances whose determinant yields simplex volume content. For a 4-simplex one has $n=4$, hence a $6\times 6$ matrix. This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: combinatorial causal classes, Wick rotation as the involution $\alpha \mapsto -\alpha$ on squared lengths, and exact evaluation of the 4-simplex CM determinant on both classes.
proof idea
Pure entrywise identity. Extensionality on matrix indices, then fin_cases on both $i$ and $j$ in $\mathrm{Fin},6$, with each of the 36 cells discharged by rfl. The composed assignment (Lorentzian squared edges of type (4,1), converted to distances, fed to the dimension-parametric CM matrix) is definitionally equal to the closed-form two-parameter matrix at $p=a^2$, $q=-\alpha a^2$. No ring lemmas or determinant facts are used.
why it matters
Direct input to the parent theorem that evaluates the type-(4,1) Lorentzian Cayley-Menger determinant: $\mathrm{cm}_4 = -((8\alpha+3)a^8)$, strictly negative for $\alpha \ge 0$ and $a > 0$. That closed form is the Lorentzian-side counterpart of the Euclidean non-degeneracy thresholds in the Seven-Gaps campaign, and it underwrites the kinematical Wick rotation (sign flip of the timelike parameter). Within Recognition Science gravity this is the 4D lift of the kernel-checked 3D causal-simplex machinery, replacing numerical CDT sampling by exact algebraic volume formulas on the two causal classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.