cm3_euclidean_pos_joint
plain-language theorem explainer
Both 3d CDT causal tetrahedron classes, (3,1) and (2,2), are simultaneously Euclidean-non-degenerate exactly when the anisotropy exceeds 1/2 (with positive spatial edge scale). Discrete-gravity and CDT workers cite this as the joint Euclidean-regime bound after Wick rotation. The proof packages the two per-type Cayley–Menger positivity lemmas and discharges each type’s alphaMin hypothesis from alpha > 1/2 by rewrite plus linear arithmetic.
Claim. Let $a>0$ and $\alpha>1/2$. Write $E_{3,1}(a,\alpha)$ and $E_{2,2}(a,\alpha)$ for the six Euclidean squared edge lengths of the Wick-rotated $(3,1)$ and $(2,2)$ causal tetrahedra (spacelike edges $a^2$, former-timelike edges $\alpha a^2$). Then the Cayley–Menger polynomial satisfies $\mathrm{CM}_3(E_{3,1}(a,\alpha))>0$ and $\mathrm{CM}_3(E_{2,2}(a,\alpha))>0$.
background
This module is the first certified Lorentzian layer of the QG Seven-Gaps campaign in $D=3$. Spatial slices are equilateral triangulations with squared edge length $a^2$. Between adjacent slices one fills with two CDT tetrahedron types: $(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). In the Lorentzian regime timelike squared lengths are $-\alpha a^2$ with $\alpha>0$; the kinematical Wick map flips that sign, equivalently continuing $\alpha\mapsto -\alpha$ on the causal class.
Non-degeneracy is read from the Cayley–Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths (from Geometry.CayleyMengerPolynomial): strict positivity means positive squared 3-volume, i.e. a non-degenerate Euclidean tetrahedron. The map euclideanSqEdges builds those six lengths from a causal type, scale $a$, and anisotropy $\alpha$. Each type has its own exact threshold alphaMin; the classical 3d CDT Euclidean regime is the joint half-line $\alpha>1/2$.
proof idea
Term-mode pair constructor. The left conjunct is cm3_euclidean_pos at type $(3,1)$ with the scale hypothesis $a>0$ and the type-wise bound alphaMin threeOne < alpha, obtained by rewriting alphaMin_threeOne and closing with linarith from $\alpha>1/2$. The right conjunct is the same lemma at type $(2,2)$, discharging alphaMin twoTwo < alpha via alphaMin_twoTwo and linarith. No new algebraic expansion of $\mathrm{CM}_3$ occurs here; the work is the joint packaging under the common CDT bound.
why it matters
Closes item 3 of the module program: a single, hand-derived parameter range on which both Euclideanized causal classes are non-degenerate, matching the standard 3d CDT Euclidean-regime bound $\alpha>1/2$. That joint range is what licenses NonDegenerateTet instances and the deficit-angle reality corollary at the physical point $\alpha=1$ (module roadmap item 4). In the broader Recognition stack this is the $D=3$ Lorentzian-sector lane of Seven-Gaps: prior discrete-gravity results were Euclidean-only; Wick rotation plus certified non-degeneracy is the bridge. The forcing chain’s $T8$ ($D=3$ spatial) is the ambient dimension in which these two CDT classes live. No downstream consumers are wired yet (used_by empty); the natural parents are the degeneracy-threshold exactness theorem at $\alpha=\mathrm{alphaMin},ty$ and any Regge deficit or measure construction that needs both types open at once.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.