physicalCausalTet
plain-language theorem explainer
The physical-point non-degenerate causal tetrahedron at unit spacing and anisotropy α = 1, for either 3d CDT type ((3,1) or (2,2)). Cited by anyone proving deficit-angle reality or dihedral angles on the Euclideanized Lorentzian simplex. One-line specialization of the Euclideanized causal-tet constructor at a = 1, α = 1, discharging positivity of 1 and α_min < 1.
Claim. For either causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$, write $\mathrm{physicalCausalTet}(\tau)$ for the non-degenerate Euclidean tetrahedron obtained by Wick-rotating the Lorentzian edge data at unit spatial edge length $a=1$ and anisotropy parameter $\alpha=1$.
background
This module is the Lorentzian-sector lane of the QG Seven-Gaps campaign. Prior discrete-gravity results in the stack are Euclidean; here one builds certified CDT-style tetrahedron classes in $D=3$, a Wick map on squared edge lengths, and non-degeneracy of the Euclideanized simplices.
Spatial slices are equilateral triangulations with squared edge length $a^2$. Between slices one fills with two types: $(3,1)$ (three vertices on $t$, one on $t+1$: 3 spacelike + 3 timelike) and $(2,2)$ (two on each slice: 2 spacelike + 4 timelike). Spacelike edges have $a^2$; timelike edges have $-\alpha a^2$ Lorentzianly ($\alpha>0$). Wick rotation flips the timelike sign, i.e. continues $\alpha\mapsto -\alpha$.
CausalTetType is the inductive label of those two classes. euclideanCausalTet builds a NonDegenerateTet on a certified $\alpha$-range; the physical point is the regular unit tetrahedron for both types.
proof idea
Definitional one-liner: instantiate euclideanCausalTet at type ty, $a=1$, $\alpha=1$, with the two side conditions one_pos ($1>0$) and alphaMin_lt_one ty (the hand-derived lower threshold for non-degeneracy lies strictly below 1). No further algebra; the heavy lifting lives in the general Euclideanized constructor and the $\alpha_{\min}$ lemmas.
why it matters
Anchors the deficit-angle reality corollary at the physical point (§7 of the module). Downstream, dihedralAngle3_physical shows every edge dihedral of this tet equals $\arccos(1/3)$, and dihedralAngle3_physical_mem_Ioo places that angle in $(0,\pi)$, so all edge deficits of the Euclideanized causal complex are real and well-defined.
At $\alpha=1$ and unit spacing both causal types coincide with the regular unit tetrahedron, so cofactor dihedral cosines are exactly $1/3$. The core non-degeneracy theorem (§5) remains symbolic in $\alpha$; the open fight flagged in the module is sign control of square-rooted degree-2 Cayley–Menger cofactor minors over the full range $\alpha>\alpha_{\min}$. This def only certifies the concrete physical point, which is the kinematical Wick landing needed before Lorentzian Regge calculus can talk about real deficits.
Lives in the gravity/Seven-Gaps stack under the $D=3$ spatial forcing (T8) and the eight-tick discrete time structure that CDT slices sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.