cmMatrix3_entry_contDiff
plain-language theorem explainer
Each entry of the 5×5 Cayley-Menger matrix of a tetrahedron is C^n in the six squared edge lengths, for every extended natural n. Anyone deriving dihedral cosines or volume formulas from the Cayley-Menger determinant would cite this lemma. The proof cases on the five-by-five indices, unfolds the matrix definition, and closes smoothness by fun_prop on constants and coordinate projections.
Claim. For every extended natural number $n$ and all indices $i,j\in\{0,\ldots,4\}$, the real-valued map sending six squared edge lengths $a\in\mathbb{R}^{6}$ to the $(i,j)$-entry of the associated $5\times 5$ Cayley-Menger matrix is of class $C^{n}$.
background
Squared edge lengths of a tetrahedron are packaged as SqEdges, the type $\mathrm{Fin},6\to\mathbb{R}$, ordered as edges $(01),(02),(03),(12),(13),(23)$. The Cayley-Menger matrix is the standard bordered $5\times 5$ array: first row/column is $(0,1,1,1,1)$, the diagonal of the lower $4\times 4$ block is zero, and the off-diagonal entries are exactly those six squared lengths.
This module sits between the explicit tetrahedral Cayley-Menger polynomial and the determinant/cofactor layer required by the dihedral cosine formula. Entrywise smoothness is the elementary analytic input before determinants and minors can be treated as smooth maps of the edge data.
proof idea
Tactic proof by exhaustive case analysis: fin_cases on both indices $i$ and $j$ (twenty-five branches). In each branch simp [cmMatrix3] reduces the entry to either the constant $0$, the constant $1$, or a single coordinate projection of the six-tuple of squared lengths. fun_prop then discharges ContDiff for constants and for the coordinate maps $\mathbb{R}^{6}\to\mathbb{R}$.
why it matters
Entrywise smoothness is the base step for the sibling results that the full Cayley-Menger determinant and every minor are smooth in the six squared lengths. Those facts underwrite the dihedral cosine formula, which is the geometric payload of the module. In the broader Recognition geometry stack the same matrix appears in discrete (Regge-type) treatments of tetrahedral cells; a clean $C^{n}$ statement keeps later zero-mode and hypersurface arguments from carrying ad-hoc regularity hypotheses. No downstream theorem currently records a direct used_by edge, but the sibling contDiff lemmas for det and minors are the intended consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.