cmMinor13_submatrix_eq
plain-language theorem explainer
The 4×4 submatrix of the tetrahedral Cayley–Menger matrix obtained by deleting row 1 and column 3 equals the explicit normal-form minor for cofactor (1,3). Anyone rewriting CM cofactors as polynomials in the six squared edges cites this identification. Proof is entrywise exhaustion on Fin 4 × Fin 4 by reflexivity.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $4\times 4$ submatrix of the Cayley–Menger matrix $CM_3(a)$ obtained by deleting row index $1$ and column index $3$ equals the explicit normal-form matrix $\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & a_0 & 0 & a_4 \\ 1 & a_1 & a_3 & a_5 \\ 1 & a_2 & a_4 & 0 \end{pmatrix}$.
background
The ambient module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so that downstream dihedral-angle calculus can quote named polynomial partials rather than opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The $5\times 5$ Cayley–Menger matrix $CM_3(a)$ is the standard bordered matrix of those squared lengths (zeros on the point-block diagonal, ones on the bordering row/column). The target normal form cmMinor13Matrix is the concrete $4\times 4$ matrix obtained by deleting row 1 and column 3 and writing the surviving entries in edge-index order.
This lemma simply certifies that Mathlib’s generic Matrix.submatrix applied to $CM_3(a)$ with the two Fin.succAbove deletions recovers that hand-written normal form.
proof idea
Pointwise matrix extensionality on the two Fin 4 indices, then exhaustive fin_cases on each index. Every one of the sixteen entries reduces by rfl to the corresponding clause of cmMatrix3 versus the literal entries of cmMinor13Matrix. No algebraic identities are required beyond definitional unfolding.
why it matters
Parent consumer is cmCofactor3_13_eq_poly, which rewrites the abstract cofactor $C_{13}(CM_3(a))$ as the named polynomial cmCofactor3Poly 1 3 a by substituting this submatrix equality and then the explicit determinant of the normal form. That step is the cofactor analogue of the derivative expansions in CayleyMengerDerivatives: once every minor is a named polynomial, partials with respect to squared edges become ordinary polynomial calculus, feeding dihedral-angle identities downstream. The result is pure classical geometry scaffolding inside the Recognition geometry layer; it does not itself invoke the forcing chain or $\varphi$-ladder, but it keeps the tetrahedral metric data fully algebraic for later RS mass and angle work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.