LorentzianClass
plain-language theorem explainer
Defines the Lorentzian causal class in 3d CDT: the set of squared-edge 6-tuples obtained from a fixed tetrahedron type by positive lattice spacing a and positive asymmetry alpha. Spacelike edges get a²; timelike edges get −alpha a². Gravity and discrete-QG workers cite it as the domain of the Wick map and of non-degeneracy statements. The body is a pure set comprehension over the Lorentzian edge-length constructor.
Claim. For each causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$, the Lorentzian causal class is the set of squared-edge 6-tuples $x$ for which there exist $a>0$ and $\alpha>0$ with $x$ equal to the Lorentzian edge-length assignment of type $\tau$ at parameters $(a,\alpha)$ (spacelike edges $a^2$, timelike edges $-\alpha a^2$).
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign. Prior discrete-gravity results in the stack are Euclidean; here one builds CDT-style causal tetrahedra in $D=3$ and a kinematical Wick rotation on squared edge lengths.
Two tetrahedron types fill the slab between adjacent spatial slices: $(3,1)$ (three vertices on slice $t$, one on $t+1$: three spacelike and three timelike edges) and $(2,2)$ (two vertices per slice: two spacelike and four timelike). Spatial slices are equilateral with squared length $a^2$; timelike squared lengths are $-\alpha a^2$ with $\alpha>0$. Edge indexing follows the Cayley–Menger convention (six edges on four vertices).
The sibling constructor lorentzianSqEdges packages that assignment into a 6-tuple. The present definition collects all such tuples over $a>0$ and $\alpha>0$ into a set of squared-edge data, the Lorentzian causal class of the given type.
proof idea
Definitional, not a proof. The set is the image of the open first quadrant $(a,\alpha)\in(0,\infty)^2$ under the map $(a,\alpha)\mapsto$ Lorentzian squared-edge 6-tuple of type $\tau$. Membership is existential: unpack witnesses $a,\alpha$ with the two strict positivity hypotheses and equality to that constructor. Downstream theorems typically simp the set membership and obtain those witnesses.
why it matters
This set is the domain object for the certified Lorentzian layer in 3d CDT. In-module, wick_image_euclidean uses membership to conclude that the Wick image is the Euclideanized tuple at the same $(a,\alpha)$. The 4d analogue reuses the same pattern on 10-edge pentachora. Downstream, ThreePentCausalConsistency cites the 4d class to place induced edge data of the three-pent hinge complex inside the Lorentzian class and to state the GAP6-A existence theorem for an admissible causal assignment.
In the Recognition gravity program this is the first certified Lorentzian object on the discrete side: it makes the Ambjørn–Jurkiewicz–Loll edge-type split a Lean set, so Wick rotation, non-degeneracy, and deficit-angle reality at $\alpha=1$ can be stated as maps and theorems on that set rather than as informal parameter ranges. It does not itself force $D=3$ (that is T8 upstream); it assumes the 3d CDT combinatorics of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.