wick_involutive
plain-language theorem explainer
The Wick map on the ten squared edge lengths of a causal 4-simplex is an involution: applying it twice recovers the original tuple. Anyone citing the Lorentzian-to-Euclidean continuation for 4D CDT (4,1) or (3,2) simplices needs this packaging. The proof is a one-line Mathlib wrapper around the pointwise double-flip identity.
Claim. For each causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$, the Wick map $W_\tau$ on squared edge-length 10-tuples is involutive: $W_\tau\circ W_\tau=\mathrm{id}$.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a). Between adjacent spatial slices of equilateral tetrahedra (squared length $a^2$), spacetime is filled by two CDT 4-simplex types: $(4,1)$ with six spacelike and four timelike edges, and $(3,2)$ with four spacelike and six timelike edges. Timelike squared lengths are $-\alpha a^2$ ($\alpha>0$) in the Lorentzian regime.
The Wick map flips the sign of every timelike squared edge length and leaves spacelike ones unchanged; on the causal class this is the algebraic continuation $\alpha\mapsto -\alpha$. Squared lengths are indexed as a 10-tuple in lexicographic edge order on vertices ${0,1,2,3,4}$.
Upstream, the pointwise identity $W_\tau(W_\tau(x))=x$ is already proved by case split on whether each edge is timelike (double negation cancels; spacelike edges are fixed). The 3D analogue in the kernel-checked CausalSimplexWick module uses the same packaging pattern.
proof idea
One-line term-mode wrapper: the Mathlib predicate Function.Involutive is inhabited by feeding the already-proved double-application theorem (pointwise $W(W(x))=x$ for every 10-tuple) as the witness. No new case analysis occurs here.
why it matters
Involutivity is the first structural fact required before the module can assert that Wick acts on the causal class as Euclideanization and before Cayley-Menger evaluations on both sides of the rotation are compared. It anchors the kinematical Wick rotation half of the module brief: the map is an involution and implements $\alpha\mapsto -\alpha$ on causal edge data.
Downstream, the 3D twin statement in CausalSimplexWick mirrors this packaging; the 4D version keeps the Lorentzian-sector lane import-independent while matching conventions. Within Recognition gravity work this is scaffolding for exact cm4 non-degeneracy thresholds and strict cm4 negativity on the Lorentzian side, not a dynamical claim about the path integral measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.