simplexVolumeSqN_eq_cm4_div
plain-language theorem explainer
The squared 4-volume of a 4-simplex from the dimension-parametric Cayley-Menger formula equals the module's bordered 6x6 determinant divided by 9216. Volume-normalization work in the CDT 4-simplex lane cites this to lock sign and scale against the shared Geometry.CayleyMengerN layer. The proof unfolds both definitions, evaluates 4! = 24 by norm_num, and closes with ring on the factor 2^4 (4!)^2.
Claim. For every assignment $x$ of ten real squared edge lengths on a 4-simplex (lexicographic order on the ten edges of five vertices), the squared 4-volume from the $n$-dimensional Cayley-Menger formula at $n=4$ equals $C_4(x)/9216$, where $C_4(x)$ is this module's bordered $6\times 6$ Cayley-Menger determinant and $9216 = 2^4\cdot(4!)^2$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: the 4D CDT lift of causal-simplex machinery. Spacetime between successive spatial slices is filled by two 4-simplex types, (4,1) and (3,2), with spacelike squared lengths $a^2$ and timelike squared lengths $-\alpha a^2$ ($\alpha>0$) in the Lorentzian regime. The ten squared edge lengths of any such simplex are packaged as a map from a 10-element index set into the reals (lexicographic edge order on vertices $0..4$).
The classical Cayley-Menger identity expresses the squared volume $V^2$ of an $n$-simplex as a normalized bordered determinant of squared distances. At $n=4$ the absolute normalizing constant is $2^4(4!)^2=9216$. The geometry layer supplies a dimension-parametric squared-volume functional; this module defines a local bordered $6\times 6$ determinant $C_4$ grounded in that same parametric determinant, and needs the two normalizations to agree exactly (including sign).
No causal or Lorentzian hypothesis enters the comparison: it is pure bookkeeping between the two presentations of the same determinant.
proof idea
Unfold the parametric squared-volume definition and the local $C_4$ abbreviation so both sides are explicit rational expressions in the bordered determinant and the factorial normalizer. The single numeric fact required is $(4!:\mathbb{N})=24$ as a real, proved by norm_num on Nat.factorial. Rewrite with that equality; ring then identifies the remaining constant $2^4\cdot 24^2$ with $9216$ and closes the equality. No lemmas about edges, slices, or causality are invoked.
why it matters
Exact evaluations of the bordered determinant on the two CDT classes (and the Euclidean non-degeneracy thresholds in $\alpha$, plus strict negativity on the Lorentzian side) only become squared-volume statements once $C_4$ is tied to the shared $n$-dimensional volume formula. This theorem is that tie: it fixes sign and the factor $9216=2^4(4!)^2$ against Geometry.CayleyMengerN, as the doc-comment states.
No parent theorem yet records a use edge, so the declaration is presently a normalization hinge rather than a cited lemma in a larger proof. Framework-wise it supports the 4D (spatial $D=3$) CDT kinematical Wick-rotation analysis in the gravity seven-gaps campaign; it is not part of the T0-T8 forcing chain, the Recognition Composition Law, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.