det_starMinor34
plain-language theorem explainer
The determinant of the normal-form (3,4) Cayley-Menger minor for the one-parameter star tetrahedron equals 2p−3. Anyone extracting hinge cofactors on the abstract four-tet star cites this closed form. The proof expands the 4×4 determinant along the first row and finishes by elementary polynomial arithmetic.
Claim. For every real $p$, the determinant of the $4\times 4$ matrix $\begin{pmatrix}0&1&1&1\\1&0&1&1\\1&1&0&1\\1&1&1&p\end{pmatrix}$ equals $2p-3$.
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, with squared-edge data locked to the slice $l=m=1$ and free equatorial edge $p$. Nondegeneracy is the Cayley-Menger sign condition on the 3-volume polynomial.
Cayley-Menger minors supply the cofactors that enter the dihedral cosine formula. The normal-form (3,4) minor is the explicit $4\times 4$ matrix with zeros on the first three diagonal entries, ones off-diagonal in the leading $3\times 3$ block, and bottom-right entry $p$. Its determinant is the algebraic input to the off-diagonal hinge cofactor $C_{34}$.
Upstream, that matrix is defined as the normal form of the star tetrahedron's (3,4) minor; the ambient determinant is the ordinary real matrix determinant (not the Loom $\mathbb{Z}/3$ toy det).
proof idea
Term-mode proof. Unfold the normal-form minor to the concrete $4\times 4$ array. Expand the determinant along the first row via Matrix.det_succ_row_zero. The resulting three $3\times 3$ minors are evaluated by Matrix.det_fin_three after simplifying the finite sums over Fin and the succAbove index map. The leftover polynomial identity is discharged by ring, yielding $2p-3$.
why it matters
This identity is the algebraic core of the off-diagonal hinge cofactor theorem: once the minor determinant is known, a short cofactor-sign computation gives $C_{34}=3-2p$ on the star squared-edge vector. That cofactor, together with the diagonal cofactors, produces the kernel-checked central dihedral cosine $q(p)=(3-2p)/3$ on the $l=m=1$ slice.
In the module's deformation family $p=(3/2)(1-h)$ one has $q=h$, so the signed deficit $2\pi-4\arccos(h)=4\arcsin(h)$ inherits its sign from the rational quantity $h$ with no transcendental evaluation. The result is therefore a load-bearing step toward the first kernel-checked signed Regge deficits on an abstract four-tet star in the repository, with explicit weak-field mesh bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.