deficit_planeWave_contDiffAt
plain-language theorem explainer
Along any plane-wave edge-field family, the Regge deficit on a fixed periodic edge is C^n at amplitude zero for every extended natural n. Gravity analysts cite it when assembling smoothness of the nonlinear Regge action profile. The proof unfolds the deficit as 2π minus a finite sum and applies the already-proved ContDiffAt of each dihedral edge-angle contribution.
Claim. For every polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, wave vector $k\in\mathbb{R}^3$, periodic edge $e$, and order $n\in\mathbb{N}\cup\{\infty\}$, the map $t\mapsto \delta_e\bigl(\text{plane-wave edge field at amplitude }t\bigr)$ is $C^n$ at $t=0$.
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign (Crux-1(c)). At fixed lattice size $N$, one studies the true nonlinear Regge action along plane-wave families of edge lengths, aiming to extract a fixed-$N$ TT Bloch symbol from the second derivative of the action profile at vanishing amplitude.
The edge deficit of a discrete metric is the classical Regge quantity $2\pi$ minus the sum of dihedral angles meeting that edge. Here the metric is the plane-wave edge field: each squared edge length is an affine path through the flat Freudenthal configuration. Upstream Gate-0 facts guarantee that at $t=0$ every squared edge is positive and every cosine of a dihedral angle lies strictly in $(-1,1)$, so local angle maps are smooth at the flat point.
Sibling results already give ContDiffAt of each tetrahedron's dihedral angles and of each edge-angle contribution along the same family. The present statement lifts those local angle facts to the assembled edge deficit.
proof idea
Term-mode, three steps. Unfold the deficit of a field to the constant $2\pi$ minus a finite sum, over cell tetrahedra, of edge-angle contributions. Subtract a constant function (ContDiffAt of any order) from a sum. The sum is ContDiffAt because each summand is, by the sibling lemma that every edge-angle contribution along the plane-wave family is ContDiffAt at $0$ of order $n$. No further analytic estimates are needed.
why it matters
Parent consumer is planeWaveActionProfile_contDiffAt: the plane-wave action profile of the true nonlinear Regge action is ContDiffAt of every finite order at $t=0$. That profile multiplies each edge's square-root hinge factor by its deficit; both factors must be smooth at the flat point. With ContDiffAt of order 2 in hand, the reusable centered-second-difference lemma yields $S''(0)$, and the module closes with existence of the fixed-$N$ TT Bloch symbol.
In the broader Recognition gravity lane this is pure analysis scaffolding for the continuum symbol, not a forcing-chain step (T0–T8). It discharges part (c) of the module's theorem list and keeps the panel-forbidden global $C^4$ route unused.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.