wickContinuationThreshold_fourOne_lt_threeTwo
plain-language theorem explainer
The Wick Euclidean-admission threshold on the four-one causal 4-simplex is strictly smaller than on the three-two simplex: 3/8 < 7/12. Gap witnesses and the complex-independent sufficiency argument cite this comparison to separate the two type gates. The proof rewrites both sides to their closed forms and finishes by numerical comparison.
Claim. The Wick continuation threshold of the four-one causal complex is strictly less than that of the three-two complex: $\alpha_{\min}(\mathrm{fourOne}) < \alpha_{\min}(\mathrm{threeTwo})$, equivalently $\tfrac{3}{8} < \tfrac{7}{12}$.
background
This module sits in the SevenGaps gravity campaign on Wick continuation for causal 4-simplices. Referees objected that the action-level certificate hardcodes the causal range $\alpha > 7/12$ on a fixed three-pent one-hinge complex; the module answers by making the threshold an explicit function of complex type.
A CausalWickComplex packages a causal pent type. The two inhabitants used here are the four-one and three-two types. The threshold function is defined by wickContinuationThreshold K := alphaMin K.ty, the exact gate for positive Cayley-Menger volume after Wick Euclideanization. Upstream evaluations give wickContinuationThreshold fourOneComplex = 3/8 and wickContinuationThreshold threeTwoComplex = 7/12.
The local theoretical point is that kinematical admission is already type-dependent: four-one continues down to $3/8$, while three-two needs $7/12$. The hardcoded $7/12$ is therefore the three-two member of this function, not a universal exact gate.
proof idea
One-line algebraic comparison. Rewrite the left side by wickContinuationThreshold_fourOne to $3/8$, rewrite the right side by wickContinuationThreshold_threeTwo to $7/12$, then close with norm_num. No geometric reasoning remains at this step; the type evaluations already did the work.
why it matters
This strict inequality is the comparison engine behind the module's honesty split between sufficient and exact thresholds. Downstream, hardcodedConstant_gt_fourOne_threshold rewrites the certificate constant $7/12$ as the three-two threshold and applies this lemma to show it overstates the four-one gate. universal_sufficient_threshold_eq_max uses the ordered pair of thresholds so that the joint admission condition is equivalent to exceeding their maximum. fourOne_only_window_witness exploits the open interval $(3/8, 7/12)$: at $\alpha = 1/2$, four-one is Euclidean-admissible while no WickActionContinuationCertV2 exists, because the certificate forces $7/12 < \alpha$ by construction.
In the Recognition gravity stack this closes Work item 5 (outcome b): the kinematical Wick gate is complex-dependent, so the action-level hardcoded constant is defensible only as a sufficient bound. Outcome (a), genuine multi-complex action-level continuation, remains a separate campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.