hardcodedConstant_gt_fourOne_threshold
plain-language theorem explainer
The Wick Euclidean-admission threshold for the four-one causal complex sits strictly below 7/12. Anyone auditing the hardcoded causal range in WickActionContinuationCertV2 cites this to separate the four-one gate from the three-two constant. The proof is a two-step term rewrite: identify 7/12 with the three-two threshold, then apply the already-proved four-one < three-two comparison.
Claim. The kinematical Wick continuation threshold of the four-one causal 4-simplex complex is strictly less than $7/12$: $\mathrm{thresh}(4{+}1) < 7/12$.
background
This module answers a referee objection to the action-level Wick certificate WickActionContinuationCertV2, which hardcodes the causal range $\alpha > 7/12$ on a fixed three-pent one-hinge complex of type three-two. The kinematical gate is already type-dependent via alphaMin on causal 4-simplices: $\alpha_{\min}(4{+}1)=3/8$ and $\alpha_{\min}(3{+}2)=7/12$, and these are exact (iff) gates for positive squared 4-volume after Wick rotation.
The Wick continuation threshold of a complex is that type's alphaMin. The constant $7/12$ is therefore the three-two member of the threshold function, not a universal exact gate. The open interval $(3/8,7/12)$ is the four-one-only window: four-one simplices continue there, three-two simplices do not, and no CertV2 can exist because its causalRange field demands $\alpha>7/12$ by construction.
proof idea
Two-line term proof. First rewrite the right-hand side via the sibling equality that identifies the hardcoded constant $7/12$ with the three-two Wick continuation threshold. The goal becomes the four-one threshold strictly below the three-two threshold, which is discharged by the already-proved comparison wickContinuationThreshold_fourOne_lt_threeTwo (itself resting on alphaMin_fourOne = 3/8 < 7/12 = alphaMin_threeTwo).
why it matters
Feeds fourOne_only_window_witness, the concrete witness that at $\alpha=1/2$ every positive spacelike scale admits four-one Euclidean continuation while no WickActionContinuationCertV2 exists. Together with the companion statements that $7/12$ is a complex-independent sufficient threshold (the max of the two type gates) and that no constant is a complex-independent exact gate, this pins the honest status of the hardcoded constant: defensible as a sufficient condition, indefensible as "the" threshold.
In the Seven Gaps / Pillar 1 strengthen campaign this converts a scope caveat into a structural finding about type-dependent Wick admission on causal 4-simplices. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it is local to the gravity/Regge–Wick certificate surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.