cmMinor43Matrix
plain-language theorem explainer
Explicit 4×4 real matrix whose entries are 0, 1, or the six squared tetrahedron edge lengths, equal to the Cayley–Menger minor that deletes row 4 and column 3. Downstream cofactor and dihedral-angle calculus cites it to replace opaque submatrix extractions by a named polynomial object. The body is a single matrix literal.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ matrix $$M_{4,3}(a)=\begin{pmatrix}0&1&1&1\\1&0&a_0&a_2\\1&a_0&0&a_4\\1&a_1&a_3&a_5\end{pmatrix}.$$
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
SqEdges is the type of maps $\mathrm{Fin},6\to\mathbb{R}$: the six squared edge lengths of a tetrahedron. The ambient object is the bordered Cayley–Menger matrix cmMatrix3 a (size $5\times 5$); cofactors of that matrix control volume and dihedral angles.
Indexing convention: the minor labelled $(4,3)$ is obtained by deleting row index 4 and column index 3 (both in $\mathrm{Fin},5$), then reindexing the remaining $4\times 4$ block onto $\mathrm{Fin},4$.
proof idea
Pure definition: a single !![ ... ] matrix literal whose twelve nontrivial entries are either the constant $1$, the constant $0$ on the squared-distance diagonal block, or the six coordinates $a_0,\ldots,a_5$ placed exactly where the Cayley–Menger border and edge-square pattern demand. No lemmas are invoked.
why it matters
Feeds two immediate parents: cmMinor43_submatrix_eq, which proves the literal equals the abstract submatrix of cmMatrix3 a after succAbove 4 / succAbove 3, and det_cmMinor43Matrix, which evaluates the determinant to $-\mathrm{cmCofactor3Poly},4,3,a$ by row expansion and ring normalization.
Those identities let the cofactor polynomial cmCofactor3Poly be treated as an ordinary polynomial in the six edge squares, which is the module’s stated purpose: supply named polynomial partials for downstream dihedral Cayley–Menger calculus. In the broader Recognition geometry stack this is scaffolding for explicit volume and angle formulae on the tetrahedron, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.