regularUnitSqEdges
plain-language theorem explainer
Constant squared-edge assignment for the unit regular tetrahedron: every one of the six edges has squared length 1. Geometry and Regge-calculus checks cite it as the standard regular test point for the Cayley-Menger polynomial and its 5×5 matrix form. The body is the constant function on Fin 6.
Claim. Let $a$ be the map from the six tetrahedron edge indices to $\mathbb{R}$ given by $a(i)=1$ for all $i$. This is the squared-edge data of the unit regular tetrahedron (all edge lengths equal to $1$).
background
The module fixes an explicit degree-3 Cayley-Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths of a tetrahedron, aiming to match classical $288 V^2$ and later compare Regge second-variation coefficients to face areas.
Squared edges are typed as $\mathrm{SqEdges} := \mathrm{Fin},6 \to \mathbb{R}$, with the fixed indexing edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$, and opposite pairs $(0,5)$, $(1,4)$, $(2,3)$.
The classical sanity check is the unit regular tetrahedron: all lengths $1$, volume $\sqrt{2}/12$, hence $288 V^2 = 4$. This definition packages that edge vector for every downstream evaluation.
proof idea
Pure definition: the constant function sending every index in $\mathrm{Fin},6$ to the real $1$. No proof obligations; it is an inhabitant of $\mathrm{SqEdges}$.
why it matters
Supplies the regular unit test point used throughout the Cayley-Menger matrix layer. Downstream, cmDet3_regular_unit proves the $5\times5$ determinant equals $4$ by reducing to the polynomial identity $\mathrm{CM}_3=4$ on this assignment; the same point drives the regular-unit cofactor theorems (entries $1$ on the off-diagonal minors) and the diagonal-minor normal-form comparison.
Those checks close the module's strategy of verifying the explicit polynomial against classical determinants before smoothness and Regge $M_{ij}$ work. In the broader Recognition geometry program this is scaffolding for comparing genuine Cayley-Menger / dihedral derivatives to face areas, not a forcing-chain (T0-T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.