contDiff_eval
plain-language theorem explainer
Every coordinate projection from the six squared edge lengths of a tetrahedron onto ℝ is C^n for arbitrary extended order n. Anyone assembling smoothness of the explicit Cayley-Menger volume polynomial cites this lemma. The argument is a one-line appeal to Mathlib's continuous-linear projection smoothness.
Claim. For every extended natural number $n$ and every index $i\in\{0,\ldots,5\}$, the map $a\mapsto a_i$ from the space of squared tetrahedron edge lengths $\mathbb{R}^6$ to $\mathbb{R}$ is of class $C^n$.
background
The ambient type is squared edge lengths of a tetrahedron: six real coordinates indexed by Fin 6, with the classical edge pairing (0,1), (0,2), (0,3), (1,2), (1,3), (2,3). Opposite-edge pairs are (0,5), (1,4), (2,3). The module writes the classical Cayley-Menger determinant for n=3 as an explicit cubic polynomial CM_3 in those six squared lengths, so that 288 V^2 = CM_3(a).
Smoothness of CM_3 is obtained by composing ContDiff combinators (add, sub, mul) on the coordinate functions. ContDiff ℝ n f means f is C^n as a map of real Banach spaces; here the domain is the product space Fin 6 → ℝ with the product topology.
This private lemma isolates the base case: each pure coordinate extraction is already C^n, so the polynomial combinators can fire without further analysis.
proof idea
One-line term proof. Identify the coordinate map a ↦ a i with the continuous linear projection ContinuousLinearMap.proj i on the product module Fin 6 → ℝ, then invoke the Mathlib fact that every continuous linear map is ContDiff of every order. No induction or explicit derivative computation is required.
why it matters
Direct feedstock for cm3_contDiff, which states that the Cayley-Menger polynomial itself is C^n for every n, built from ContDiff.add, ContDiff.sub, and ContDiff.mul on these six projections. That smoothness is the analytic prerequisite for differentiating CM_3 with respect to squared edge lengths, hence for forming the Regge second-variation matrix M_ij and comparing it componentwise to face areas.
The module exists to close Philip's deeper concern: genuine Regge Hessian data must match area(f_ij) entry by entry, not merely in a scalar identity. Establishing ContDiff of the coordinate scaffolding is the first algebraic step before any derivative of dihedral angles or volumes is taken. No T0-T8 forcing step is invoked here; the result is pure real analysis supporting the geometric side of the Recognition program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.