fourOneComplex
plain-language theorem explainer
Names the (4,1) causal 4-simplex type as an inhabitant of the Wick-complex index class used throughout the threshold comparison. Anyone citing type-dependent Wick Euclidean admission (alphaMin = 3/8 for fourOne versus 7/12 for threeTwo) uses this label. The body is a one-field structure constructor wrapping the CausalPentType.fourOne enum value.
Claim. Let $\mathsf{CausalWickComplex}$ be the one-field index of CDT causal 4-simplex types. Define the $(4,1)$ inhabitant by packing the enum value $\mathsf{fourOne}$ (four vertices on slice $t$, one on $t+1$) into that structure.
background
Causal dynamical triangulations (CDT) in 4d admit two inequivalent causal 4-simplex types between adjacent spatial slices: $(4,1)$ has four vertices on slice $t$ and one on $t+1$ (time reflection $(1,4)$ shares the edge data), while $(3,2)$ has three on $t$ and two on $t+1$. The inductive type CausalPentType records exactly those two constructors.
This module studies the kinematical Wick Euclidean-admission threshold for those types. The structure CausalWickComplex is deliberately a thin label: one field holding a CausalPentType, carrying no incidence or gluing. Geometric content lives in squared edge lengths and the Cayley–Menger determinant cm4, which the threshold theorems call via alphaMin.
The module converts a referee objection (the action-level certificate hardcodes $\alpha > 7/12$ on a fixed threeTwo complex) into a structural fact: the exact gate for cm4 > 0 after Wick is already type-dependent, with $\alpha_{\min}(4,1)=3/8$ and $\alpha_{\min}(3,2)=7/12$.
proof idea
Pure definition: the anonymous constructor of CausalWickComplex applied to CausalPentType.fourOne. No proof obligations, no lemmas, no tactics.
why it matters
This is one of the two named inhabitants that make the complex-dependence of the Wick threshold visible. Downstream, wickContinuationThreshold_fourOne evaluates the threshold on this label to $3/8$; wickContinuationThresholds_differ and wickContinuationThreshold_fourOne_lt_threeTwo compare it to the threeTwo value $7/12$; hardcodedConstant_gt_fourOne_threshold shows the action-level constant $7/12$ strictly overshoots the fourOne gate; and universal_sufficient_threshold_eq_max identifies $7/12$ as the max of the two type thresholds (sufficient for every type, exact for none). Together they underwrite outcome (b) of the pillar: $7/12$ is a complex-independent sufficient bound, not an exact universal gate, and the window $(3/8,7/12)$ is where fourOne continues while the CertV2 surface cannot fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.