wick_eq_continuation
plain-language theorem explainer
On either CDT 4-simplex type, the Wick map sends the Lorentzian squared-edge 10-tuple at parameters (a, α) to the same family at (a, −α). Anyone citing the kinematical Wick rotation for (4,1) or (3,2) simplices uses this identity. The proof is a two-step equality chain: Wick on the Lorentzian class, then algebraic continuation of α.
Claim. For either causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$ and real parameters $a,\alpha$, if $L(\tau,a,\alpha)$ denotes the Lorentzian squared-edge 10-tuple (spacelike edges $a^2$, timelike edges $-\alpha a^2$), then the Wick map satisfies $W_\tau\bigl(L(\tau,a,\alpha)\bigr)=L(\tau,a,-\alpha)$.
background
This module is the 4D Lorentzian lane of the QG Seven-Gaps campaign (Phase 3a): CDT-style causal 4-simplices between adjacent spatial slices, with Wick rotation realized as an explicit map on the ten squared edge lengths.
Two combinatorial types appear. Type (4,1) places four vertices on slice $t$ and one on $t+1$ (six spacelike, four timelike edges); type (3,2) places three and two (four spacelike, six timelike). Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$). The Wick map flips the sign of the timelike squared lengths.
The parameter $\alpha$ here is the CDT edge-ratio parameter, not the electromagnetic fine-structure constant. The theorem packages two prior facts: Wick applied to a Lorentzian tuple, and the algebraic identity that swapping the sign of $\alpha$ in the Lorentzian family is the same operation.
proof idea
Term-mode proof by transitivity of equality. First apply wick_lorentzian, which identifies the Wick image of the Lorentzian squared-edge tuple at $(a,\alpha)$ with an intermediate Euclideanized form. Then apply the symmetric form of lorentzian_continuation, which states that the Lorentzian family at $-\alpha$ equals that same intermediate. The composite is exactly Wick of Lorentzian-$(a,\alpha)$ equals Lorentzian-$(a,-\alpha)$. No case split on the simplex type is needed at this layer; both types are handled uniformly by the two lemmas.
why it matters
Module goal (2) is that Wick is an involution and acts on the causal class as the continuation $\alpha\mapsto -\alpha$. This theorem is the second half of that package: it makes the kinematical Wick rotation identical to analytic continuation in the single free edge-ratio parameter.
That identification is the bridge from Lorentzian CDT edge data to the Euclideanized tuples on which the Cayley–Menger determinant cm4 and the exact non-degeneracy thresholds in $\alpha$ are evaluated (module goals 3–4). The parallel 3D statement in CausalSimplexWick has the same shape for tetrahedra; the 4D version closes the matching gap for pentatopes in $D=4$ (forcing-chain landmark T8).
Downstream, the identity is the citation point whenever a proof needs to replace a Wick image by a sign-flipped Lorentzian parameter without re-expanding the ten edge components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.