tetDihedralAngle_planeWave_contDiffAt
plain-language theorem explainer
Along any plane-wave edge-length family, each local dihedral angle of a periodic tetrahedron is infinitely differentiable (every finite order) at vanishing amplitude. Gravity analysts cite this when building the fixed-N TT Bloch symbol from the true nonlinear Regge action. The proof composes the angle map's smoothness at the nondegenerate Freudenthal flat point with the affine squared-edge path through that point.
Claim. For every polarization matrix $E$, wave vector $k$, periodic tetrahedron, edge-slot index $f\in\{0,\ldots,5\}$, and order $n\in\mathbb{N}\cup\{\infty\}$, the map $t\mapsto$ (dihedral angle of slot $f$ on the tetrahedron whose squared edges come from the plane-wave edge field of amplitude $t$) 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. The ambient objects are periodic tetrahedra on an $N^3$ lattice and plane-wave edge fields: amplitude $t$ scales a polarization $E$ against a wave vector $k$, producing a time-dependent assignment of edge lengths.
Squared edge lengths of a tetrahedron are a 6-tuple SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The flat reference is the Freudenthal tetrahedron; at $t=0$ the plane-wave path hits exactly that flat 6-tuple (all six squared edges positive, Cayley–Menger volume factor $cm_3=8>0$, and all six face cosines strictly inside $(-1,1)$). Those nondegeneracy facts are Gate-0 material from ReggeTTDerivativeGate (flatCos_ne_endpoints).
The dihedral-angle map on squared edges is therefore smooth at the flat point. Upstream, the squared-edge path itself is already known to be an affine line $t\mapsto\mathrm{flat}+t\cdot v$ and hence $C^\infty$ in amplitude (planeWaveTetSqEdges_contDiff).
proof idea
Three steps, then composition.
- Invoke
dihedralAngle3Sq_contDiffAt_nonDegenerateat the Freudenthal squared-edge tuple and slot $f$, usingflatCos_ne_endpointsso the cosine is interior to $(-1,1)$: the angle map isContDiffAtof order $n$ there. - Pull
planeWaveTetSqEdges_contDiffdown toContDiffAtat $0$ for the path $t\mapsto$ squared edges of the plane-wave field on the given cell. - Rewrite the evaluation point of the angle map via
planeWaveTetSqEdges_zero(at $t=0$ the path is exactly the Freudenthal tuple), then applyContDiffAt.comp. A finalcongr_of_eventuallyEqwith a trivialrflidentifies the composite with the stated dihedral-angle-of-field map.
why it matters
Item (b) in the module's theorem list: local dihedral angles along the plane-wave family are smooth at vanishing amplitude. The sole direct consumer is edgeAngleContribution_planeWave_contDiffAt, which lifts the same smoothness to the per-tetrahedron contribution in an edge's angle sum (finite case split on slot lookup; none branch constant zero).
That feeds the action-profile smoothness theorem (c), then the reusable centered-second-difference lemma (d), and finally the fixed-$N$ TT Bloch symbol existence statement (e): $S''(0)$ of the true nonlinear Regge action is well-defined and equals the continuum second variation. Without angle smoothness at the flat point, the Schläfli two-jet bookkeeping cannot start. The argument stays local to Gate A1 and deliberately avoids the panel-forbidden global $C^4$ continuum-limit route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.