cmMatrixN_euclidean_fourOne
plain-language theorem explainer
The bordered Cayley–Menger matrix of a Euclideanized type-(4,1) causal 4-simplex, with spatial scale $a$ and relative parameter $\alpha$, equals the explicit two-parameter matrix at $p=a^2$ and $q=\alpha a^2$. Volume and non-degeneracy calculations in 4d CDT cite this identification. The proof is a finite entrywise case-split that collapses to definitional equality.
Claim. For all real $a$ and $\alpha$, the bordered Cayley–Menger matrix of the squared edge lengths of the Euclideanized type-$(4,1)$ causal 4-simplex equals the two-parameter matrix evaluated at $p = a^2$ and $q = \alpha a^2$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: 4d CDT-style causal 4-simplices between adjacent spatial slices, with Wick rotation as the algebraic continuation $\alpha \mapsto -\alpha$ on squared edge lengths. Type $(4,1)$ places four vertices on slice $t$ and one on $t+1$ (six spacelike edges of squared length $a^2$, four cross-slice edges). In the Euclideanized regime the cross-slice squared lengths are $+\alpha a^2$ with $\alpha > 0$.
The Cayley–Menger matrix is the standard bordered $(n+2)\times(n+2)$ matrix built from squared pairwise distances of an $n$-simplex; here $n=4$, so the matrix is $6\times 6$. The construction cmMatrixN is the dimension-parametric version from Geometry.CayleyMengerN. The Euclideanized $(4,1)$ edge data are packaged as a ten-component squared-length tuple (lex edge order on vertices $0..4$), then fed to that matrix builder.
The right-hand side is the closed two-parameter form of that matrix when all spacelike squares equal $p$ and all cross-slice squares equal $q$, specialized at $p=a^2$, $q=\alpha a^2$.
proof idea
Term-mode proof by matrix extensionality: it suffices that every entry of the $6\times 6$ matrix agrees. Both index types are Fin 6, so fin_cases exhausts all thirty-six pairs $(i,j)$. Each residual goal is definitional equality of the corresponding entry (border zeros/ones versus the squared-distance formula from the Euclideanized $(4,1)$ edge tuple versus the two-parameter template), discharged by rfl. No algebraic lemmas are required beyond the definitions of the matrix builder, the edge map, and the two-parameter template.
why it matters
This is the matrix-level bridge from combinatorial edge data to the scalar Cayley–Menger determinant used for 4-simplex volume and non-degeneracy. The sole direct consumer is cm4_euclidean_fourOne, which rewrites the determinant through this identity and the closed det of the two-parameter matrix to obtain
$\mathrm{cm}_4 = (8\alpha-3)a^8$
for Euclideanized type $(4,1)$. That formula cross-checks the Ambjørn–Jurkiewicz–Loll volume $V(4,1)=(a^4/96)\sqrt{8\alpha-3}$ via $9216 V^2=(8\alpha-3)a^8$, and supplies the exact Euclidean non-degeneracy threshold $\alpha>3/8$ stated in the module program.
In the broader Seven-Gaps campaign this closes the Euclidean side of the kinematical Wick rotation for the $(4,1)$ class in $D=4$, complementary to the Lorentzian sign-flipped evaluation and to the parallel $(3,2)$ lane. It sits downstream of the dimension-parametric CM infrastructure and upstream of positivity/threshold theorems that police degenerate simplices in the causal triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.