hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration
plain-language theorem explainer
On any incidence-consistent 3D triangulation that is flat, both the conformal hinge length and the Regge deficit, restricted to every straight line through the zero potential, are differentiable in a neighborhood of the origin. Anyone assembling the product rule for the first variation of the nonlinear Regge action cites this. The argument lifts two ContDiffAt-⊤ facts at t = 0 to eventual DifferentiableAt via a filter lemma.
Claim. Let $K$ be a 3-dimensional triangulation with consistent incidence, and suppose the configuration is flat. Then for every vertex potential direction $\xi$, there is a neighborhood of $t = 0$ on which, for every edge $e$, both $t \mapsto$ (conformal hinge measure of $e$ along the line $s\mapsto s\xi$) and $t \mapsto$ (Regge deficit angle of $e$ along that line) are differentiable at $t$.
background
The module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative at the flat potential must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
A vertex potential $\xi$ is a real assignment to vertices. The line through the flat (zero) potential in direction $\xi$ is $t \mapsto t\xi$. Along that line the conformal hinge measure of an edge is its conformal edge length $\sqrt{g_e},\exp((\xi_u+\xi_v)/2)$, and the deficit angle is $2\pi$ minus the sum of local dihedral contributions. Flatness of the configuration is the hypothesis that makes the deficit line $C^\infty$ at the origin.
The target proposition packages the finite product-rule hypothesis: near $t=0$, every hinge line and every deficit line is differentiable. Upstream, ContDiffAt $\top$ of the deficit line at zero is already proved under flatness, and the hinge line is smooth independently of flatness.
proof idea
Term-mode proof that unpacks the target. Fix a direction $\xi$ and rewrite the filter quantifier as a universal over edges. For each edge, apply the local lemma that ContDiffAt $\top$ at $0$ implies DifferentiableAt on a neighborhood of $0$, once to the hinge-measure line (using the hinge ContDiffAt fact) and once to the deficit-angle line (using deficitLine_contDiffAt_zero_of_flatConfiguration). Combine the two eventualities with filter_upwards and pair the resulting differentiability witnesses.
why it matters
This is the differentiability half of the product rule for the first derivative of the nonlinear Regge action along lines through the flat point. The sole downstream consumer is actionDerivativeProductRuleNearZero_of_flatConfiguration, which feeds the factor-differentiability lemma into the product-rule target and thereby advances the chain toward the nonlinear directional Hessian equaling the canonical incidence Hessian.
In the Recognition geometry stack this sits inside the discrete curvature / Regge sector that must match continuum second variation at the flat background. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete differential geometry supporting the Hessian identification that later couples to the RS action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.