canonicalRemainderLineThirdDerivBound_of_flatConfiguration
plain-language theorem explainer
On any incidence-consistent 3D triangulation that is flat, the third derivative of the canonical Regge remainder along the line potential is O(‖ξ‖³) near the origin. Analysts of the nonlinear Regge action cite this to close the cubic Taylor remainder estimate. The proof is a two-premise term application of the chain-rule-plus-local-norm assembly lemma, both premises already discharged from flatness.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation that admits a flat configuration. Then there exist $r>0$ and $M\ge 0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$ and every $t\in[0,1]$, the absolute value of the third iterated derivative (in the line parameter) of the canonical Regge-action remainder along the line potential through $\xi$ is at most $M\|\xi\|^3$.
background
This module isolates the last analytic Taylor ingredient needed once the nonlinear Hessian of the Regge action is identified: a local third-order bound on the remainder in the finite-dimensional space of vertex potentials.
The target proposition asserts existence of a radius $r>0$ and a constant $M\ge 0$ controlling the third iterated derivative of the map $s\mapsto$ (canonical Regge remainder evaluated on the line potential through $\xi$ at parameter $s$), uniformly for $s\in[0,1]$ and $|\xi|<r$. The line potential is the straight-line path in vertex-potential space from the zero configuration to $\xi$. Flatness of the configuration supplies the geometric vanishing that makes the low-order jets of the remainder controllable.
Upstream, the same flatness hypothesis already yields a chain-rule bound on the line-restricted third derivative and a local norm bound on the third iterated Fréchet derivative of the canonical remainder; those two facts are the only analytic inputs required here.
proof idea
Pure term-mode assembly. Apply the general combiner that turns a chain-rule bound and a local third-derivative norm bound into the line third-derivative target. Feed it the two flat-configuration lemmas already proved in this module: the chain-rule bound for the line-restricted remainder, and the local bound on the third iterated Fréchet derivative of the canonical remainder. No further calculation is performed at this site.
why it matters
Closes one of the four analytic sub-targets (ContDiff, quadratic-Taylor vanishing, chain-rule, local norm) that the module packages into the composite line-Taylor data target. Downstream, the analytic-closure certificate records this fact as the line third-derivative clause discharged from flatness alone, and the local Hessian–Taylor input constructor consumes the same bound when assembling nonlinear Regge cubic-Taylor hypotheses from an eventually-zero edge stencil and a remainder-jet target.
In the broader Recognition geometry stack this is the cubic remainder control that lets the discrete Regge action sit under a genuine third-order Taylor theorem in vertex-potential space, after the nonlinear Hessian identification. It is pure analysis on a fixed triangulation; it does not itself force $D=3$ or the eight-tick structure, but it is the estimate those discrete structures rely on once the continuum bridge is in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.