cm4_regular_unit
plain-language theorem explainer
The regular unit 4-simplex (all ten squared edge lengths equal to 1) has Cayley-Menger determinant equal to 5, matching the classical volume identity V = √5/96 so that 9216 V² = 5. CDT and Regge workers cite it as the Euclidean sanity anchor before non-degeneracy thresholds in α. The proof rewrites the constant-1 edge map as the four-one Euclidean assignment at α = 1, applies the closed four-one evaluation, and finishes by norm_num.
Claim. The 4-simplex Cayley-Menger determinant of the regular unit simplex, with all ten squared edge lengths equal to $1$, equals $5$. Classically this is the identity $9216 V^2 = 5$ for the regular unit 4-volume $V = \sqrt{5}/96$.
background
This module is the 4D Lorentzian (CDT) lift in the QG Seven-Gaps campaign. Between adjacent spatial slices one fills spacetime with two causal 4-simplex types: (4,1) with six spacelike and four timelike edges, and (3,2) with four spacelike and six timelike edges. Spacelike squared lengths are $a^2$; timelike ones are $-\alpha a^2$ in the Lorentzian regime. Wick rotation is the algebraic continuation $\alpha \mapsto -\alpha$ on those edge data.
The quantity cm4 is the bordered 6×6 Cayley-Menger determinant for a 4-simplex (via the dimension-parametric cmDetN), a homogeneous polynomial in the ten squared edge lengths. Positivity of cm4 is the Euclidean non-degeneracy criterion used later to fix exact thresholds $\alpha_{\min}(4,1)=3/8$ and $\alpha_{\min}(3,2)=7/12$.
The regular unit simplex (every squared length 1) is the Euclidean fixed point of that picture: it is what the Wick map produces from the physical point $a=1$, $\alpha=1$ on either causal class.
proof idea
Term-mode, three steps. First rewrite the constant map fun _ => 1 as the Euclidean squared-edge assignment of the (4,1) causal type at $\alpha = 1$ (the lemma that Euclidean edges at unit $\alpha$ are identically 1). Second, apply the closed-form evaluation of cm4 on that (4,1) Euclidean family. Third, norm_num discharges the resulting rational identity to 5. No case split on (3,2) is needed: the constant-1 edge multiset is shared.
why it matters
Sanity anchor for the whole 4D causal-simplex lane: before quoting non-degeneracy thresholds or Lorentzian sign flips, one must recover the classical regular volume. Downstream, physical_point_regular in ThreePentCausalConsistency uses it as the non-vacuity check that at the physical point $a=1$, $\alpha=1$ every pent of the complex Wick-rotates to the regular unit 4-simplex with cm4 = 5.
In the Seven-Gaps gravity program this pins the Euclidean basepoint of the kinematical Wick rotation (Phase 3a), so later strict cm4 negativity on the Lorentzian side and exact degeneracy at $\alpha_{\min}$ are measured against a known positive value rather than an abstract sign. It does not itself force $D=3$ or the eight-tick structure; those sit upstream in the T0–T8 chain. It closes the elementary volume check that any referee expects before the $\alpha$-threshold theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.