euclideanSqEdges_alpha_one
plain-language theorem explainer
At unit spatial edge length and unit causal parameter, both CDT 4-simplex types Euclideanize to the regular unit 4-simplex: all ten squared edge lengths equal 1. Gravity and CDT workers cite it as the physical-point anchor for Cayley-Menger and Wick-rotation sanity checks. The proof is a pointwise case split on timelike versus spacelike edges; both branches reduce to 1 by arithmetic.
Claim. For either causal 4-simplex type $\tau$ (the $(4,1)$ or $(3,2)$ CDT class between adjacent slices), the Euclideanized squared-edge assignment at $a=1$ and $\alpha=1$ is the constant map $e \mapsto 1$ on all ten lexicographic edges.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: CDT-style 4-simplex classes in $D=4$ and their kinematical Wick rotation. Spatial slices are equilateral tetrahedra of squared edge length $a^2$. Between slices one fills with two types: $(4,1)$ (six spacelike + four timelike edges) and $(3,2)$ (four spacelike + six timelike). Timelike squared lengths are $-\alpha a^2$ Lorentzian; Wick rotation continues $\alpha \mapsto -\alpha$, flipping those signs.
CausalPentType is the inductive label for those two classes. The Euclideanized squared-edge map assigns $a^2$ on spacelike edges and $\alpha a^2$ on timelike edges (the positive continuation). The ten edges are indexed lexicographically on vertices $0..4$. At the physical point $a=\alpha=1$ every edge, regardless of type, should carry squared length $1$, recovering the regular unit 4-simplex tuple used by the bordered Cayley-Menger determinant cm4.
proof idea
Extensionality on the ten edges, then unfold the Euclideanized edge map. Case-split on whether the edge is timelike for the given causal type. In the timelike branch the if fires and the expression is $\alpha a^2$ at $(1,1)$, which norm_num reduces to $1$. In the spacelike branch the complementary if fires and the expression is $a^2=1$. No external lemmas beyond the definition and Boolean case analysis.
why it matters
Sanity anchor for the Euclidean physical point in the 4D causal-simplex stack. Downstream, cm4_regular_unit rewrites through this identity and the four-one Euclidean evaluation to obtain cm4 = 5 (classical $V=\sqrt{5}/96$, so $9216 V^2=5$). physical_point_regular in the three-pent consistency module uses it to show every pent of the complex Wick-rotates to the regular unit 4-simplex with cm4=5, a non-vacuity check. The 3D sibling in CausalSimplexWick is the same statement for tetrahedra and feeds the cofactor dihedral cosine $1/3$ at the physical point. Within the Seven-Gaps campaign this closes the Euclidean endpoint of the Wick involution before the exact non-degeneracy range in $\alpha$ is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.