wickContinuationThresholdOf
plain-language theorem explainer
Assigns to each causal 4-simplex type its exact Wick Euclidean non-degeneracy threshold: 3/8 for (4,1) and 7/12 for (3,2). Anyone quantifying over CausalPentType cites this rather than pattern-matching alphaMin. The body is a one-line alias of the typewise alphaMin table.
Claim. For each causal 4-simplex type $\mathrm{ty}\in\{(4,1),(3,2)\}$, the Wick continuation threshold is the real number $\alpha_{\min}(\mathrm{ty})$, equal to $3/8$ on $(4,1)$ and $7/12$ on $(3,2)$.
background
In 4d causal dynamical triangulations, adjacent time slices are glued by 4-simplices of two combinatorial types: $(4,1)$ (four vertices on slice $t$, one on $t+1$) and $(3,2)$ (three and two). After Wick rotation of the squared edge lengths, Euclidean non-degeneracy is controlled by the CDT ratio $\alpha$ of timelike to spacelike squared lengths.
Upstream, alphaMin on causal pent types records the exact gates: $\alpha_{\min}(4,1)=3/8$ and $\alpha_{\min}(3,2)=7/12$. These are iff thresholds for the post-Wick Cayley–Menger determinant $c_{m4}>0$. The module converts a referee objection (the action certificate hardcodes $\alpha>7/12$ on a fixed $(3,2)$ complex) into the structural claim that the kinematical threshold is already type-dependent.
This definition is the type-level packaging of that table, so later statements can quantify over types without case-splitting on the inductive constructors.
proof idea
One-line definitional alias: the value on each type is exactly alphaMin ty from CausalSimplex4D. No proof obligations; the numerical content lives in the upstream pattern match ($3/8$ vs $7/12$).
why it matters
This is the load-bearing threshold function for the whole module. Downstream, wickEuclideanAdmissible_iff states that Wick Euclidean admission holds iff the CDT ratio strictly exceeds this value; exactness at the gate is wickEuclideanAdmissible_false_at_threshold. Non-constancy (wickContinuationThresholdOf_not_constant) and the absence of a common exact gate (no_common_typewise_exact_threshold) both reduce to the two distinct table entries.
The positive companion joint_wickEuclideanAdmissible_iff recovers $7/12$ as the complex-independent sufficient threshold (the max of the two). The fourOne-only window witness at $\alpha=1/2$ uses this definition to show $(4,1)$ continues while no CertV2 exists. In the Seven Gaps / Pillar 1 campaign, it turns the hardcoded $7/12$ from a claimed universal constant into the $(3,2)$ member of a typewise function, without attempting full multi-complex action-level continuation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.