CanonicalRemainderLineDifferentiabilityNearZeroTarget
plain-language theorem explainer
For every conformal vertex potential on an incidence-consistent 3D triangulation, both the nonlinear Regge action and the canonical quadratic term are differentiable along the conformal line in some neighborhood of the flat point t=0. Authors of the nonlinear directional Hessian cite this Prop as the line-regularity hypothesis on the action/quadratic split. It is a pure interface definition (no proof obligation).
Claim. Let $K$ be a finite 3D Regge triangulation with consistent incidence data. The named target asserts: for every vertex conformal potential $\xi$, there is a neighborhood of $t=0$ such that, at every $t$ in that neighborhood, both the nonlinear Regge action restricted to the conformal line through the flat potential in direction $\xi$, and the canonical quadratic form of the incidence Hessian along that same line, are differentiable.
background
The module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that chain-rule calculation is supplied, the existing second-variation input package follows immediately.
A Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tetrahedra) with nondegenerate squared-edge data. Incidence consistency is the standing combinatorial hypothesis. Vertex potentials are real assignments on vertices; the zero assignment is the flat background. The conformal line through the flat potential in direction $\xi$ is the one-parameter family $t\mapsto t\xi$.
actionAlongLine evaluates the full nonlinear Regge action on that line. canonicalQuadraticAlongLine is half the Hessian quadratic form of the canonical incidence Hessian on the same line potential. Differentiability of both near $t=0$ is the minimal first-order regularity needed to differentiate the remainder (action minus quadratic).
proof idea
No proof body: the declaration is a Prop-valued definition. It packages the filter statement that for every vertex potential $\xi$, eventually in the neighborhood filter of $0\in\mathbb{R}$, both the action-along-line map and the canonical-quadratic-along-line map are differentiable at $t$. Downstream lemmas either derive this interface from action-line differentiability (the quadratic term is smooth, so the conjunction reduces) or consume it via filter_upwards to obtain derivative identities for the remainder.
why it matters
This target is a regularity gate in the nonlinear Regge Hessian proof interface. The module endpoint is equality of the second directional derivative of the nonlinear action at the flat potential with the canonical incidence Hessian.
Two immediate parents use it. From action-line differentiability near zero one obtains this remainder-line differentiability target. Given the target, the canonical remainder derivative identity near zero follows by filtering the conjunction and differentiating action minus quadratic. Those steps feed the first-order tangency and linearization path toward the nonlinear directional Hessian theorem, which is the exact endpoint of the second chain-rule calculation for Regge second variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.