actionAlongLine_contDiffAt_zero_of_flatConfiguration
plain-language theorem explainer
Along any ray through a vertex potential, the concrete 3D Regge action is C^∞ at the origin whenever the background is a flat configuration. Geometric analysts of discrete gravity cite this to justify unrestricted differentiation of the action along conformal lines. The proof is a short chain-rule composition: infinite smoothness of the line embedding at 0, plus flat-configuration smoothness of the action at the zero potential.
Claim. Let $K$ be an incidence-consistent 3D triangulation and suppose the background is a flat configuration. For every vertex potential $\xi$, the real function $t \mapsto S_K(\ell_\xi(t))$ obtained by restricting the concrete Regge action to the line of potentials through $\xi$ is $C^\infty$ at $t = 0$.
background
The module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The concrete action is the sum over edges of hinge measure times deficit angle under the vertex-conformal ansatz. A vertex potential $\xi$ parametrizes conformal edge lengths; the line potential embeds a real parameter $t$ into potential space so that $t=0$ is the zero (flat) potential. Flat configurations supply, among other things, infinite differentiability of the action at that zero potential.
The local objects needed here are therefore: the line embedding of potentials, the concrete Regge action as a function of potentials, and the flat-configuration hypothesis that unlocks $C^\infty$ of the action at the origin of potential space.
proof idea
Obtain $C^\infty$ of the line-potential map at $t=0$ from the existing line-potential smoothness lemma. Separately, flatness gives $C^\infty$ of the Regge action at the image point linePotential ξ 0; a simp with the zero-line identity rewrites that point as the zero potential. Unfold the action-along-line definition (composition of action with the line map) and apply ContDiffAt.comp. A final simp on function composition finishes.
why it matters
This is a local analytic lemma inside the nonlinear Regge Hessian proof interface. Its sole downstream consumer is the near-zero line differentiability target: for every potential, the action along that line is eventually differentiable near the origin, obtained by specializing infinite smoothness at zero to ordinary differentiability in a neighborhood.
That target is part of the chain that forces the second directional derivative of the nonlinear action at the flat point to equal the canonical incidence Hessian. In the broader Recognition geometry stack this closes a calculus gap on the discrete action before second-variation identities are fed into continuum or forcing arguments. It does not itself invoke the T0–T8 forcing chain, RCL, or the mass ladder; it is pure discrete-geometric analysis supporting those later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.