cmCofactor3_conformal_contDiffAt_zero
plain-language theorem explainer
At the flat (zero) conformal potential on a finite 3D triangulation, every Cayley–Menger cofactor of a tetrahedron’s conformally scaled squared edges is C^n-smooth in the vertex potentials. Anyone building dihedral-angle or Regge-action smoothness at the flat chart cites this. The proof is a one-line specialization of the global ContDiff statement via ContDiff.contDiffAt.
Claim. Let $K$ be a finite 3D triangulation, $\tau$ a tetrahedron of $K$, and $r,c\in\{0,\ldots,4\}$. For every extended order $n\in\mathbb{N}\cup\{\infty\}$, the map sending a vertex conformal potential $\xi$ to the Cayley–Menger cofactor $C_{r,c}$ of the six conformally scaled squared edge lengths of $\tau$ is $C^n$ at the zero potential $\xi\equiv 0$.
background
The module supplies analytic hypotheses for the full nonlinear Regge action: the conformal edge chart must remain in the nondegenerate tetrahedral cone, arccos arguments must stay off $\pm 1$, and the finite action must be smooth at the flat potential. These are recorded as named configuration facts rather than axioms.
A vertex conformal potential on $K$ is a real assignment to each vertex; the zero potential is the flat chart. For each tetrahedron $\tau$, the conformal ansatz produces six squared-edge coordinates. The Cayley–Menger cofactor $C_{r,c}$ is the signed $4\times 4$ minor of the $5\times 5$ Cayley–Menger matrix built from those edges; it enters the classical formulae for tetrahedral volume and dihedral cosines.
The global companion already proves that $\xi\mapsto C_{r,c}(\mathrm{conformal\ edges}(\xi,\tau))$ is $C^n$ everywhere on the potential space, by composing polynomial cofactor smoothness with conformal-edge smoothness.
proof idea
One-line term proof. Apply ContDiff.contDiffAt to the global theorem cmCofactor3_conformal_contDiff, which states full $C^n$ smoothness of the same composite map on all of VertexPotential K. Specializing at zeroPotential K yields the pointwise ContDiffAt claim. No local chart or nondegeneracy hypothesis is needed at this step because the global composite is already smooth everywhere.
why it matters
Dihedral cosine-squared and dihedral denominator smoothness at the flat potential both unfold into rational expressions in Cayley–Menger cofactors of opposite vertex pairs. Those two downstream theorems therefore invoke this pointwise cofactor fact at zero before dividing and composing with further smooth maps.
In the Recognition geometry stack this is part of the analytic input layer for the nonlinear Regge action: once cofactors, denominators, and cosines are $C^n$ at the flat chart, the finite action and its Hessian can be treated as smooth functions of the conformal potentials. The module’s stated goal is exactly that package of smoothness inputs, supporting the closed second-order component theorem’s passage from quadratic truncation to the full nonlinear action. No forcing-chain landmark (T5–T8) is touched directly; the result is pure discrete-geometry analysis feeding the Regge side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.