CausalWickComplex
plain-language theorem explainer
One-field index for which of the two CDT causal 4-simplex types is under study when tracking Wick Euclidean-admission thresholds. It wraps the two-constructor enum (4+1 versus 3+2) and carries no geometry. Anyone citing type-dependent Wick gates or the complex-family threshold function uses this label. The declaration is a pure structure definition.
Claim. A causal Wick complex is a one-field record whose only datum is a causal 4-simplex type: either the $(4,1)$ type (four vertices on slice $t$, one on $t+1$) or the $(3,2)$ type (three on $t$, two on $t+1$) of 4d causal dynamical triangulations between adjacent slices.
background
In 4d CDT, adjacent spatial slices are joined by causal 4-simplices of two combinatorial types. The inductive type of those types has constructors $(4,1)$ and $(3,2)$; time reflections $(1,4)$ and $(2,3)$ share the same edge data. Squared edge lengths live on a ten-edge index, and a Cayley–Menger-style quantity cm4 detects non-degeneracy after Wick rotation of the time edges.
This module answers a referee objection to an earlier action-level Wick certificate that hardcoded the causal range $\alpha > 7/12$ on one fixed three-pent one-hinge complex of type $(3,2)$. The kinematical admission gate is already type-dependent: the exact threshold for cm4 > 0 after Wick is $3/8$ for $(4,1)$ and $7/12$ for $(3,2)$.
The present structure is only a label for which type is being tracked. Geometric content stays in the edge-length and cm4 maps that the threshold theorems call.
proof idea
No proof. One-field structure whose sole field is a value of the two-constructor causal 4-simplex type enum. Inhabitants are built by pairing the constructor with either type.
why it matters
Gives a common class so the Wick Euclidean-admission threshold can be stated as a function of complex type rather than a single hardcoded constant. Downstream, the two inhabitants seed the $(4,1)$ and $(3,2)$ labels; the threshold map sends each complex to the exact cm4 non-degeneracy gate of its type; and the equality theorem records that this map is definitionally that gate.
In the Recognition gravity campaign this converts a scope caveat into a structural finding: $7/12$ is a complex-independent sufficient threshold (the max of the two type gates) but not a complex-independent exact gate, since $(4,1)$ continues down to $3/8$. The window $(3/8, 7/12)$ is where type dependence is visible and where the older action certificate cannot exist for $(4,1)$. 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.