dihedralCos3Sq_alpha_one
plain-language theorem explainer
At the physical point (alpha = 1, unit spacelike edges), every edge of either CDT tetrahedron type has cofactor dihedral cosine exactly 1/3. Anyone proving deficit-angle reality or Euclidean dihedral angles for causal simplices cites this. The proof rewrites the Euclideanized edge data to the regular unit tetrahedron and applies the known cofactor evaluation.
Claim. For either causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$ and every edge $e\in\{0,\ldots,5\}$, the Cayley–Menger cofactor dihedral cosine of the Euclideanized squared-edge data at the physical point $\alpha=1$, $a=1$ equals $1/3$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in $D=3$. Prior discrete-gravity results were Euclidean; here causal (CDT-style) tetrahedra fill the slab between adjacent spatial slices of equilateral triangles. Type $(3,1)$ has three vertices on slice $t$ and one on $t+1$ (three spacelike, three timelike edges); type $(2,2)$ has two vertices on each slice (two spacelike, four timelike). Spacelike squared lengths are $a^2$; timelike ones are $-\alpha a^2$ Lorentzianly. Wick rotation is the algebraic continuation $\alpha\mapsto -\alpha$.
The dihedral cosine is the Cayley–Menger cofactor ratio dihedralCos3Sq: opposite-vertex cofactor over the edge denominator. Upstream, dihedralCos3_regularUnit already proves that on the regular unit tetrahedron this cosine is $1/3$ at every edge, with no external assumptions. The physical Euclideanized edge multiset at $\alpha=1$, $a=1$ is exactly that regular unit configuration for both causal types.
proof idea
One-line term proof. Rewrite the Euclideanized squared-edge data via euclideanSqEdges_alpha_one, which identifies euclideanSqEdges ty 1 1 with the regular unit tetrahedron edge multiset for either causal type. Then apply dihedralCos3_regularUnit e, the cofactor evaluation that yields $\cos\theta=1/3$ on every edge of the regular unit tetrahedron.
why it matters
This is the numerical anchor for deficit-angle reality at the physical point in the causal simplex Wick lane. Downstream, dihedralCos3Sq_alpha_one_mem_Ioo uses it to place the arccos argument strictly in $(-1,1)$, and dihedralAngle3_physical lifts it to $\theta=\arccos(1/3)\in(0,\pi)$ at every edge, so hinge deficits $2\pi-\sum\theta$ are real and well-defined.
In the module's four-step program (causal classes, Wick involution, non-degeneracy, deficit reality), this closes the cosine evaluation half of step 4. It sits in the gravity domain of Recognition Science discrete geometry, feeding Regge-style curvature on CDT tetrahedra once the Euclideanized physical point is certified. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.