cmCofactor3_contDiff
plain-language theorem explainer
Every entry of the 5×5 Cayley–Menger cofactor matrix is a C^∞ (in fact ContDiff of every order) function of the six squared edge lengths of a tetrahedron. Anyone proving differentiability of dihedral cosines or first variation of Regge action cites this. The proof is a one-line product of a constant sign with the already-smooth minor.
Claim. For every smoothness order $n \in \mathbb{N}_{\infty}$ and every row–column pair $(r,c) \in \{0,\ldots,4\}^2$, the map sending six squared edge lengths $a \in \mathbb{R}^6$ to the Cayley–Menger cofactor $C_{r,c}(a)$ is $C^n$ as a real-valued function on $\mathbb{R}^6$.
background
The module builds the determinant/cofactor layer that links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5 \times 5$ bordered matrix of squared edge lengths. Rows/columns are indexed $0..4$ with the standard border of ones and zeros on the squared-distance block; the six free entries are the squared lengths $(01),(02),(03),(12),(13),(23)$, packaged as SqEdges := Fin 6 → ℝ.
A cofactor is defined by $C_{r,c}(a) = (-1)^{r+c} M_{r,c}(a)$, where $M_{r,c}$ is the corresponding $4 \times 4$ principal minor of that matrix. The sibling theorem cmMinor3_contDiff already shows every such minor is ContDiff of every order in the six squared lengths (by expanding the determinant and applying fun_prop). The present result lifts that smoothness through the constant sign factor.
proof idea
Unfold the definition of the cofactor: it is the product of the constant sign cmCofactorSign3 r c with the minor cmMinor3 a r c. Apply ContDiff.mul to contDiff_const (smoothness of a constant map) and the upstream lemma cmMinor3_contDiff n r c. No case analysis on indices is needed here; that work lives inside the minor lemma.
why it matters
Dihedral cosines in Regge calculus are rational functions of Cayley–Menger cofactors. Downstream, hasFDerivAt_cmCofactor3 obtains Fréchet derivatives everywhere from this ContDiff statement; dihedralCos3Sq_contDiffAt_nonDegenerate and dihedralDenom3_contDiffAt_nonDegenerate inherit ContDiffAt on nondegenerate tetrahedra; conformal pullbacks (cmCofactor3_conformal_contDiff) and continuity of denominators/cosines in ReggeActionSmoothness compose against it; and flat_nondegeneracy_eventually in the TT derivative gate uses the same smoothness. In the Recognition geometry stack this is the cofactor half of the determinant layer required before first variation of the Regge action can be written rigorously.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.