wick_image_euclidean
plain-language theorem explainer
Any 4-simplex squared-edge tuple in a Lorentzian causal class (type (4,1) or (3,2)) maps under Wick rotation to a Euclideanized edge tuple with the same positive lattice spacing and asymmetry. Cited by anyone tracking the CDT Wick bridge or cm4 sign analysis in the Seven-Gaps Lorentzian lane. Proof unpacks class membership and rewrites via the algebraic identity that Wick sends Lorentzian edges to Euclidean ones.
Claim. Let $\mathrm{ty}$ be a causal 4-simplex type ((4,1) or (3,2)) and let $x$ be a 10-tuple of squared edge lengths belonging to the Lorentzian causal class of that type. Then there exist $a>0$ and $\alpha>0$ such that the Wick image of $x$ equals the Euclidean squared-edge tuple of type $\mathrm{ty}$ with parameters $(a,\alpha)$ (the same witnesses that place $x$ in the Lorentzian class).
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: the 4D CDT lift of the kernel-checked 3D causal-simplex Wick machinery. Spatial slices are equilateral tetrahedra of squared edge $a^2$. Between slices one fills with two 4-simplex types: (4,1) (six spacelike, four timelike edges) and (3,2) (four spacelike, six timelike). Timelike squared lengths are $-\alpha a^2$ with $\alpha>0$ in the Lorentzian regime.
The Lorentzian causal class is the set of all 10-tuples equal to the standard Lorentzian edge assignment for some $a>0$ and $\alpha>0$. Wick rotation flips the sign of every timelike squared length, equivalently the continuation $\alpha\mapsto -\alpha$ on that class. The Euclideanized tuple is the same assignment with positive timelike squared lengths $\alpha a^2$.
Edge data live in $\mathrm{Fin},10\to\mathbb{R}$ under lexicographic vertex-pair order on the 4-simplex. Downstream the module evaluates the Cayley-Menger determinant $\mathrm{cm}_4$ on both images to get exact Euclidean non-degeneracy thresholds in $\alpha$.
proof idea
One-line unpacking of the set membership. Unfold the Lorentzian class definition to obtain witnesses $a,\alpha>0$ with $x$ equal to the standard Lorentzian edge tuple at those parameters. Substitute into the goal and rewrite by the already-proved identity that Wick of the Lorentzian assignment equals the Euclidean assignment at the same $(a,\alpha)$. No case split on type is needed: the identity is type-parametric.
why it matters
Closes the algebraic half of the 4D kinematical Wick bridge in the Seven-Gaps campaign: Lorentzian class members land in the Euclideanized family, so every subsequent Euclidean positivity or $\mathrm{cm}_4$ computation on the Wick image is legitimate. The module then uses that image to evaluate $\mathrm{cm}_4$ exactly on both causal types, prove Euclidean non-degeneracy thresholds in $\alpha$, and record strict $\mathrm{cm}_4$ negativity on the Lorentzian side.
It is the 4D counterpart of the 3D statement of the same name in CausalSimplexWick, and is the step that turns the combinatorial edge-type assignment into a usable Euclidean continuation. Framework landmark: this is pure CDT kinematics (Ambjorn-Jurkiewicz-Loll conventions), not yet the dynamical measure; it supplies the sign-controlled edge data that later gravity and volume arguments need when $D=4$ is forced (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.