lorentzian_continuation
plain-language theorem explainer
For either CDT 4-simplex type, the ten squared edge lengths in the Lorentzian class at parameter −α equal the Euclideanized lengths at +α. Anyone citing the kinematical Wick rotation or Gap-6 lookalike receipts needs this identity. The proof is a pointwise case split on timelike versus spacelike edges, finished by ring on the timelike branch.
Claim. For each causal 4-simplex type $\mathrm{ty}\in\{(4,1),(3,2)\}$ and real parameters $a,\alpha$, the Lorentzian squared-edge 10-tuple at $-\alpha$ equals the Euclidean squared-edge 10-tuple at $\alpha$: $\ell^2_{\mathrm{Lor}}(\mathrm{ty},a,-\alpha)=\ell^2_{\mathrm{Euc}}(\mathrm{ty},a,\alpha)$. Spacelike edges carry $a^2$; timelike edges carry $-\alpha\,a^2$ (Lorentzian) or $\alpha\,a^2$ (Euclidean).
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4D CDT lift of the kernel-checked 3D causal-simplex Wick machinery. Spatial slices are equilateral tetrahedra of squared edge $a^2$. Between slices one fills with two 4-simplex types: $(4,1)$ (six spacelike + four timelike edges) and $(3,2)$ (four spacelike + six timelike). Time reflections share the same edge-length multiset.
In the Lorentzian regime, spacelike squared lengths are $a^2$ and timelike ones are $-\alpha a^2$ with $\alpha>0$. The Euclideanized assignment keeps spacelike edges at $a^2$ and sets timelike edges to $+\alpha a^2$. The ten edges are indexed lexicographically on vertices ${0,1,2,3,4}$. The type CausalPentType is the inductive label of the two classes; isTimelike decides the edge signature from the slice partition.
The module goal is to treat Wick rotation as an explicit map on the ten squared lengths and prove it acts on the causal class exactly as the algebraic continuation $\alpha\mapsto -\alpha$, before evaluating the Cayley–Menger determinant cm4 on both sides.
proof idea
Pointwise on the ten edges via funext. Unfold both squared-edge maps, then case on whether the edge is timelike for the given type.
On the timelike branch both sides reduce to the same conditional arm; ring equates $-(-\alpha)a^2$ with $\alpha a^2$. On the spacelike branch both arms return $a^2$ with no further algebra. No external lemmas are required beyond the definitions of the two edge maps and the decidable timelike predicate.
why it matters
This is the algebraic half of the 4D kinematical Wick story. Downstream, wick_eq_continuation composes it with the direct Wick-on-Lorentzian identity to conclude that the Wick map on a Lorentzian tuple is exactly the Lorentzian tuple at $-\alpha$. The same pattern is banked in Gap6LookalikeReceipt as lorentzian_continuation_4d_kinematical_banked, and the 3D twin lives in CausalSimplexWick.
In the Seven-Gaps campaign this closes the edge-tuple continuation step for $D=4$ CDT simplices (Ambjørn–Jurkiewicz–Loll conventions). It is kinematical only: it does not evaluate the Regge action or settle dynamical Wick rotation. It feeds the later exact cm4 thresholds (Euclidean non-degeneracy, Lorentzian strict negativity) that the module advertises as Phase 3a deliverables. Framework-wise it sits in the gravity lane that ultimately supports the $D=3$ spatial forcing (T8) and continuum bridge, but the theorem itself is pure edge algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.