euclideanSqEdges
plain-language theorem explainer
Defines the Euclideanized ten-edge squared-length assignment for a causal 4-simplex of either CDT type: spacelike edges get lattice spacing squared $a^2$, timelike edges get $\alpha a^2$. Anyone evaluating Cayley–Menger determinants or non-degeneracy thresholds on the Wick-rotated side cites this map. The body is a one-line pointwise case split on the combinatorial timelike predicate.
Claim. For a causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$ and real parameters $a,\alpha$, the Euclideanized squared-edge tuple is the map on the ten lexicographic edges sending each edge $e$ to $\alpha a^2$ if $e$ is timelike for $\tau$, and to $a^2$ otherwise. This is the image of the Lorentzian assignment (timelike edges $-\alpha a^2$) under Wick rotation, equivalently the continuation $\alpha\mapsto -\alpha$.
background
Module setting is Phase 3a of the QG Seven-Gaps Lorentzian lane: 4D CDT-style causal 4-simplices between adjacent spatial slices, with Wick rotation as an explicit map on the ten squared edge lengths. Spatial slices are equilateral tetrahedra of squared edge $a^2$. Two filling types appear: $(4,1)$ (four vertices on slice $t$, one on $t+1$: six spacelike + four timelike edges) and $(3,2)$ (three + two: four spacelike + six timelike). Reflections $(1,4)$ and $(2,3)$ share the same edge-length multisets.
Squared edge data is a function on $\mathrm{Fin},10$ in lexicographic vertex-pair order. The combinatorial predicate isTimelike marks which of those ten edges cross slices for a given type. In the Lorentzian regime timelike edges carry $-\alpha a^2$ with $\alpha>0$; the Euclideanized tuple flips that sign, so timelike edges carry $+\alpha a^2$. The module evaluates the bordered $6\times 6$ Cayley–Menger determinant cm4 on both classes and extracts exact non-degeneracy thresholds in $\alpha$.
proof idea
Pure definition, not a proof. The body is the pointwise function on edge indices: if the edge is timelike for the given causal type, return $\alpha a^2$; otherwise return $a^2$. No lemmas are applied. Downstream theorems unfold this definition (or the matching matrix builders) and reduce the Cayley–Menger determinant by ring or norm_num arithmetic.
why it matters
This is the Euclidean input to every exact cm4 evaluation in the module. Downstream theorems include cm4_euclidean_fourOne ($\mathrm{cm4}=(8\alpha-3)a^8$, matching the AJL volume identity $9216 V^2=(8\alpha-3)a^8$), the $(3,2)$ companion, the core iff cm4_euclidean_pos_iff (positivity exactly when $\alpha>\alpha_{\min}(\tau)$), joint non-degeneracy for both types on $\alpha>7/12$ (the standard 4d CDT Euclidean-regime bound), and exact degeneracy at threshold. The campaign ledger anchors gap flags against these artifacts.
In the Recognition gravity lane this closes the kinematical Wick step for $D=4$ causal simplices: Lorentzian class continued by $\alpha\mapsto -\alpha$, with Euclidean CM positivity thresholds stated exactly rather than numerically. It does not itself force $D=3$ or the eight-tick structure; those sit upstream in the forcing chain. The classical equivalence of $\mathrm{cm4}>0$ to embeddability in $\mathbb{R}^4$ remains unformalized here (3D analog lives in tetrahedron realization).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.