fourTet_regular_sanity
plain-language theorem explainer
At equatorial squared length p = 1 on the unit four-tet hinge star, the common hinge dihedral cosine equals 1/3, recovering the regular tetrahedron. Anyone checking the Cayley-Menger cofactor pipeline against the classical regular value cites this. Proof rewrites the closed-form central-cosine identity and finishes by numerical normalization.
Claim. On the four-tetrahedron star with squared edges $(l,m,m,m,m,p)=(1,1,1,1,1,1)$, the common hinge dihedral cosine equals $1/3$.
background
The module studies an abstract four-tet hinge star: four congruent tetrahedra around a shared edge AB, given only as squared-edge data $(l,m,m,m,m,p)$ with hinge AB as edge 0. Nondegeneracy is the Cayley-Menger sign $\mathrm{cm}_3>0$; no coordinate embedding of the link is formalized.
The common hinge cosine is the repository cofactor formula dihedralCos3Sq. On the kernel-checked slice $l=m=1$ one has the closed form $q(p)=(3-2p)/3$. The configuration starSq 1 is that slice at $p=1$, i.e. all six squared edges equal to 1: the regular tetrahedron, whose classical dihedral cosine is $1/3$.
Upstream, fourTet_centralDihedralCosine supplies the identity $q(p)=(3-2p)/3$ used here; the regular-unit comparison target is the known value recorded as dihedralCos3_regularUnit.
proof idea
One-line tactic proof. Rewrite by fourTet_centralDihedralCosine, which specializes the cofactor formula on $l=m=1$ to $q(p)=(3-2p)/3$. Substitute $p=1$ and finish with norm_num, obtaining $1/3$.
why it matters
Sanity anchor for the signed-Regge four-tet star module: it pins the Cayley-Menger cosine pipeline to the classical regular tetrahedron before any deformation is introduced. The module then runs the family $p(h)=(3/2)(1-h)$, on which $q=h$ exactly, so the signed deficit $2\pi-4\arccos(h)=4\arcsin(h)$ has sign certified by the rational $h$ with no interval arithmetic.
No downstream Lean users yet (used_by empty); the declaration is the basepoint of that deformation story and the check that the abstract star at $p=1$ matches the regular unit tetrahedron. It sits in the geometry layer supporting continuum/Regge bridges (simplicial ledger continuum identification), consistent with the forced $D=3$ spatial setting (forcing chain T8) in which tetrahedral hinges live.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.