threeTwoComplex
plain-language theorem explainer
Names the three-two causal 4-simplex type as an inhabitant of the common Wick-complex class. Anyone comparing type-dependent Wick Euclidean-admission thresholds cites it as the label for the CDT (3,2) simplex. The definition is a one-field structure constructor over the inductive constructor CausalPentType.threeTwo.
Claim. Let $\mathsf{CausalWickComplex}$ be the one-field index of CDT causal 4-simplex types. Define the three-two complex as the inhabitant whose type field is the $(3,2)$ causal pent type (three vertices on slice $t$, two on slice $t+1$).
background
In 4d causal dynamical triangulations, adjacent spatial slices are joined by two inequivalent causal 4-simplex types. The inductive type CausalPentType records them: fourOne (four vertices on slice $t$, one on $t+1$, and its time reflection) and threeTwo (three on $t$, two on $t+1$, and its reflection). Edge data and the Cayley-Menger determinant cm4 (sign-normalized so cm4 > 0 means a non-degenerate Euclidean 4-simplex, with cm4 = 9216 V^2) live on squared edge lengths, not on this label.
This module answers a referee objection to the action-level Wick certificate, which hardcodes the causal range $\alpha > 7/12$ on a fixed three-two one-hinge complex. The kinematical Wick Euclidean-admission gate is already type-dependent via alphaMin: $3/8$ for four-one and $7/12$ for three-two, each an exact iff condition for cm4 > 0 after Wick. CausalWickComplex is deliberately a thin wrapper over the two-constructor enum: it carries no simplices, incidence, or gluing, only which causal type is under discussion.
proof idea
Pure structure introduction: pack the inductive constructor CausalPentType.threeTwo into the single field of CausalWickComplex. No lemmas, no tactics, no arithmetic.
why it matters
This constant is the handle every type-indexed threshold statement in the module uses for the $(3,2)$ side. Downstream, wickContinuationThreshold_threeTwo identifies its continuation threshold with $7/12$; hardcodedConstant_eq_threeTwo_threshold equates that value to the literal baked into WickActionContinuationCertV2; and certV2_above_threeTwo_threshold shows every action-level certificate lives strictly above this gate. Gap witnesses such as wickContinuationThreshold_fourOne_lt_threeTwo, universal_sufficient_threshold_eq_max, and no_certV2_in_fourOne_only_window compare it against the four-one inhabitant to prove that $7/12$ is a complex-independent sufficient threshold (the max of the two type gates) but not an exact common gate, and that the open window $(3/8, 7/12)$ is visible even at certificate level. Together with fourOneComplex it supplies the two inhabitants needed by causalWickComplex_two_inhabitants. 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.