planeWaveEdgeValue_contDiff
plain-language theorem explainer
Along the fixed-N plane-wave family, each periodic edge's squared-length field is C^n in the amplitude for every extended order n (in fact globally affine). Gravity analysts cite it when building smoothness of square-root hinges and the nonlinear Regge action profile at the flat background. The proof rewrites the field as constant plus t times a t-independent coefficient, then applies the standard ContDiff rules for constants and the identity.
Claim. Fix a polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, a wave covector $k$, a periodic lattice edge $e$, and an order $n\in\mathbb{N}\cup\{\infty\}$. The real map $t\mapsto$ (squared edge length of $e$ in the plane-wave deformation of amplitude $t$) is $C^n$ on $\mathbb{R}$.
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 profile along plane-wave deformations is smooth enough at the flat background that a fixed-$N$ TT Bloch symbol exists as the second derivative at amplitude zero.
The plane-wave edge field assigns to each amplitude $t$ the squared length of a chosen periodic edge after a monochromatic displacement with polarization $E$ and wave vector $k$. By construction it is an affine path through the flat Freudenthal background: flat squared displacement plus $t$ times a polarization-and-phase coefficient. Sibling results already record that every tetrahedron's six squared edges form such an affine path, and that at $t=0$ one recovers the nondegenerate flat tuple (Cayley–Menger $cm3=8>0$, cosines strictly inside $(-1,1)$).
Mathlib's ContDiff predicate is the working notion of $C^n$ (including $C^\infty$). The present lemma is the single-edge building block before composing with square roots, dihedral angles, and the full action sum.
proof idea
Unfold the plane-wave edge field and simplify: after funext and ring, the map equals
$t \mapsto d_0 + t\cdot c$,
where $d_0$ is the flat periodic squared displacement of the edge and $c$ is the product of a polarization edge coefficient with the cosine of the edge-midpoint phase (both independent of $t$).
Rewrite the goal along this equality, then apply the Mathlib calculus facts that constants are $C^n$, the identity is $C^n$, and $C^n$ is closed under multiplication and addition: contDiff_const.add (contDiff_id.mul contDiff_const). No analysis beyond affine structure is required.
why it matters
Gate A1 needs every local ingredient of the Regge action to be $C^n$ (or at least ContDiffAt at $t=0$) so the centered second difference converges to $S''(0)$ and the fixed-$N$ TT Bloch symbol can be identified with that second jet. This lemma supplies the edge-level $C^n$ fact.
It is consumed immediately by sqrtEdge_planeWave_contDiffAt, which composes with real square root after checking the flat edge value lies in ${1,2,3}>0$, and by the neighborhood positivity argument in eventually_pathGoodAt (path goodness near the flat amplitude). Those feed dihedral-angle smoothness, deficit smoothness, and finally planeWaveActionProfile_contDiffAt and the Bloch-symbol existence theorem in the same campaign.
Within Recognition Science gravity, this is discrete-geometry analysis supporting the continuum TT symbol, not a forcing-chain (T0–T8) step; it closes a smoothness gate rather than an open physical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.