canonicalRemainderLine_hasDerivAt_zero_of_remainderFirstVar
plain-language theorem explainer
Along any ray t ↦ tξ in vertex-potential space, the Regge-action remainder has ordinary derivative zero at t = 0, once the free-space first variation of that remainder vanishes at the zero potential. Anyone building the cubic Taylor jet of the remainder on a flat triangulation cites this. The argument is a chain-rule composition: ContDiff of the remainder at zero yields a zero Fréchet derivative, which kills the directional derivative of the linear path.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation in a flat configuration, and let $R$ be the Regge-action remainder relative to the canonical Hessian. Assume the Fréchet derivative of $R$ at the zero vertex potential is the zero map. Then for every vertex potential $\xi$, the scalar path $t \mapsto R(t\xi)$ satisfies $\frac{d}{dt}\big|_{t=0} R(t\xi) = 0$.
background
This module supplies the final local analytic Taylor bound for the nonlinear Regge remainder after the Hessian has already been identified. The ambient space is the finite-dimensional vector space of vertex potentials on a 3D triangulation $K$; the zero potential is the origin of that space. The remainder $R$ is the Regge action minus its quadratic Hessian piece (the canonical Regge Hessian), so $R$ is the higher-order defect that must be controlled for a cubic Taylor estimate.
A flat configuration means the discrete geometry sits at a critical point where curvature defects vanish in the usual Regge sense. The first-variation input package asserts precisely that $\mathrm{D}R(0)=0$ as a continuous linear map on vertex potentials. The line potential $t\mapsto t\xi$ is the straight ray through $\xi$; restricting $R$ to that ray produces a scalar function of one real variable whose jet at $0$ is what the cubic bound needs.
Upstream, smoothness of $R$ at the origin on a flat configuration is already available (canonicalRemainder_contDiffAt_zero_of_flatConfiguration), and the first-variation vanishing is packaged as a named hypothesis rather than re-proved here.
proof idea
Start from ContDiffAt of the free-space remainder at the zero potential (flat-configuration smoothness). ContDiff implies DifferentiableAt, hence HasFDerivAt with derivative equal to the Fréchet derivative fderiv R 0. The first-variation input rewrites that Fréchet derivative as the zero map. Identify the zero potential with the line potential at $t=0$. The inner path $t\mapsto t\xi$ has ordinary derivative $\xi$ at $0$ (hasDerivAt_linePotential). Compose HasFDerivAt of $R$ with HasDerivAt of the line: the chain rule yields HasDerivAt of $R\circ\mathrm{line}$ with derivative $(\mathrm{D}R(0))(\xi)$. Because $\mathrm{D}R(0)=0$, that directional value is $0$, and simpa closes.
why it matters
This is the first-order jet step on rays needed before any cubic remainder estimate. The sole downstream consumer is iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs, which lifts the ordinary derivative statement to iteratedDerivWithin 1 of the line-restricted remainder on the unit interval, again equal to zero. That iterated-derivative vanishing is an input to the module's cubic Taylor target for the nonlinear Regge remainder.
In the broader Recognition geometry stack, controlling the cubic defect of the Regge action on flat 3D triangulations is the discrete-curvature counterpart of the continuum Einstein-Hilbert expansion; the module isolates exactly that analytic bound once the Hessian identification is finished. The result does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law, but it is part of the geometric scaffolding that later feeds continuum limits and curvature matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.