wick_wick
plain-language theorem explainer
The Wick map on squared edge lengths of a 3D CDT tetrahedron is an involution: applying it twice recovers the original assignment. Anyone building the Lorentzian sector of the Seven-Gaps discrete-gravity lane cites this as the algebraic backbone of Euclideanization. The proof is a pointwise case split on edge type, using double negation of the sign flip on timelike edges.
Claim. For every causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$ and every assignment $x:\{0,\ldots,5\}\to\mathbb{R}$ of squared edge lengths, the Wick map $W_\tau$ (sign flip on timelike edges, identity on spacelike edges) satisfies $W_\tau(W_\tau(x))=x$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in $D=3$ CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are equilateral triangulations with squared edge length $a^2$; spacetime between adjacent slices is filled by two tetrahedron types: $(3,1)$ (three vertices on slice $t$, one on $t+1$) and $(2,2)$ (two on each slice). Spacelike edges carry $a^2$; 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 predicate isTimelike marks cross-slice edges from the combinatorial slice assignment. The Wick map flips the sign of every timelike squared length and leaves spacelike lengths fixed; on the causal class this is the continuation $\alpha\mapsto -\alpha$.
The same involution statement already appears for 4D causal pentachora (CausalSimplex4D.wick_wick); the present result is the 3D tetrahedron analogue.
proof idea
Pointwise equality of functions $\mathrm{Fin},6\to\mathbb{R}$. After funext on the edge index $e$, case-split on whether $e$ is timelike for the given tetrahedron type.
- If timelike: both applications of Wick insert a minus, so the composite is $-(-x_e)=x_e$ via
neg_neg. - If spacelike: both applications leave the value unchanged, so the composite is $x_e$.
Each branch closes by simplifying the definition of Wick under the corresponding if hypothesis. No external lemmas beyond the definition of the map and basic real arithmetic.
why it matters
Certified involutivity is the first algebraic fact required of any Wick rotation: Euclideanization must be reversible. Downstream, wick_involutive repackages this as Mathlib Function.Involutive, and the same identity is the 3D twin of the 4D CausalSimplex4D.wick_wick / wick_involutive pair.
In the module roadmap this sits under item 2 of the Lorentzian layer: Wick is an involution and acts on the causal class as $\alpha\mapsto -\alpha$. Later non-degeneracy theorems for Euclideanized simplices and the deficit-angle reality corollary at $\alpha=1$ rely on having a well-defined, invertible map from Lorentzian to Euclidean edge data. Within Recognition Science gravity, this is pure kinematics of the discrete Lorentzian sector; it does not yet touch the forcing chain (T0–T8) or the mass ladder, but it is the certified bridge from Euclidean Regge calculus to CDT-style Lorentzian tetrahedra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.