wick
plain-language theorem explainer
The Wick map on squared edge lengths of a 3D CDT tetrahedron: negate every timelike edge, leave spacelike edges fixed. Anyone working the Lorentzian-sector Seven-Gaps lane cites it as the explicit kinematical bridge from Lorentzian causal tuples to Euclideanized ones. The body is a one-line pointwise conditional on the combinatorial edge-type predicate.
Claim. Given a causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$ and a squared-edge assignment $x:\{0,\ldots,5\}\to\mathbb{R}$, the Wick map returns $W_\tau(x)$ with $(W_\tau x)(e)=-x(e)$ if edge $e$ is timelike for $\tau$, and $(W_\tau x)(e)=x(e)$ otherwise.
background
This module opens the Lorentzian layer of the QG Seven-Gaps campaign for $D=3$ CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are equilateral triangulations with squared length $a^2$; spacetime between slices is filled by 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). In the Lorentzian regime spacelike edges carry $a^2$ and timelike edges carry $-\alpha a^2$ with $\alpha>0$.
Squared edge data live in SqEdges $=\mathrm{Fin},6\to\mathbb{R}$, indexed as in the Cayley–Menger setup (edges $0=(0,1),\ldots,5=(2,3)$). The sibling predicate isTimelike marks cross-slice edges from the fixed slice assignment. The Wick map is the algebraic sign flip on those edges, i.e. the continuation $\alpha\mapsto -\alpha$ on the causal class.
proof idea
Pure definition: pointwise on each of the six edges, branch on whether the edge is timelike for the given causal type. If yes, return the negation of the input squared length; if no, return the input unchanged. No lemmas are invoked; the subsequent involution and continuation theorems are proved from this clause by case analysis on the same predicate.
why it matters
This is the explicit kinematical Wick rotation that every Lorentzian-sector result in the module hangs on. Downstream it feeds the involution theorem, the identity that Wick sends Lorentzian causal tuples to Euclideanized ones, the continuation statement $\alpha\mapsto -\alpha$, the image-is-Euclidean membership lemma, and the composite non-degeneracy theorem (Wick image has positive Cayley–Menger determinant on the certified $\alpha$ range). The 4D sibling module copies the same pattern on pentachora. Within Recognition Science this is the first certified bridge from Euclidean discrete gravity (all prior formal and numerical work) into the Lorentzian sector needed for physical deficit angles at $\alpha=1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.