cm4_euclidean_scale
plain-language theorem explainer
The Cayley-Menger determinant of a Euclideanized causal 4-simplex factors out spatial scale as (a²)⁴ = a⁸. Anyone checking 4D CDT non-degeneracy or Wick-rotated volume signs cites this homogeneity. Proof cases on the two CDT types, rewrites each side by the closed-form cm4 evaluations, and finishes with ring.
Claim. For either causal 4-simplex type ((4,1) or (3,2)) and all real $a,\alpha$, if $E(a,\alpha)$ is the 10-tuple of Euclideanized squared edge lengths at spatial scale $a$ and anisotropy $\alpha$, then $\mathrm{CM}_4(E(a,\alpha))=(a^2)^4\,\mathrm{CM}_4(E(1,\alpha))$. Equivalently the bordered 4-simplex Cayley-Menger determinant is homogeneous of degree 4 in the squared distances.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a). Between adjacent spatial slices of equilateral tetrahedra with squared edge length $a^2$, spacetime is filled by two CDT 4-simplex classes: type (4,1) (six spacelike + four timelike edges) and type (3,2) (four spacelike + six timelike). Timelike squared lengths are $-\alpha a^2$ Lorentzian and flip sign under Wick rotation ($\alpha\mapsto -\alpha$).
The object cm4 is the bordered $6\times 6$ Cayley-Menger determinant of a 4-simplex (via the dimension-parametric cmDetN). Euclideanized edge data replace Lorentzian signs so all ten squared lengths are positive multiples of $a^2$ controlled by $\alpha$. Homogeneity of CM determinants in squared distances is classical: degree $n$ for an $n$-simplex, so degree 4 here (the 4D analog of the 3D scaling with exponent 3).
CausalPentType is the inductive label of the two classes; the theorem is stated uniformly over both.
proof idea
Term-mode proof by cases on the causal type.
- On
fourOne, rewrite both sides with the closed-form evaluation ofcm4on Euclideanized (4,1) edge data (once at scale $a$, once at scale 1). The resulting rational expressions in $a$ and $\alpha$ are identical up to the monomial $(a^2)^4$;ringdischarges the identity. - On
threeTwo, the same pattern with the (3,2) closed form, again finished byring.
No external lemmas beyond those two exact evaluations; the homogeneity is read off algebraically rather than from an abstract multi-linearity argument on the bordered matrix.
why it matters
Exact scale factoring lets every later cm4-positivity or degeneracy threshold be reduced to the unit-scale simplex $a=1$, so non-degeneracy bounds become pure inequalities in the anisotropy $\alpha$. That is the kinematical prerequisite for the module's Euclidean non-degeneracy thresholds and for comparing Lorentzian-side cm4 negativity after Wick rotation.
In the Recognition gravity lane this sits inside the 4D causal-simplex / CDT package that lifts the already kernel-checked 3D Wick machinery. It is the direct 4D counterpart of 3D edge-length scaling for Cayley-Menger volumes, and it keeps the seven-gaps Lorentzian sector honest about how the spatial yardstick $a$ enters 4-volume signs. No downstream consumers are wired yet in the graph; the natural parents are the unit-scale threshold theorems and any global Regge or CDT action estimates that normalize $a=1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.