rightAngleUnitSqEdges
plain-language theorem explainer
Canonical squared-edge assignment for the right-angle unit tetrahedron: three orthogonal unit legs from one vertex, three face diagonals of squared length 2. Geometers and Regge analysts cite it as the standard non-regular test point for Cayley–Menger evaluations. The body is a total match on Fin 6 with an absurdity branch for the impossible index.
Claim. Define the squared-edge map $a:\{0,\ldots,5\}\to\mathbb{R}$ of the right-angle unit tetrahedron by $a(0)=a(1)=a(2)=1$ (the three orthogonal unit edges from a common vertex) and $a(3)=a(4)=a(5)=2$ (the three opposite face diagonals).
background
The module builds an explicit degree-3 Cayley–Menger polynomial $CM_3$ in the six squared edge lengths of a tetrahedron, so that classical volume satisfies $288 V^2 = CM_3(a)$. Edges are indexed by $\mathrm{Fin},6$: edges $0,1,2$ leave vertex $0$ toward $1,2,3$; edges $3,4,5$ are the opposite face edges $(1,2)$, $(1,3)$, $(2,3)$. Opposite pairs are $(0,5)$, $(1,4)$, $(2,3)$.
SqEdges is the type of maps $\mathrm{Fin},6\to\mathbb{R}$ recording those six squared lengths. The right-angle unit tetrahedron places three mutually orthogonal unit edges at a single vertex; Pythagoras then forces the three remaining squared lengths to equal $2$. This configuration is the classical check point with $V=1/6$, hence $288 V^2=8$.
The same module also defines the regular-unit edge map; both serve as concrete test vectors before smoothness and scaling identities for $CM_3$ are proved.
proof idea
Pure definitional construction: a function on Fin 6 by pattern match. Indices $0,1,2$ return $1$; indices $3,4,5$ return $2$. The residual clause n+6 is discharged by absurd plus omega, since no element of Fin 6 has value $\ge 6$. No lemmas are invoked.
why it matters
This edge map is the standard non-regular test tetrahedron for the Cayley–Menger program that underwrites rigorous Regge calculus in the monolith. Downstream, cm3_rightAngle_unit evaluates $CM_3=8$ by unfolding and norm_num, matching the classical identity $288 V^2=8$ for $V=1/6$; cmDet3_rightAngle_unit transfers the same check to the $5\times 5$ determinant form.
It also seeds geometric certificates: rightAngleUnit_mem_realisableTetCone places the point in the basic realisability cone, and rightAngleUnitTet packages it as a non-degenerate tetrahedron (all squared edges positive). Both feed ReggeRigorousFoundationCert, which records that $CM_3$ is the fully explicit polynomial needed before comparing the Regge second-variation matrix $M_{ij}$ componentwise to face areas.
In the broader Recognition geometry stack this closes a concrete calibration step toward Philip's concern: genuine dihedral-angle derivatives from Cayley–Menger, not formal placeholders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.