lorentzian_continuation
plain-language theorem explainer
For either 3D CDT tetrahedron class, the Euclidean squared-edge tuple at parameter α equals the Lorentzian tuple evaluated at −α. Anyone wiring Wick rotation into Regge or CDT kinematics cites this identity. The proof is a pointwise case split on timelike versus spacelike edges plus a one-line ring identity on the sign flip.
Claim. For each causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$ and real parameters $a,\alpha$, the Lorentzian squared-edge assignment at $-\alpha$ equals the Euclidean squared-edge assignment at $\alpha$: $\ell^2_{\mathrm{Lor}}(\tau,a,-\alpha)=\ell^2_{\mathrm{Euc}}(\tau,a,\alpha)$. Spacelike edges keep $a^2$; timelike edges flip the sign of the $\alpha a^2$ term.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign for 3D CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are equilateral triangulations with squared edge length $a^2$. Between adjacent slices the filling uses two tetrahedron types: $(3,1)$ (three vertices on slice $t$, one on $t+1$: 3 spacelike + 3 timelike edges) and $(2,2)$ (two vertices per slice: 2 spacelike + 4 timelike). The inductive type CausalTetType packages exactly those two classes.
In the Lorentzian regime, spacelike edges carry $a^2$ and timelike edges carry $-\alpha a^2$ with $\alpha>0$. The Euclideanized assignment uses $+\alpha a^2$ on the same timelike slots. Edge indexing follows the Cayley–Menger convention (six edges on vertices $0..3$). The companion maps lorentzianSqEdges and euclideanSqEdges build the six-tuples from type, $a$, and $\alpha$; isTimelike decides the slot type from the slice partition.
Prior discrete-gravity work in the monolith is Euclidean. This identity is the algebraic bridge that makes the Wick map on edge lengths equal to the parameter continuation $\alpha\mapsto -\alpha$.
proof idea
Term-mode proof by extensionality on the six edges. Unfold both squared-edge maps, then case on whether the edge is timelike for the given tetrahedron type.
If timelike, both sides reduce to the same if_pos branch; ring equates $(-(-\alpha))a^2$ with $\alpha a^2$. If spacelike, both sides hit the if_neg branch and agree on $a^2$ with no algebra. No external lemmas are required beyond the definitions of the two maps and the timelike predicate.
why it matters
This is the kinematical core of the certified Wick layer in 3D: it proves that Euclideanizing the causal class is literally the algebraic continuation $\alpha\mapsto -\alpha$ of the Lorentzian edge tuple, matching the module claim and the CDT convention that Wick flips the sign of timelike squared lengths.
It feeds wick_eq_continuation in the same module, which composes the explicit Wick map with this identity so that Wick on a Lorentzian tuple equals the Lorentzian tuple at $-\alpha$. The 4D pentachoron twin in CausalSimplex4D copies the same statement. Gap-6 lookalike receipts re-export both the 3D and 4D versions as banked kinematical facts, explicitly noting they are edge-tuple algebra only, not action-level closers.
Within the Seven-Gaps Lorentzian lane this clears the first certified step from Euclidean Regge data toward Lorentzian CDT kinematics, before non-degeneracy ranges and the deficit-angle reality corollary at $\alpha=1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.