canonicalRemainderLineChainRuleBound_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 ray t↦t·ξ obeys the chain-rule bound |∂³(R∘ℓ_ξ)(t)| ≤ ‖D³R(t·ξ)‖·‖ξ‖³ for all t∈[0,1] and all sufficiently small ξ. Analysts closing the cubic Taylor estimate for the nonlinear Regge action cite this. The proof localizes C³ smoothness at the flat point to a ball, applies the within-set chain rule, then uses the multilinear operator norm.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation that is a flat configuration. Then there exists $\varepsilon>0$ such that for every vertex potential $\xi$ with $\|\xi\|<\varepsilon$ and every $t\in[0,1]$, $$\bigl|\partial_s^3\bigl(R_K(\ell_\xi(s))\bigr)\big|_{s=t}\bigr|\le \|D^3 R_K(t\cdot\xi)\|\,\|\xi\|^3,$$ where $R_K$ is the canonical Regge-action remainder (relative to the canonical Hessian) and $\ell_\xi(s)=s\cdot\xi$.
background
The module isolates the final analytic cubic Taylor bound for the nonlinear Regge remainder after the Hessian has been identified. Work takes place in the finite-dimensional space of vertex potentials on a 3D triangulation $K$ that is incidence-consistent. The flat configuration hypothesis means the background geometry is undeformed, so the zero potential is the natural expansion point.
The canonical remainder $R_K$ is the Regge action minus its quadratic Hessian piece at the flat point. The line map $\ell_\xi(s)=s\cdot\xi$ restricts potentials to the real segment from $0$ to $\xi$. The target being proved is the localized chain-rule sub-target: existence of a ball radius $\varepsilon$ on which the third iterated derivative of $R_K\circ\ell_\xi$ is controlled by the free-space third Fréchet derivative of $R_K$ times $|\xi|^3$.
Upstream, $C^\infty$ regularity of the canonical remainder at the zero potential under flatness is already available (canonicalRemainder_contDiffAt_zero_of_flatConfiguration). Global $C^3$ is not assumed, so all differentiation is within open neighborhoods of zero.
proof idea
Start from flatness: the canonical remainder is $C^\infty$ at the zero potential, hence $C^3$ there. Extract a neighborhood on which it is $C^3$ on a set, then shrink to an open metric ball of radius $\varepsilon>0$ about zero (using that the zero potential is the zero vector).
For $|\xi|<\varepsilon$ and $t\in[0,1]$, the scaled point $t\cdot\xi$ stays inside the ball. The preimage of the ball under the continuous line map is open in $\mathbb{R}$, so unique differentiability holds on both the ball and the preimage. Apply ContinuousLinearMap.iteratedFDerivWithin_comp_right to obtain the within-set chain rule for the third iterated Fréchet derivative of $R\circ\ell_\xi$.
Because both domains are open, convert within-set derivatives to free-space ones via iteratedFDerivWithin_of_isOpen. The resulting continuous multilinear map applied to $(\xi,\xi,\xi)$ is bounded by the operator norm times $|\xi|^3$ (ContinuousMultilinearMap.le_opNorm), which is exactly the claimed scalar third-derivative bound.
why it matters
This declaration closes the localized chain-rule half of the cubic line estimate from flatness alone. Downstream it is fed directly into the third-derivative bound on the line-restricted remainder (canonicalRemainderLineThirdDerivBound_of_flatConfiguration), which multiplies the chain-rule estimate by the local norm bound on $D^3R$. That third-derivative bound, together with ContDiff and quadratic-jet vanishing, assembles the full line-Taylor data package used by the cascade closure theorems (canonicalRemainderLineTaylorData_of_flat_and_remainderJets, canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm) and the analytic-closure certificate.
In the broader Recognition geometry stack this is the analytic step that turns the nonlinear Hessian identification into a genuine cubic remainder control in vertex-potential space, the finite-dimensional setting underlying discrete curvature and Regge-type actions. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure local analysis on the triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.