wick
plain-language theorem explainer
The Wick map on a causal 4-simplex flips the sign of every timelike squared edge length and leaves spacelike ones fixed. Anyone working the 4D CDT Lorentzian-to-Euclidean continuation cites it as the explicit edge-length map. The body is a one-line pointwise conditional on the combinatorial timelike predicate for the given simplex type.
Claim. For each causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$ and each assignment $x$ of ten real squared edge lengths, the Wick map $W_\tau(x)$ is the assignment with $(W_\tau x)_e=-x_e$ when edge $e$ is timelike for $\tau$, and $(W_\tau x)_e=x_e$ otherwise.
background
This module is the 4D Lorentzian-sector lift in the QG Seven-Gaps campaign (Phase 3a), mirroring the 3D causal-simplex Wick machinery. Spatial slices are equilateral tetrahedra of squared length $a^2$; spacetime between adjacent slices is filled by CDT 4-simplices of two types: $(4,1)$ (four vertices on slice $t$, one on $t+1$: six spacelike + four timelike edges) and $(3,2)$ (three + two: four spacelike + six timelike).
Squared edge data live in $\mathrm{SqEdges}_{10}:=\mathrm{Fin},10\to\mathbb{R}$, indexed in lexicographic order on vertex pairs among ${0,1,2,3,4}$. The predicate isTimelike marks cross-slice edges: indices ${3,6,8,9}$ for $(4,1)$ and ${2,3,5,6,7,8}$ for $(3,2)$. In the Lorentzian regime, spacelike edges carry $a^2$ and timelike edges carry $-\alpha a^2$ with $\alpha>0$; Wick is the algebraic continuation $\alpha\mapsto -\alpha$ realized edgewise.
proof idea
Pure definitional construction, not a theorem. Pointwise on each edge index $e\in\mathrm{Fin},10$, branch on whether the edge is timelike for the given type: if so, negate the squared length; otherwise copy it. No lemmas are applied; the conditional is exactly the combinatorial edge-type assignment already fixed by the slice structure.
why it matters
This is the explicit kinematical Wick rotation on 4-simplex edge data that the rest of the module builds on. Downstream: involution (wick_wick, wick_involutive); on the causal class it equals Euclideanization and the continuation $\alpha\mapsto -\alpha$ (wick_lorentzian, wick_eq_continuation); Lorentzian class members map to Euclideanized tuples (wick_image_euclidean); and the composite non-degeneracy theorem (wick_lorentzian_nondegenerate) certifies $\mathrm{cm}_4>0$ after Wick on the exact $\alpha$ range.
In the Recognition gravity lane this closes the 4D half of the CDT-style Wick story (the 3D analogue lives in CausalSimplexWick). It sits under the $D=3$ spatial forcing (T8) and the eight-tick octave only indirectly: the local object is pure Lorentzian kinematics and Cayley–Menger positivity, not the full dynamical path integral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.