LorentzianClass
plain-language theorem explainer
Defines the Lorentzian causal class of a 4-simplex type as the set of all ten-tuples of squared edge lengths realized by positive lattice spacing a and positive asymmetry alpha under the standard CDT Lorentzian assignment. Anyone working the 4D Wick map, Cayley–Menger sign, or three-pent consistency cites this set. The body is a pure set comprehension over the existing Lorentzian edge map.
Claim. For each causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$, the Lorentzian causal class is the set of all maps $x:\{0,\ldots,9\}\to\mathbb{R}$ for which there exist $a>0$ and $\alpha>0$ with $x$ equal to the standard Lorentzian squared-edge assignment of type $\tau$ at parameters $(a,\alpha)$ (spacelike edges $a^2$, timelike edges $-\alpha a^2$).
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4D CDT lift of the 3D causal-simplex Wick machinery. Spatial slices are equilateral tetrahedra of squared edge $a^2$; spacetime between slices is filled by type $(4,1)$ (six spacelike + four timelike edges) or type $(3,2)$ (four spacelike + six timelike). Timelike squared lengths are $-\alpha a^2$ with $\alpha>0$ in the Lorentzian regime.
CausalPentType is the two-value inductive of those types; SqEdges10 is the type of real 10-tuples indexed in lexicographic edge order on vertices $0..4$. The companion map lorentzianSqEdges builds the concrete assignment from $(a,\alpha)$. The class packages exactly those assignments with strictly positive parameters, matching the 3D LorentzianClass convention in CausalSimplexWick.
proof idea
Definition only: the set of $x$ such that there exist $a,\alpha\in\mathbb{R}$ with $0<a$, $0<\alpha$, and $x=$ the Lorentzian squared-edge map of the given type at $(a,\alpha)$. No lemmas or tactics.
why it matters
This set is the domain language for the 4D kinematical Wick rotation and non-degeneracy lane. Downstream, wick_image_euclidean states that the Wick image of any class member is the Euclideanized tuple at the same witnessing $(a,\alpha)$. In ThreePentCausalConsistency, threePent_lorentzian_class puts each induced edge tuple of the minimal three-pent hinge into this class for type $(3,2)$, and the GAP6-A headline threePent_causal_assignment strengthens that to a single global assignment on the CDT range $\alpha>7/12$ with strict Lorentzian CM negativity and Euclidean CM admissibility after Wick. The definition mirrors the 3D class so the 4D lift stays convention-aligned with Ambjørn–Jurkiewicz–Loll CDT and the module’s $D=4$ Cayley–Menger analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.