wickContinuationThreshold
plain-language theorem explainer
Exact kinematical Wick Euclidean-admission threshold for a labeled causal 4-simplex type: the lower gate on the CDT ratio α at which squared 4-volume stays positive after Wick rotation. Cited by anyone separating the action-level hardcoded 7/12 from a complex-independent constant. One-line projection of the type-wise alpha-min onto the two-type causal index.
Claim. For each causal Wick complex $K$ (an index of CDT type four-one or three-two), the Wick continuation threshold is the real $\alpha_{\min}$ of its underlying causal pent type: $3/8$ for four-one and $7/12$ for three-two. This is the exact non-degeneracy gate for $\mathrm{cm}_4>0$ after Wick Euclideanization.
background
The module treats Work item 5 (outcome b) of the Pillar 1 strengthen campaign: the action-level Wick certificate hardcodes $\alpha>7/12$ on a fixed three-two one-hinge complex, and referees objected that this is not a complex-independent constant. The structural reply is that the kinematical gate is already type-dependent.
CausalWickComplex is a one-field index over the two CDT causal 4-simplex types (four-one and three-two). It carries no incidence or gluing; geometric content lives in the Lorentzian edge squares and the Cayley-Menger 4-volume. Upstream, alphaMin on CausalPentType is the exact non-degeneracy threshold: $3/8$ for four-one and $7/12$ for three-two, as iff gates for $\mathrm{cm}_4>0$ after Wick.
The honest split is that $7/12$ is a complex-independent sufficient threshold (the max of the two type gates) but not a complex-independent exact gate, since four-one continues down to $3/8$. The open window $(3/8,7/12)$ is where that difference is visible.
proof idea
Pure definitional projection: the threshold of a causal Wick complex is alphaMin of its underlying causal pent type. No tactics, no lemmas; the body is the one-field unwrap alphaMin K.ty. The companion equality theorem is definitional reflexivity.
why it matters
This is the named threshold function that turns the referee caveat into a structural finding. Downstream, the arithmetic identification equates the hardcoded $7/12$ with the three-two value; the strict inequality shows it overstates the four-one gate; and the max characterization proves $7/12$ is still a universal sufficient threshold for joint Euclidean admission of both types.
Action-level consequences use it directly: every WickActionContinuationCertV2 lives strictly above the three-two threshold (via the certificate's causalRange field), and in the four-one-only window no such certificate exists even though a four-one simplex admits continuation. That is the precise sense in which $7/12$ is a scope boundary of the certificate, not of the geometry. Outcome (a), genuine multi-complex action-level continuation, remains a separate campaign; this definition only organizes the kinematical side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.