no_certV2_in_fourOne_only_window
plain-language theorem explainer
Below the three-two Wick threshold (7/12), no action-level Wick continuation certificate exists for any CDT ratio α. Gravity and CDT workers cite this to separate certificate scope from geometry: four-one simplices still admit Euclidean continuation in (3/8, 7/12), but CertV2 cannot. The proof is a one-line absurdity from the certificate's built-in lower bound on α.
Claim. If $\alpha < \alpha_{\min}(\mathrm{three\text{-}two}) = 7/12$, then there is no action-level Wick continuation certificate $\mathrm{CertV2}(\alpha)$. Equivalently: every valid $\mathrm{CertV2}$ forces $\alpha$ at or above the three-two threshold, so the open four-one-only window carries no such certificate.
background
Causal dynamical triangulations (CDT) build 4d spacetime from glued 4-simplices of two combinatorial types: four-one and three-two. After Wick rotation, Euclidean admission is gated by a type-dependent lower bound on the CDT edge-length ratio $\alpha$: $\alpha_{\min}(\mathrm{four\text{-}one}) = 3/8$ and $\alpha_{\min}(\mathrm{three\text{-}two}) = 7/12$. These are exact iff-gates for positive squared 4-volume after Wick.
The action-level certificate WickActionContinuationCertV2 was written against a fixed three-two one-hinge complex and hardcodes the causal range $\alpha > 7/12$. Module work item 5 converts the referee objection ("7/12 is not complex-independent") into a structural split: $7/12$ is a universal sufficient threshold (the max of the two type gates) but not a universal exact gate, since four-one continues down to $3/8$.
The open interval $(3/8, 7/12)$ is therefore the four-one-only window: geometry continues for four-one, while any CertV2 is impossible by construction of its causal-range field.
proof idea
Term-mode reductio. Assume a WickActionContinuationCertV2 at $\alpha$. The upstream lemma certV2_above_threeTwo_threshold extracts from any such certificate the inequality $\alpha \ge$ the three-two wick-continuation threshold. That contradicts the hypothesis $\alpha <$ three-two threshold (via le_of_lt and not_lt). absurd discharges the goal. No case split on simplex type is needed: the certificate surface itself forces the three-two bound.
why it matters
Feeds the concrete witness fourOne_only_window_witness at $\alpha = 1/2$, which packages Euclidean admissibility of every positive-scale four-one simplex together with non-existence of CertV2. That witness is the action-level half of the module's honesty claim: the window is real not only kinematically (cm4 > 0 after Wick) but also at certificate level.
In the Seven Gaps / Pillar 1 campaign this closes the scope caveat on the hardcoded $7/12$: it is a scope boundary of the certificate, not of the geometry. Downstream readers should not treat CertV2 as a complex-independent exact gate. Outcome (a) of the module (action-level continuation for a genuine multi-complex family) remains open; this theorem only records the negative half for the existing CertV2 surface.
Framework contact is local to the gravity/CDT stack rather than T0–T8 forcing, but the pattern matches RS style: make the type-dependence of a threshold explicit instead of papering it as a universal constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.