canonicalRemainderLineDifferentiabilityNearZero_of_actionLineDifferentiabilityNearZero
plain-language theorem explainer
If the Regge action along every ray through the flat potential is differentiable near the origin, then the same holds for the pair of that action and the canonical quadratic form along the ray. Cited by anyone discharging the remainder second-variation identity in the nonlinear Hessian chain. Proof is a filter lift pairing the hypothesis with global differentiability of the quadratic term.
Claim. Let $K$ be a finite incidence-consistent 3D Regge triangulation. Suppose that for every vertex potential $\xi$, the scalar action along the line $t\mapsto t\xi$ is differentiable at all sufficiently small $t\in\mathbb{R}$. Then for every such $\xi$, both that action and the canonical quadratic form along the same line are differentiable at all sufficiently small $t$.
background
The module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the action 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 Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tets) with nondegenerate squared-edge data on every tetrahedron; incidence consistency is the usual combinatorial well-formedness hypothesis. Vertex potentials $\xi$ are real assignments to vertices; the action and the canonical quadratic are restricted to the real line $t\mapsto t\xi$ through the flat configuration.
The hypothesis target asserts only that the action along each such line is eventually differentiable near $t=0$. The conclusion target strengthens this by also requiring differentiability of the canonical quadratic along the same line. The quadratic piece is already known to be differentiable at every real $t$, independently of any action hypothesis.
proof idea
Term-mode proof, essentially a one-line filter argument. Fix a vertex potential $\xi$. Apply filter_upwards to the neighborhood filter of $0$ using the action-differentiability hypothesis at $\xi$. On that neighborhood, pair the given differentiability of the action with the already-proved global fact that the canonical quadratic along the line is differentiable at every real parameter (the sibling lemma canonicalQuadraticAlongLine_differentiableAt). The resulting conjunction is exactly the remainder-line target.
why it matters
This bridge sits inside the nonlinear Regge Hessian proof interface. It is consumed by canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_actionLineDiffNearZero, which combines the nonlinear directional Hessian theorem with action-line differentiability near zero to conclude that the canonical remainder has vanishing second variation.
In the broader Recognition geometry stack this is bookkeeping on the path from the full nonlinear Regge action down to the canonical incidence Hessian at the flat potential. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure differential calculus on the triangulation action. Closing the remainder second-variation zero statement is the last local gate before the second-variation input package is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.