wick_wick
plain-language theorem explainer
Applying the Wick map twice to any 10-tuple of squared 4-simplex edge lengths returns the original tuple, for both CDT types (4,1) and (3,2). Anyone working the Lorentzian-to-Euclidean continuation of causal 4-simplices cites this as the raw involution identity. The proof is a pointwise case split on whether each edge is timelike, using double negation on the flipped components.
Claim. For either causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$ and any assignment $x$ of ten real squared edge lengths, if $W_\tau$ flips the sign of every timelike squared length and leaves spacelike ones fixed, then $W_\tau(W_\tau(x))=x$.
background
This module is the 4D Lorentzian lift of the 3D causal-simplex Wick machinery (CDT-style Ambjørn–Jurkiewicz–Loll conventions). Between adjacent spatial slices one fills spacetime with two 4-simplex types: (4,1) has four vertices on slice $t$ and one on $t+1$ (six spacelike, four timelike edges); (3,2) has three on $t$ and two on $t+1$ (four spacelike, six timelike). Squared edge lengths live in $\mathrm{SqEdges}_{10}:=\mathrm{Fin},10\to\mathbb{R}$, ordered lexicographically on vertex pairs among ${0,1,2,3,4}$.
Timelike edges are those that cross slices: indices ${3,6,8,9}$ for (4,1) and ${2,3,5,6,7,8}$ for (3,2). The Wick map $W_\tau$ negates $x(e)$ exactly when $e$ is timelike and leaves spacelike components unchanged. In the causal class this is the algebraic continuation $\alpha\mapsto -\alpha$ on the Lorentzian squared length $-\alpha a^2$. The 3D sibling module states the same involution identity for tetrahedra; this declaration is the independent 4D copy.
proof idea
Pointwise on $\mathrm{Fin},10$. After funext e, case-split on whether the edge is timelike for the given type. If yes, unfold Wick twice and cancel with neg_neg. If no, both applications leave the component untouched, so equality is immediate. No external lemmas beyond the definition of Wick and the Boolean edge-type predicate.
why it matters
Involution is the first structural fact required of the kinematical Wick rotation in the QG Seven-Gaps Lorentzian-sector lane (Phase 3a). Downstream, wick_involutive repackages this identity as Mathlib Function.Involutive, which then feeds the statement that Wick sends the causal class exactly to the Euclideanized edge-length tuple and acts as $\alpha\mapsto -\alpha$. That packaging is what later cm4 non-degeneracy thresholds and Lorentzian-side negativity arguments rely on when comparing Euclidean and Lorentzian regimes of the bordered Cayley–Menger determinant. The same pattern already closed the 3D kernel; this theorem is the 4D counterpart that keeps the two dimensions aligned without importing the 3D module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.