alphaMin_threeTwo
plain-language theorem explainer
The Euclidean non-degeneracy threshold for a (3,2) causal 4-simplex is exactly 7/12. Anyone citing the 4d CDT Euclidean regime bound or the joint cm4-positivity theorems needs this value. The proof is pure definitional unfolding by rfl.
Claim. For the causal 4-simplex type with three vertices on one spatial slice and two on the adjacent slice, the exact Euclidean non-degeneracy threshold equals $7/12$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: the 4D CDT lift of the 3D causal-simplex Wick machinery. Between adjacent spatial slices of equilateral tetrahedra (squared edge length $a^2$), spacetime is filled by two 4-simplex types. Type (3,2) places three vertices on slice $t$ and two on $t+1$, giving four spacelike and six timelike edges; type (4,1) is the complementary count.
Timelike squared lengths are $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$). Wick rotation continues $\alpha\mapsto -\alpha$. The Cayley-Menger determinant cm4 (bordered 6×6, from cmDetN) supplies the Euclidean non-degeneracy test. The threshold function alphaMin packages the exact critical values: $3/8$ for (4,1) and $7/12$ for (3,2). The 3D analog used $1/3$ and $1/2$ for the tetrahedron types.
proof idea
One-line definitional equality. The definition of alphaMin on the threeTwo constructor is literally 7/12, so rfl closes the goal with no further lemmas.
why it matters
Pins the numerical threshold that every downstream Euclidean-regime statement quotes. cm4_euclidean_degenerate_at_min rewrites at this value to prove cm4=0 exactly on the boundary. cm4_euclidean_pos_iff uses it for the sharp iff cm4>0 \Leftrightarrow \alpha>\alpha_{\min}. The joint theorem cm4_euclidean_pos_joint then takes the stricter bound $\alpha>7/12$ so both causal types are simultaneously non-degenerate, recovering the standard 4d CDT Euclidean window. That same bound is imported by threePent_euclidean_admissible to guarantee that all three pents of a causal consistency configuration Euclideanize at once. In the Recognition gravity lane this is pure kinematics (Cayley-Menger positivity), not yet the dynamical measure or the forcing-chain landmarks T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.