canonicalRemainderLineDifferentiability_of_actionLineDifferentiability
plain-language theorem explainer
On a consistent 3D Regge triangulation, action-line differentiability implies the canonical remainder along every vertex-potential line is differentiable. Hessian-identity proofs cite this as the bridge from action smoothness to remainder smoothness. The argument pairs the given action hypothesis with the elementary differentiability of the quadratic line term.
Claim. Let $K$ be a finite 3D Regge triangulation with consistent incidence data. If for every vertex potential direction $\xi$ and every real parameter $t$ the Regge action restricted to the affine line through $\xi$ is differentiable at $t$, then for every such $\xi$ and $t$ both that action line and the canonical quadratic form along the same line are differentiable at $t$.
background
The module isolates the remaining hard step of the nonlinear Regge Hessian program: the second directional derivative of the full nonlinear Regge action at the flat potential must equal the canonical incidence Hessian. Along each affine line of vertex potentials one splits the action into a canonical quadratic piece plus a remainder.
Action-line differentiability is the proposition that the action restricted to every such line is differentiable at every real parameter. The canonical remainder target asks for the same of the action line together with differentiability of the quadratic line. The quadratic piece is elementary; its line-differentiability theorem is already available in-module. Incidence consistency guarantees that the abstract edge and tetrahedron incidence of the triangulation is compatible.
As the remainder-target doc states, this is "the concrete differentiability condition sufficient for the derivative identity," with the smoothness chain responsible only for the action side.
proof idea
Short term proof. Introduce an arbitrary direction $\xi$ and parameter $t$. Form the conjunction of two DifferentiableAt witnesses: the action-line hypothesis applied at $(\xi,t)$, and the already-proved theorem that the canonical quadratic along any line is differentiable at every real point. That conjunction is exactly the remainder-line target.
why it matters
The sole downstream consumer is the theorem that, given the nonlinear directional Hessian theorem and action-line differentiability, the second variation of the canonical remainder vanishes. That zero-remainder second variation is the last algebraic link closing the nonlinear Hessian identity (second directional derivative at flat equals the canonical incidence Hessian).
In the Recognition geometry stack this lives on finite 3D Regge triangulations, matching the forced spatial dimension $D=3$ (forcing chain T8). The declaration itself is pure bookkeeping: once action smoothness is supplied, remainder differentiability is free because the quadratic summand is elementary. It discharges no open analytic gap; it only packages the elementary half of the remainder target so the parent second-variation theorem can take a single action-line hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.