cmCofactor3_conformal_contDiff
plain-language theorem explainer
The Cayley-Menger cofactor of a tetrahedron, read on conformal squared edges from a vertex potential, is C^n-smooth for every extended natural n. Anyone establishing smoothness of the nonlinear Regge action near flat potentials cites this. The proof is a one-line ContDiff composition of the cofactor map with the conformal edge chart.
Claim. For any 3D triangulation $K$, tetrahedron $\tau$, indices $r,c\in\{0,\ldots,4\}$, and order $n\in\mathbb{N}\cup\{\infty\}$, the map sending a vertex potential $\xi$ to the Cayley-Menger cofactor $C_{r,c}$ of the conformal squared edge lengths of $\tau$ is $C^n$ as a real-valued map on the space of vertex potentials.
background
This module packages analytic inputs for the full nonlinear Regge action. The closed second-order component theorem uses an exact quadratic truncation; the nonlinear action needs the conformal edge chart to stay in the nondegenerate tetrahedral cone, arccos arguments away from $\pm 1$, and the finite Regge action smooth at the flat potential.
The Cayley-Menger cofactor $C_{r,c}$ is the signed $4\times 4$ minor of the $5\times 5$ Cayley-Menger matrix on squared edge lengths; it feeds volume and dihedral formulas. Conformal squared edges arise by pushing a vertex potential through the triangulation's edge chart, so the composite is the natural potential-dependent cofactor.
Upstream, the cofactor is already $C^n$ in the six squared-edge coordinates, and the conformal tetrahedron edge map is already $C^n$ in the potential.
proof idea
Term-mode one-liner: ContDiff.comp of two prior results. The outer map is the Cayley-Menger cofactor as a function of squared edges (ContDiff by cmCofactor3_contDiff). The inner map is the conformal squared-edge chart of tetrahedron $\tau$ as a function of the vertex potential (ContDiff by conformalTetSqEdges_contDiff). No algebraic expansion or case split.
why it matters
Immediate parent is cmCofactor3_conformal_contDiffAt_zero, which specializes the global ContDiff statement to ContDiffAt at the zero (flat) potential via contDiffAt. That local fact is part of the named analytic configuration this module exposes for the nonlinear Regge action at flat configurations, rather than hiding smoothness as an axiom.
In the geometry stack, discrete curvature built from Cayley-Menger data must be smooth enough for continuum limits and second-variation analysis around flat space. Cofactor smoothness is a necessary intermediate before dihedral cosines, volumes, and the full action can be treated as smooth functions of the potential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.