star_denom
plain-language theorem explainer
On the four-tetrahedron star edge data with rim parameter p, the Cayley-Menger dihedral denominator at the shared hinge is the constant 3 for every real p. Downstream work on the rational central-dihedral cosine cites this identity. The proof substitutes the two hinge-adjacent cofactors (each -3) and takes a positive square root.
Claim. For every real $p$, the Cayley-Menger dihedral denominator of the four-tetrahedron star squared-edge configuration with rim squared length $p$, evaluated at the hinge edge, equals $3$.
background
The module studies an abstract four-tet hinge star: four congruent tetrahedra around a common edge AB, given only as squared-edge data. With repository vertex order (A,B and equatorial pair), the edge vector is $(l,m,m,m,m,p)$; the kernel-checked slice fixes $l=m=1$ and varies the rim $p$. Nondegeneracy is the Cayley-Menger sign $\mathrm{cm}_3>0$.
Dihedral cosines at AB are computed from Cayley-Menger cofactors. The denominator piece (square root of a product of the two face-adjacent principal cofactors) is what this theorem evaluates. Sibling lemmas already pin those cofactors on the star: each equals $-3$ when $l=m=1$. The module header records the offline general formula $q(l,m,p)=(l-4m+2p)/(l-4m)$, of which the $l=m=1$ slice is the rational certificate proved later.
proof idea
Term-mode proof. Unfold the dihedral-denominator definition and simplify the opposite-vertex indexing for the hinge. Rewrite the two principal cofactors via the sibling identities that each equals $-3$ on the star. Reduce $(-3)\cdot(-3)=3^2$ by norm_num, then apply Real.sqrt_sq with a nonnegativity witness (again norm_num) to obtain the constant $3$.
why it matters
This constant clears the denominator in fourTet_centralDihedralCosine, the rational certificate that the hinge dihedral cosine equals $(3-2p)/3$ for all real $p$. That identity is the kernel-checked $l=m=1$ slice of the module's general cofactor formula and is the algebraic engine behind signed Regge deficits on the star: with the deformation $p=(3/2)(1-h)$ one gets cosine $=h$ on the nose, so $\mathrm{deficit}(h)=4\arcsin(h)$ and the sign of the deficit is the sign of a rational, with no arccos numerics.
In the broader Recognition geometry stack this is the first kernel-checked signed deficit family on an abstract four-tet star (not a full Triangulation3D embedding). It sits under the geometry domain that feeds continuum bridges and simplicial ledger identifications, where hinge deficits appear as discrete curvature sources.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.