edgeAngleContribution_planeWave_contDiffAt
plain-language theorem explainer
Along any plane-wave edge-length family, the contribution of one tetrahedron to a given edge's angle sum is C^n-smooth at amplitude zero, for every extended natural n. Gravity analysts cite this when assembling edge deficits and the Regge action profile. The proof is a two-branch case split on whether the edge sits in the tetrahedron: constant zero, or the already-proved dihedral-angle smoothness lemma.
Claim. Fix a polarization matrix $E$, wave vector $k$, periodic edge $e$, and periodic tetrahedron $\tau$. For every extended order $n\in\mathbb{N}_\infty$, the map $t\mapsto$ (angle contribution of $\tau$ to edge $e$ under 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 program. The goal is local existence of the fixed-$N$ TT Bloch symbol: the second derivative at zero of the true nonlinear Regge action along plane-wave deformations of edge lengths on the periodic Freudenthal lattice.
A plane-wave edge field deforms squared edge lengths affinely through the flat Freudenthal tuple. At amplitude zero every tetrahedron is nondegenerate (Gate-0 facts: positive squared edges, cosines strictly inside $(-1,1)$), so each local dihedral angle is already known to be $C^n$ at zero by composition of the angle map with that affine path.
The edge-angle contribution of a tetrahedron to a hinge is either the corresponding dihedral angle (when a canonical slot lookup finds the edge inside the tet) or identically zero (when the edge is absent). Edge deficit is then $2\pi$ minus the sum of those contributions over incident tets.
proof idea
Unfold the contribution definition and case-split on the optional canonical edge-slot lookup for $(e,\tau)$.
- If the lookup returns none, the contribution is the constant zero function; apply
contDiffAt_const. - If it returns some face index $f$, the contribution is exactly the plane-wave dihedral angle of $\tau$ at face $f$; invoke the sibling lemma
tetDihedralAngle_planeWave_contDiffAtand simplify.
No further analytic work: smoothness is inherited from the constant map or from the already-established dihedral smoothness at the flat point.
why it matters
This is the per-tetrahedron brick in the smoothness tower for the Regge action profile. Downstream, deficit_planeWave_contDiffAt subtracts a finite sum of these contributions from the constant $2\pi$, yielding $C^n$ edge deficits at amplitude zero. Those deficits feed planeWaveActionProfile_contDiffAt, which establishes that the true nonlinear Regge action $S(t)$ is $C^n$ at $t=0$ for every finite $n$.
That ContDiffAt hypothesis is exactly what the reusable centered-second-difference lemma needs to identify $S''(0)$ without a global $C^4$ assumption (forbidden for this family). The endpoint is planeWave_TTBlochSymbolIs_secondVariation: existence of the fixed-$N$ TT Bloch symbol as $(2/N^3)S''(0)$. In the QG campaign this closes Crux-1(c) Gate A1 toward the continuum TT symbol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.