joint_wickEuclideanAdmissible_iff
plain-language theorem explainer
Joint kinematical Wick Euclidean admission for both CDT 4-simplex types (4,1) and (3,2) holds if and only if the CDT ratio α strictly exceeds 7/12. Anyone citing the hardcoded causal range on WickActionContinuationCertV2 as a complex-independent sufficient gate needs this equivalence. The proof is a two-sided constructor: the harder type forces α > 7/12, and that bound lifts both types via the per-type threshold lemmas.
Claim. For every positive spacelike scale $a > 0$ and every CDT ratio $\alpha \in \mathbb{R}$, both causal 4-simplex types admit kinematical Wick Euclidean continuation (i.e., $\mathrm{cm}_4 > 0$ after Wick of the Lorentzian squared-edge tuple) if and only if $\alpha > 7/12$.
background
In 4d causal dynamical triangulations the two adjacent-slice 4-simplex types are (4,1) (four vertices on slice $t$, one on $t+1$) and (3,2) (three and two). Each carries a Lorentzian squared-edge tuple scaled by a spacelike length $a$ and a CDT ratio $\alpha$. Wick rotation produces a Euclidean edge tuple; kinematical Euclidean admission is the positivity criterion $\mathrm{cm}_4 > 0$ on that Wick image.
CausalSimplex4D already records exact type thresholds: $\alpha_{\min}(4,1) = 3/8$ and $\alpha_{\min}(3,2) = 7/12$. The module converts a referee objection to the action-level certificate's hardcoded range $\alpha > 7/12$ into a structural fact: that constant is the (3,2) member of the typewise threshold function, not a universal exact gate. Joint admission of both types is the natural complex-independent sufficient condition.
proof idea
Term-mode constructor on the biconditional.
Forward: from the joint pair, discard the (4,1) conjunct and apply the per-type iff for (3,2). After unfolding the continuation threshold to $\alpha_{\min}(3,2) = 7/12$, one obtains $\alpha > 7/12$.
Reverse: assume $\alpha > 7/12$. For each type, invoke the one-sided lemma that admission follows from exceeding that type's threshold. For (4,1) the comparison $3/8 < 7/12 < \alpha$ is closed by linarith; for (3,2) the hypothesis is exactly the threshold inequality. The resulting pair is the joint admission statement.
why it matters
This is the positive half of the module's honesty picture. Downstream, universal_sufficient_threshold_eq_max rewrites the same fact as joint admission iff $\alpha$ exceeds the max of the two named complex thresholds, making the hardcoded $7/12$ defensible as a complex-independent sufficient constant. The companion negative statement (no_common_typewise_exact_threshold) shows it is not an exact gate, since (4,1) continues down to $3/8$.
fourOne_only_window_witness uses the same threshold machinery to exhibit the open window $(3/8, 7/12)$ at $\alpha = 1/2$: (4,1) continues while no WickActionContinuationCertV2 exists, because the certificate's causalRange field is $\alpha > 7/12$ by construction. Within the SevenGaps / Pillar-1 strengthen campaign this closes the scope caveat on the action-level Wick certificate without claiming multi-complex action continuation (outcome (a) remains a separate campaign).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.