localDihedralAngleLineDifferentiabilityNearZero_of_flatConfiguration
plain-language theorem explainer
Under a flat configuration on an incidence-consistent 3D triangulation, every local conformal dihedral angle along a line through the flat potential is differentiable in a neighborhood of the origin. Analysts of the nonlinear Regge Hessian cite this to justify termwise differentiation of deficit angles. The proof downgrades already-proved C^∞ smoothness at zero to eventual differentiability via a neighborhood filter lemma.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation that admits a flat configuration. Then for every vertex potential $\xi$, there exists a neighborhood of $t=0$ such that for every tetrahedron $\tau$ and every local edge slot $f\in\{0,\ldots,5\}$, the map $s\mapsto\theta_{\tau,f}(s\cdot\xi)$ is differentiable at $s=t$, where $\theta_{\tau,f}$ is the dihedral angle of tetrahedron $\tau$ at slot $f$ under the conformal edge-length ansatz.
background
The module isolates the hard analytic step in the nonlinear Regge Hessian: the second directional derivative of the Regge action at the flat potential must match the canonical incidence Hessian. Local building blocks are conformal dihedral angles computed from Cayley-Menger cofactors on squared edge lengths, and the line potential $t\mapsto t\cdot\xi$ through the flat vertex potential in direction $\xi$.
The target proposition asserts that, near $t=0$, each local dihedral angle along that line is differentiable. That is the analytic input needed to expand the derivative of a global deficit angle as a finite sum of derivatives of its incident local dihedral angles.
Upstream, $C^\infty$ smoothness of each conformal dihedral angle along the line at the flat point is already available under the flat-configuration hypothesis. A general filter lemma then converts ContDiffAt of order $\top$ at a point into DifferentiableAt on a neighborhood.
proof idea
Term-mode reduction after two filter rewrites. Fix the direction $\xi$, then rewrite the nested $\forall^\infty$ quantifiers over tetrahedra and edge slots via Filter.eventually_all. For each fixed tetrahedron $\tau$ and slot $f$, apply differentiableAt_eventually_of_contDiffAt_top to the real map $t\mapsto$ conformal dihedral angle of $\tau$ at $f$ along the line potential in direction $\xi$. The ContDiffAt hypothesis at $0$ is supplied by tetDihedralAngleUnderConformal_line_contDiffAt_zero_of_flatConfiguration under incidence consistency and flatness. No new geometric calculation occurs here.
why it matters
This closes the local differentiability interface required before deficit angles can be differentiated termwise near the flat point. Downstream it is consumed by canonicalPeriodicConformalSchlaefliNearZeroExpansionTarget on the canonical periodic Freudenthal torus: that result differentiates the finite deficit-angle sum near zero and reindexes global edge incidences into local tetrahedral slots.
In the module's own framing, the endpoint is equality of the second directional derivative of the nonlinear Regge action with the canonical incidence Hessian; once the chain-rule calculation is complete, ReggeActionSecondVariationInput follows. The present lemma is the analytic gate for that expansion, not a new physical assumption. It sits in the geometry layer that feeds discrete gravity instances (six-tet cubic Dirichlet), not in the T0-T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.