euclideanSqEdges
plain-language theorem explainer
Euclideanized squared-edge lengths for a 3d CDT tetrahedron: spacelike edges carry a², timelike edges carry α a². This is the Wick image of the Lorentzian edge tuple (equivalently the continuation α ↦ −α on the causal class). Discrete-gravity and Cayley–Menger arguments cite it as the edge data for non-degeneracy and deficit-angle checks. The body is a one-line piecewise map on the six edges.
Claim. For a causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$, lattice spacing $a\in\mathbb{R}$, and asymmetry $\alpha\in\mathbb{R}$, define the Euclideanized squared-edge assignment by sending each edge $e$ to $\alpha a^{2}$ if $e$ is timelike for $\tau$, and to $a^{2}$ if $e$ is spacelike. The result is a six-edge squared-length tuple of Cayley–Menger type.
background
This module opens the Lorentzian lane of the QG Seven-Gaps campaign in 3d CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are equilateral triangulations with squared edge length $a^{2}$. Between slices $t$ and $t+1$ the bulk is filled by two causal tetrahedron types: $(3,1)$ (three vertices on $t$, one on $t+1$: three spacelike and three timelike edges) and $(2,2)$ (two vertices on each slice: two spacelike and four timelike edges). The time-reflected $(1,3)$ shares the $(3,1)$ edge multiset.
In the Lorentzian regime, spacelike edges carry $a^{2}$ and timelike edges carry $-\alpha a^{2}$ with $\alpha>0$. Wick rotation flips the sign of the timelike squared lengths and is identified with the algebraic continuation $\alpha\mapsto -\alpha$ on the causal class. Edge indexing follows the Cayley–Menger convention: vertices $0,1,2,3$ and edges $0=(0,1),\ldots,5=(2,3)$. The type CausalTetType records which of the two combinatorial classes is in play; isTimelike decides edge signature from the slice assignment.
SqEdges is the six-component squared-length tuple used by the Cayley–Menger polynomial infrastructure. This definition supplies the Euclideanized tuple that non-degeneracy and deficit-angle results act on.
proof idea
Pure definition, no proof obligations. On each of the six edges, branch on the combinatorial predicate isTimelike ty e: if the edge is timelike for the given causal type, assign $\alpha a^{2}$; otherwise assign $a^{2}$. The result has type SqEdges (a function on the edge index set). No lemmas are applied; the construction is the explicit Wick image of the Lorentzian edge assignment.
why it matters
This is the Euclideanized edge data for the certified Lorentzian layer in the Seven-Gaps gravity campaign. Module goals require an explicit Wick map on squared lengths, non-degeneracy of the Euclideanized simplices on a hand-derived $\alpha$ range, and a deficit-angle reality corollary at the physical point $\alpha=1$; all of those statements are phrased on this tuple (or its Lorentzian sibling).
Downstream, the same pattern feeds Cayley–Menger positivity and threshold-exactness theorems for Euclideanized causal simplices (including the 4d analogues that evaluate cm4 on Euclideanized edges and pin the joint non-degeneracy window $\alpha>7/12$). The campaign ledger re-anchors proved gap flags against imported artifacts, so this edge map is part of the load-bearing discrete-geometry substrate rather than a free-floating convention.
In framework terms it sits in the gravity/Regge lane that builds on $D=3$ spatial structure and the discrete simplex calculus; it does not itself touch the T5–T8 forcing chain or the RCL, but it makes the Euclidean-to-Lorentzian bridge on edge lengths fully algebraic and checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.