planeWaveTetSqEdges_contDiff
plain-language theorem explainer
Along any plane-wave edge field of amplitude t, each periodic tetrahedron's local squared-edge 6-tuple is C^n in t for every order n (in fact the path is affine). Cited by anyone composing dihedral angles or the nonlinear Regge action along the family, and by the fixed-N TT Bloch symbol existence argument. Proof rewrites the path as flat Freudenthal edges plus t times a fixed velocity, then applies product ContDiff lemmas.
Claim. For every polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, wave covector $k$, periodic tetrahedron on the $N$-torus, and smoothness order $n\in\mathbb{N}\cup\{\infty\}$, the map $t\mapsto$ (squared-edge 6-tuple of that tetrahedron under the plane-wave edge field of amplitude $t$) is $C^n$ as a map $\mathbb{R}\to\mathbb{R}^6$.
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program: prove that the true nonlinear Regge action along plane-wave families is smooth enough at the flat background that a fixed-$N$ TT Bloch symbol exists as $S''(0)$.
The ambient geometry is the periodic Freudenthal triangulation of the $N$-torus. Every tetrahedron carries a local squared-edge 6-tuple; on the flat background that tuple is exactly the Freudenthal values (three unit steps, two face diagonals, one body diagonal: $1,2,3,1,2,\ldots$). A plane-wave edge field deforms every edge length by an amplitude parameter $t$ with polarization $E$ and wave vector $k$.
The companion identity planeWaveTetSqEdges_apply states that the deformed 6-tuple is affine in $t$: flat Freudenthal edges plus $t$ times a fixed velocity vector assembled from $E$ and $k$. Gate-0 nondegeneracy (positive edges, cosines strictly inside $(-1,1)$) lives upstream in the derivative-gate module and is not re-proved here.
proof idea
One algebraic rewrite, then standard ContDiff combinators. First, functional extensionality plus the sibling identity planeWaveTetSqEdges_apply identifies the path with
$t\mapsto f\mapsto \mathrm{freudenthalTetSqEdges}(f)+t\cdot v(f)$,
where $v$ is the named plane-wave tet velocity. After rewriting, contDiff_pi reduces to each of the six scalar components. Each component is constant plus identity times constant, hence $C^n$ for every $n$ by contDiff_const and contDiff_id.mul.
why it matters
Item (a) of the module's theorem list: smoothness of the local squared-edge path. Downstream, tetDihedralAngle_planeWave_contDiffAt composes the dihedral-angle map (ContDiffAt at the nondegenerate flat Freudenthal point) with this affine path to get amplitude smoothness of every local angle at $t=0$. That feeds edge-angle contributions, deficit smoothness, and ultimately planeWaveActionProfile_contDiffAt: the true nonlinear Regge action profile $S(t)$ is ContDiffAt every finite order at the flat point.
Separately, eventually_pathGoodAt in the flat second-variation module uses continuity of these affine edge paths plus the derivative gate's flat neighborhood nondegeneracy to keep all edges positive near $t=0$. Together these close Gate A1 toward planeWave_TTBlochSymbolIs_secondVariation: the fixed-$N$ TT Bloch symbol exists as $(2/N^3)S''(0)$. No continuum $N\to\infty$ limit is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.