CanonicalRemainderLineChainRuleBoundTarget
plain-language theorem explainer
Named Prop packaging a localized chain-rule bound: on a small ball about the flat vertex potential, the third ordinary derivative of the Regge remainder along any line segment is controlled by the third Fréchet derivative times ‖ξ‖³. Cubic-Taylor analysts cite it as sub-target (a) before assembling the line third-derivative estimate. As a definition it carries no proof; later flat-configuration theorems inhabit it.
Claim. For an incidence-consistent 3D triangulation $K$, there exists $\varepsilon>0$ such that for every vertex potential $\xi$ with $\|\xi\|<\varepsilon$ and every $t\in[0,1]$, $$\bigl|\partial_s^3\, R(\mathrm{line}(\xi,s))\bigr|_{s=t} \le \|D^3 R(t\cdot\xi)\|\,\|\xi\|^3,$$ where $R$ is the canonical Regge action remainder (action minus the canonical Hessian quadratic) and $\mathrm{line}(\xi,s)=s\cdot\xi$.
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 a 3D triangulation $K$ that is incidence-consistent. The canonical remainder $R$ is the Regge action minus the quadratic form of the canonical Regge Hessian; the flat configuration is the zero-potential point.
Global $C^3$ of $R$ is unavailable, so chain-rule identities for third derivatives hold only inside a neighborhood of the flat point. The relevant comparison is between the ordinary third derivative of the scalar path $s\mapsto R(s\cdot\xi)$ and the third Fréchet derivative $D^3 R$ evaluated along that path. Localization to $|\xi|<\varepsilon$ and $t\in[0,1]$ keeps $t\cdot\xi$ inside the $C^3$ ball so within-set Fréchet calculus upgrades to free-space derivatives.
Upstream geometry supplies the concrete remainder and Hessian; the module then splits the cubic bound into named sub-targets (contDiff, quadratic jet vanishing, this chain-rule inequality, and a local norm bound on $D^3 R$).
proof idea
Definition only: the body is the Prop asserting existence of $\varepsilon>0$ and the pointwise inequality between $|\mathrm{iteratedDeriv},3$ of the line-restricted remainder| and $|\mathrm{iteratedFDeriv},\mathbb{R},3, R(t\cdot\xi)|,|\xi|^3$. No tactics or lemmas are applied here. Downstream, the inhabiting theorem extracts a $C^\infty$ neighborhood of the flat point from flatness, restricts to the open ball of radius $\varepsilon$, applies the within-set chain rule for composition on the right, and upgrades within-set Fréchet derivatives to free-space ones on that open set.
why it matters
Sub-target (a) in the cubic Taylor cascade for the nonlinear Regge remainder. It is discharged by the flat-configuration closure theorem, which proves the Prop under FlatConfiguration. The third-derivative line bound is then obtained conditionally from this chain-rule target plus the local norm bound on $D^3 R$. Those pieces assemble into line-Taylor data and feed the analytic-closure certificate that yields the full nonlinear Regge cubic Taylor theorem from flatness and jet inputs.
In the broader Recognition geometry stack this is pure analysis on the discrete action: it does not touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula, but it is required infrastructure for controlling higher-order curvature defects once the Hessian is fixed. Without the localized chain rule the cubic remainder estimate cannot pass from Fréchet data to ordinary line derivatives on $[0,1]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.