canonicalRemainderDerivativeIdentity_of_lineDifferentiability
plain-language theorem explainer
On any incidence-consistent 3D triangulation, pointwise differentiability of the Regge action and of the canonical quadratic form along every conformal line implies that the first derivative of the canonical remainder equals the difference of those two derivatives. Second-variation arguments cite this as the calculus glue between the action split and HasSecondDerivAt. The proof rewrites the remainder as action minus quadratic, then applies the product rule for derivatives of differences.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every vertex potential $\xi$ and every real $t$, both the Regge action restricted to the conformal line through $\xi$ and the canonical quadratic form along that line are differentiable at $t$. Then for every $\xi$, $$\partial_t\,R_K(\xi;t)=\partial_t\,S_K(\xi;t)-\partial_t\,Q_K(\xi;t),$$ where $R_K$ is the canonical remainder, $S_K$ the action along the line, and $Q_K$ the canonical quadratic term.
background
This module isolates the hard calculus step for the full nonlinear Regge action: the second directional derivative at the flat potential must match the canonical incidence Hessian. The endpoint is not a new geometric assumption; once the chain-rule calculation is in place, the existing second-variation input package follows at once.
The concrete Regge action under the vertex-conformal ansatz is a sum over edges of hinge measure times deficit angle. Along a conformal line $t\mapsto$ linePotential$(K,\xi,t)$, one splits the action into a canonical quadratic piece (half the Hessian quadratic form of the incidence Hessian) plus a remainder. The theorem canonicalRemainderAlongLine_eq_action_sub_quadratic records the explicit subtraction form of that remainder (action minus the flat-potential constant minus the quadratic).
Because HasSecondDerivAt is phrased through deriv, one needs a first-derivative identity: the derivative of the remainder equals the difference of the action and quadratic derivatives. The hypothesis packages exactly the pointwise differentiability of those two summands along every line; the quadratic line is elementary, so the smoothness chain only has to deliver differentiability of the action line.
proof idea
Fix a vertex potential $\xi$ and apply functional extensionality in the line parameter $t$. Rewrite the remainder via canonicalRemainderAlongLine_eq_action_sub_quadratic. From the differentiability hypothesis extract differentiability of the action line and of the quadratic line at $t$. Subtracting the constant flat-potential action value preserves differentiability. Apply deriv_sub to the difference of (action minus constant) and the quadratic, then simplify with sub_eq_add_neg and deriv_sub_const to drop the constant. The resulting pointwise identity is exactly the derivative-identity target.
why it matters
This is pure calculus glue, not the geometric Cayley-Menger/arccos/hinge expansion. It sits between the explicit action-quadratic split and the remainder second-variation target that the nonlinear Hessian program must close.
The sole downstream consumer is canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_lineDiff, which combines the nonlinear directional Hessian theorem with this line-differentiability package to conclude that the second variation of the canonical remainder vanishes. That vanishing is the remaining hard step toward matching the second directional derivative of the full nonlinear Regge action at the flat potential with the canonical incidence Hessian, and thereby discharging the second-variation input interface for the geometry layer.
In the broader Recognition geometry stack this is scaffolding closure inside the Regge sector, not a forcing-chain landmark (T5-T8). It keeps the nonlinear Hessian proof modular: smoothness supplies differentiability, this lemma turns it into a deriv identity, and the parent theorem finishes the second-variation claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.