planeWaveActionProfile_contDiffAt
plain-language theorem explainer
Along any plane-wave family of edge lengths on the fixed-N periodic Freudenthal torus, the true nonlinear Regge action profile S(t) is C^n at t = 0 for every finite order n. Gravity analysts cite this to justify taking the second derivative S''(0) that defines the fixed-N TT Bloch symbol. The proof rewrites S as a finite sum of √edge × deficit terms and multiplies the two already-proved ContDiffAt lemmas for those factors.
Claim. For every polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, every wave vector $k\in\mathbb{R}^3$, and every finite smoothness order $n$, the plane-wave action profile $S(t)=\sum_e\sqrt{\ell_e(t)}\,\delta_e(t)$ of the true nonlinear Regge action is $C^n$ at $t=0$.
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the ReggeTTContinuumSymbol program. At fixed lattice side $N$, one probes the true nonlinear Regge action along plane-wave families of squared edge lengths on the periodic Freudenthal torus. Edges are the positive-displacement PeriodicEdge cells (base vertex plus one of seven cube displacements).
The action profile $S(t)$ is the sum, over all such edges, of $\sqrt{\ell_e(t)}$ times the angle deficit at that edge computed from the plane-wave edge field. Upstream Gate-0 facts guarantee that at $t=0$ every flat edge length is at least $1>0$ and every dihedral cosine lies strictly in $(-1,1)$, so square roots and arccosines are smooth at the base point.
Sibling lemmas already establish ContDiffAt of the squared-edge affine paths, of each local dihedral angle, of each edge's deficit contribution, and of each $\sqrt{\ell_e}$ factor. The present result assembles those into ContDiffAt of the full action profile.
proof idea
Unfold the definition: after funext, the action profile equals the finite sum over PeriodicEdge N N N of $\sqrt{\texttt{planeWaveEdgeField},t,e}$ times $\texttt{deficitOfField}$ of that same field. Rewrite with that equality, then apply ContDiffAt.sum. Each summand is the product of two ContDiffAt maps already proved: sqrtEdge_planeWave_contDiffAt and deficit_planeWave_contDiffAt. ContDiffAt is closed under multiplication, so the product (and hence the sum) is ContDiffAt at $0$ of every finite order $n$.
why it matters
This is clause (c) of the module's theorem list and the last smoothness input needed before the reusable centered-second-difference bridge (d). Downstream, planeWave_TTBlochSymbolIs_secondVariation quotes it to identify the fixed-$N$ TT Bloch symbol with $(2/N^3)\cdot S''(0)$: the preflight second-difference quotient converges to the iterated second derivative precisely because $S$ is $C^2$ at $0$.
In the broader QG campaign this closes the local analytic gate that lets the continuum TT symbol be defined from the true nonlinear Regge action rather than a linearized surrogate. It does not yet evaluate $S''(0)$; it only guarantees the derivative exists so the existence theorem can name it. Framework-wise it sits in the gravity analysis stack that eventually feeds continuum limits on the eight-tick / $D=3$ lattice geometry forced upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.