cmMinor3_contDiff
plain-language theorem explainer
Every 4×4 minor of the tetrahedral Cayley-Menger matrix is a C^n map of the six squared edge lengths, for any extended natural n (including C^∞). Needed by anyone building dihedral cosines or volume formulas from CM cofactors. Proof is exhaustive casework on the deleted row and column, then automatic smoothness of the resulting polynomial expressions.
Claim. For every extended natural number $n$ and every pair of indices $r,c \in \{0,1,2,3,4\}$, the map sending six squared edge lengths $a \in \mathbb{R}^6$ to the determinant of the $4 \times 4$ submatrix of the Cayley-Menger matrix obtained by deleting row $r$ and column $c$ is $C^n$ as a real-valued function of $a$.
background
The module builds the determinant and cofactor layer for a tetrahedron, linking the explicit Cayley-Menger polynomial cm3 to the genuine $5 \times 5$ matrix whose entries are $0$, $1$, or squared edge lengths $a_0,\ldots,a_5$ (edges $01,02,03,12,13,23$). That matrix is the function cmMatrix3 of SqEdges := Fin 6 → ℝ.
A minor cmMinor3 a r c is the determinant of the submatrix after deleting row $r$ and column $c$ via Fin.succAbove. These minors feed the cofactors used in the classical dihedral-cosine formula from Cayley-Menger data.
Smoothness is stated in Mathlib's ContDiff ℝ n for arbitrary $n : \mathbb{N}_\infty$, so the same statement covers finite differentiability and $C^\infty$.
proof idea
Unfold the minor and the matrix definition. Case-split on the five choices of deleted row and the five choices of deleted column (fin_cases). On each of the 25 branches, simplify the submatrix determinant with Matrix.det_succ_row_zero, finite sums, and Fin.succAbove, reducing to an explicit polynomial (sums and products of coordinates of $a$ and constants). Discharge smoothness of that expression by fun_prop, which closes under the ring operations and projections on SqEdges.
why it matters
This is the smoothness engine for the cofactor layer. The immediate parent is cmCofactor3_contDiff, which multiplies the minor by the constant sign $(-1)^{r+c}$ and inherits $C^n$ in one line. Together they underwrite any later argument that dihedral cosines, or other rational functions of CM cofactors, remain smooth (or analytic) away from degeneracy loci.
In the broader Recognition geometry stack, the tetrahedral CM determinant is the volume/defect carrier that sits under discrete curvature and edge-length dynamics on the phi-ladder. Establishing that minors are smooth is bookkeeping, but without it the cofactor and cosine pipelines cannot quote differentiability. No forcing-chain landmark (T5–T8) is proved here; the result is pure classical geometry infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.