conformalTetSqEdges_contDiff
plain-language theorem explainer
The six conformally scaled squared-edge coordinates of any tetrahedron depend C^n-smoothly on the vertex conformal potentials. Anyone assembling the nonlinear Regge action, its cofactors, or its Hessian cites this to push smoothness through the Cayley-Menger edge chart. The argument is a product reduction: ContDiff on the six-tuple follows componentwise from the already-proved local edge maps.
Claim. For every finite 3D triangulation $K$, every tetrahedron index $\tau$, and every extended natural number $n\in\mathbb{N}_\infty$, the map $\xi\mapsto$ (six conformally scaled squared edges of $\tau$ under $\xi$) is $C^n$ as a map from vertex conformal potentials $\mathbb{R}^{n_V}$ into $\mathbb{R}^6$.
background
The module collects analytic inputs 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. Those requirements are recorded as named configuration facts rather than axioms.
A Triangulation3D is a finite abstract 3-complex with incidence data and a nondegenerate squared-edge tuple on every tetrahedron. Vertex conformal potentials are real assignments on the vertices. The six-tuple of conformally scaled squared edges of a tetrahedron is assembled edgewise from the local conformal squared-edge functions.
Upstream, each individual local conformal squared-edge map is already $C^n$ in the potential (proved by unfolding and fun_prop). The present statement lifts that componentwise fact to the full six-edge chart used by Cayley-Menger polynomials and dihedral cosines.
proof idea
Rewrite the target with the product characterization of ContDiff (smoothness of a map into a finite product is equivalent to smoothness of each coordinate). For each of the six edge indices, invoke the already-established local result that the corresponding conformal squared-edge function is $C^n$ in the vertex potential. No further analytic work is done here; the six-tuple inherits ContDiff from its components.
why it matters
This is the chart-level smoothness lemma that lets cofactors, dihedral cosines, and positivity statements along conformal lines inherit ContDiff or continuity from the edge data. Downstream it is composed into cofactor ContDiff for the conformal chart, into continuity at the zero potential of squared dihedral cosines, and into eventual positivity of the Cayley-Menger cubic along conformal line potentials in the nonlinear Hessian proof.
In the broader Recognition geometry stack this sits under the smoothness inputs for the nonlinear Regge action (as opposed to the exact quadratic truncation used by the closed second-order component theorem). It does not itself force dimension or the eight-tick structure; it supplies the analytic glue so those discrete geometric facts can be differentiated under the conformal ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.