WickEuclideanAdmissible
plain-language theorem explainer
Kinematical Wick Euclidean admission is the predicate that, after Wick-rotating a Lorentzian causal 4-simplex of a given type at spacelike scale a and CDT ratio α, the Cayley–Menger 4-volume form stays strictly positive. Gravity and CDT workers cite it as the load-bearing gate behind type-dependent continuation thresholds (3/8 for four-one, 7/12 for three-two). The definition is a one-line positivity check on the Wick image of the Lorentzian squared-edge tuple.
Claim. For a causal 4-simplex type $\mathrm{ty}$, spacelike scale $a\in\mathbb{R}$, and CDT ratio $\alpha\in\mathbb{R}$, Wick Euclidean admission holds when $0 < \mathrm{cm}_4\bigl(W_{\mathrm{ty}}(L_{\mathrm{ty}}(a,\alpha))\bigr)$, i.e. the Cayley–Menger 4-form of the Wick-rotated Lorentzian squared-edge lengths is strictly positive.
background
This module sits in the SevenGaps gravity campaign on Wick continuation for causal 4-simplices. Causal pent types are the two combinatorial classes of Lorentzian 4-simplices used in CDT-style assemblies: four-one and three-two. Each type carries a Lorentzian squared-edge assignment at spacelike scale $a$ and ratio $\alpha$, then a type-dependent Wick map that Euclideanizes the timelike edges.
The scalar $\mathrm{cm}_4$ is the 4D Cayley–Menger determinant (volume-squared form) on six edge lengths of a 4-simplex. Positivity of $\mathrm{cm}_4$ is the kinematical Euclidean-admission criterion: the Wick image must still describe a nondegenerate Euclidean 4-simplex.
Module scope is deliberately kinematical. Action-level certificates such as WickActionContinuationCertV2 hardcode $\alpha>7/12$ on a fixed three-two one-hinge complex; this definition isolates the pure geometric gate so that type dependence of the threshold can be stated without the action analytic chain. Upstream, $\alpha_{\min}$ on the causal simplex side already records the exact gates $3/8$ (four-one) and $7/12$ (three-two).
proof idea
Definitional abbreviation, not a proof. The body unfolds to a single strict inequality: apply the type's Lorentzian squared-edge map at $(a,\alpha)$, Wick-rotate that edge tuple, then require $\mathrm{cm}4>0$ on the result. No lemmas are invoked at the definition site; downstream iff theorems unfold this predicate and rewrite via the Wick–Lorentzian identity to the comparison $\alpha{\min}(\mathrm{ty})<\alpha$.
why it matters
This predicate is the common interface for the module's structural finding that Wick Euclidean admission is type-dependent. Downstream, the iff theorem makes the general threshold function load-bearing: admission holds exactly when $\alpha$ strictly exceeds the type's continuation threshold. Degeneracy at threshold, one-sided sufficiency above threshold, and the gap witness all quote this predicate.
Joint admission of both types is equivalent to $7/12<\alpha$ (the max of the two thresholds), so $7/12$ remains a complex-independent sufficient constant while failing as a universal exact gate (no_common_typewise_exact_threshold). The four-one-only window witness at $\alpha=1/2$ uses admission for four-one together with nonexistence of the action certificate, closing the referee objection that hardcoded $7/12$ was misread as universal. Outcome (a), full action-level multi-complex continuation, remains a separate campaign; this definition only underwrites the kinematical half of that honesty split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.