wick_eq_continuation
plain-language theorem explainer
Wick rotation on squared edge lengths of a causal CDT tetrahedron sends the Lorentzian edge tuple at parameter α to the same tuple at −α. CDT and discrete-gravity workers cite this to equate the kinematical Wick map with algebraic continuation on the causal class. The proof is a two-step equality: Wick of Lorentzian equals the Euclideanized form, which equals the continued Lorentzian.
Claim. For either causal tetrahedron type ((3,1) or (2,2)) and real parameters $a$, $\alpha$, the Wick map applied to the Lorentzian squared-edge lengths at $(a,\alpha)$ equals the Lorentzian squared-edge lengths at $(a,-\alpha)$.
background
In 3D CDT (Ambjørn–Jurkiewicz–Loll), spacetime between adjacent spatial slices is filled by two tetrahedron types: (3,1) with three vertices on slice $t$ and one on $t+1$, and (2,2) with two on each. Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$). The Wick rotation flips the sign of the timelike squared lengths.
This module is the first certified Lorentzian layer of the QG Seven-Gaps campaign; every prior discrete-gravity result in the stack was Euclidean. The Lorentzian squared-edge assignment packages the edge-type rule above. Companion lemmas identify the Wick image of that assignment with a Euclideanized tuple, and identify the Euclideanized tuple with the algebraic continuation $\alpha\mapsto -\alpha$.
proof idea
Term-mode proof by Eq.trans. Apply the companion lemma that Wick of the Lorentzian edge tuple equals the Euclideanized edge tuple at the same $(a,\alpha)$. Then apply the symmetric form of the continuation lemma, which equates that Euclideanized tuple with the Lorentzian tuple at $(a,-\alpha)$. The composite is the claim. No case split on tetrahedron type or edge index is needed at this layer.
why it matters
Closes item (2) of the module program: on the causal class, Wick acts exactly as $\alpha\mapsto -\alpha$. That identification is the kinematical bridge letting Euclidean Regge/CDT certificates migrate into Lorentzian signature without ad-hoc analytic continuation. Downstream it feeds the non-degeneracy theorems for Euclideanized simplices on the hand-derived parameter range and the deficit-angle reality corollary at the physical point $\alpha=1$. A parallel statement holds for 4D causal pentachora in the sibling CausalSimplex4D lane. Within the Recognition gravity stack this is the discrete-geometry step that opens the Lorentzian sector of the Seven-Gaps campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.