CanonicalRemainderIteratedFDerivLocalBoundTarget
plain-language theorem explainer
Names the local-norm sub-target on the third Fréchet derivative of the canonical Regge remainder near the flat point: existence of δ>0 and M≥0 with the third derivative norm at most M whenever the potential norm is below δ. Analysts closing the cubic Taylor estimate for nonlinear Regge action cite it as sub-target (b). The Prop is pure packaging; the closing theorem uses ContDiffAt continuity of the iterated derivative at zero.
Claim. For an incidence-consistent 3D triangulation $K$, there exist $\delta>0$ and $M\ge 0$ such that every vertex potential $z$ with $\|z\|<\delta$ satisfies $\|D^3 R(z)\|\le M$, where $R$ is the canonical Regge-action remainder (Regge action minus the quadratic piece of the canonical Hessian).
background
The module isolates the final analytic cubic Taylor theorem for the nonlinear Regge remainder after the Hessian has been identified. Work takes place in the finite-dimensional space of vertex potentials on an incidence-consistent 3D triangulation $K$. The remainder $R$ is the Regge action with the quadratic contribution of the canonical Hessian subtracted, so $R$ and its first two variations vanish at the flat configuration.
Sub-target (b) asks only for a local operator-norm bound on the third Fréchet derivative $D^3 R$ in a neighborhood of zero. Continuity of the third iterated Fréchet derivative at the flat point (from ContDiffAt at top order) is the intended source of such a bound. A companion chain-rule target then turns the local norm into a line-restricted third-derivative estimate along rays $t\cdot\xi$ for $t\in[0,1]$.
proof idea
Definition of a proposition, not a proved statement. The body is the existential claim that there exist $\delta>0$ and $M\ge 0$ controlling the third Fréchet derivative of $R$ on the open $\delta$-ball about the zero potential. Downstream, the flat-configuration closure obtains ContDiffAt of $R$ at top order, invokes continuity of the iterated Fréchet derivative at zero, and takes $M$ one larger than the norm at zero with $\delta$ from the continuity statement. The line third-derivative bound then unpacks that pair and combines it with the chain-rule pointwise estimate.
why it matters
Feeds four local consumers: the flat-configuration closure of this target; the line third-derivative bound conditional on chain-rule plus local norm; the composite line-Taylor data assembly from the four sub-targets; and the cascade closure certificate that builds the cubic Taylor theorem from flatness plus jet inputs. In the Recognition geometry stack this is the last pure analytic local bound needed once the nonlinear Hessian is fixed, enabling cubic remainder control in finite-dimensional vertex-potential space and completing the Taylor side of the Regge-action analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.