wick_involutive
plain-language theorem explainer
The Wick map on squared edge lengths of a causal tetrahedron is an involution: applying it twice recovers the original lengths. Anyone bridging Lorentzian and Euclidean 3D CDT tetrahedra cites this to treat Wick rotation as a two-sided map, not a one-way flip. The proof is a one-line packaging of the pointwise double-application identity into Mathlib's Involutive predicate.
Claim. For each causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$, the Wick map $W_\tau$ on squared edge lengths (sign flip on every timelike edge, identity on every spacelike edge) is an involution: $W_\tau\circ W_\tau=\mathrm{id}$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps discrete-gravity lane. Prior certified results were Euclidean; here the building blocks are the two CDT tetrahedron classes between adjacent spatial slices in $D=3$: type $(3,1)$ (three vertices on slice $t$, one on $t+1$) and type $(2,2)$ (two vertices on each slice). Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ with $\alpha>0$.
The Wick map $W_\tau$ flips the sign of every timelike squared length and leaves spacelike lengths fixed. Combinatorially this is the algebraic continuation $\alpha\mapsto -\alpha$ on the causal class. Edge indexing follows the Cayley–Menger convention (six edges on four vertices); slice membership is fixed by type, so timelike versus spacelike is decideable.
Upstream, the pointwise identity $W_\tau(W_\tau(x))=x$ is already proved for every squared-edge tuple. The present statement only repackages that identity in Mathlib's Function.Involutive form.
proof idea
One-line term wrapper. The proof is the lambda fun x => wick_wick ty x, which feeds the already-established double-application identity into Mathlib's definition of involutivity. No case split is repeated here: the upstream identity already handles the timelike branch (double negation) and the spacelike branch (identity) by a pointwise by_cases on the edge type.
why it matters
Involutivity is the first certified algebraic property of the kinematical Wick rotation in the Lorentzian CDT layer. The module's program needs it before proving that Wick sends the causal class to the Euclideanized edge tuple, before non-degeneracy of the Euclideanized simplices on the hand-derived parameter range, and before the deficit-angle reality corollary at the physical point $\alpha=1$.
Downstream, the four-dimensional analogue (causal 4-simplex / pentatope Wick involution) follows the same packaging pattern. Within the Recognition forcing chain this sits in the gravity sector after $D=3$ is forced (T8) and after the eight-tick octave (T7): it supplies the discrete Lorentzian-to-Euclidean bridge on tetrahedra rather than a continuum analytic continuation. It closes no open gap by itself; it is scaffolding-free infrastructure for the Lorentzian-sector lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.