starMinor34Matrix
plain-language theorem explainer
Explicit 4×4 normal form of the (3,4) Cayley–Menger minor for the one-parameter star tetrahedron (squared equatorial edge p). Anyone computing star-local cofactors or the signed Regge deficit on the four-tet hinge cites this matrix. The body is a pure matrix literal; no proof.
Claim. For $p \in \mathbb{R}$, the normal form of the $(3,4)$ Cayley–Menger minor of the star tetrahedron is the matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & 1 & 1 \\ 1 & 1 & 0 & 1 \\ 1 & 1 & 1 & p \end{pmatrix}.$$
background
The module studies signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior edge AB in a closed 4-cycle link. Squared edges are locked to the panel $(l,m,m,m,m,p)$; the kernel-checked slice is $l=m=1$, with deformation parameter $p$ (flat value $p_0=3/2$).
Cayley–Menger determinants and their cofactors supply dihedral cosines without coordinates. The full $5\times5$ Cayley–Menger matrix of the star (built from the squared-edge vector) has a $(3,4)$ principal minor whose entries, after the repository edge convention, collapse to the simple pattern above: three zero diagonals among the first three rows/columns, ones off-diagonal, and $p$ in the bottom-right corner.
That minor enters the cofactor formula for the common dihedral cosine at the hinge; its determinant is the algebraic engine behind the sign of the deficit.
proof idea
Definition only: the matrix is introduced by a single !![...] literal with entries $0,1,1,1$ on the first three rows in the usual bordered pattern and bottom-right entry $p$. No lemmas, no tactics.
why it matters
This normal form is the concrete object that det_starMinor34 evaluates ($\det=2p-3$) and that star_minor_34_eq identifies with the actual submatrix of cmMatrix3 (starSq p) after deleting row 3 and column 4. Those two theorems feed the cofactor pipeline for the star dihedral cosine on the $l=m=1$ slice, which in turn certifies that the signed four-tet deficit equals $4\arcsin(h)$ with $h=q(p)$ and therefore carries the sign of the rational parameter $h$—no arccos numerics required. In the broader Recognition geometry stack this is the first kernel-checked signed Regge deficit on an abstract hinge star, a local building block toward discrete curvature and continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.