wick_lorentzian
plain-language theorem explainer
On either CDT causal 4-simplex type, the Wick map sends the Lorentzian squared-edge tuple to the Euclideanized one. Cited by anyone proving the 4D kinematical Wick rotation or cm4 non-degeneracy after rotation. Proof is a pointwise case split on the ten edges: flip sign on timelike edges (double negation), leave spacelike edges fixed.
Claim. For either causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$ and real parameters $a,\alpha$, applying the Wick map to the Lorentzian squared-edge lengths (spacelike edges $a^2$, timelike edges $-\alpha a^2$) yields exactly the Euclideanized lengths (spacelike $a^2$, timelike $+\alpha a^2$).
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: the 4D CDT lift of the already kernel-checked 3D causal-simplex Wick machinery. Spatial slices are equilateral tetrahedra of squared edge length $a^2$; spacetime between adjacent slices is filled by two 4-simplex types. Type $(4,1)$ has four vertices on slice $t$ and one on $t+1$ (six spacelike, four timelike edges); type $(3,2)$ has three on $t$ and two on $t+1$ (four spacelike, six timelike). Time reflections share the same edge-length multisets.
In the Lorentzian regime, spacelike edges carry $a^2$ and timelike edges carry $-\alpha a^2$ with $\alpha>0$. The Euclideanized tuple flips the timelike sign to $+\alpha a^2$. The Wick map is the explicit sign flip on those edges classified as timelike by the slice structure. The ten edges are indexed lexicographically on vertices ${0,1,2,3,4}$.
Upstream, euclideanSqEdges is defined as the pointwise conditional that puts $\alpha a^2$ on timelike edges and $a^2$ elsewhere; the Lorentzian twin uses the opposite timelike sign. The causal type is the inductive CausalPentType with constructors fourOne and threeTwo.
proof idea
Term-mode proof by functional extensionality on the ten edges. For each edge $e$, case-split on whether it is timelike for the given type. On the timelike branch, unfold Wick, Lorentzian, and Euclidean definitions; the if_pos arms give $-(-\alpha a^2)=\alpha a^2$ via neg_neg. On the spacelike branch, all three definitions agree on $a^2$ via if_neg. No external lemmas beyond the local definitions and Boolean case analysis.
why it matters
This is the elementary identification that makes the 4D kinematical Wick rotation algebraic rather than analytic. Downstream, wick_eq_continuation composes it with the Lorentzian continuation identity to prove Wick acts as $\alpha\mapsto -\alpha$ on the causal class; wick_image_euclidean lifts the identity to set membership in the Lorentzian class; and wick_lorentzian_nondegenerate rewrites through it to obtain cm4>0 on the Wick image whenever $\alpha$ exceeds the exact Euclidean threshold. The same pattern is mirrored in the 3D module CausalSimplexWick, and ThreePentCausalConsistency.physical_point_regular consumes the 4D form.
In the Seven-Gaps campaign this closes the "Wick produces the Euclideanized tuple" step of Phase 3a, before Cayley-Menger positivity and the classical embeddability upgrade. It sits in the Lorentzian-sector lane that ultimately supports discrete gravity kinematics consistent with the RS forcing chain's $D=3$ spatial dimensions (T8) once the time direction is restored.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.