canonicalRemainder_line_eq_comp
plain-language theorem explainer
On any incidence-consistent 3D triangulation, the canonical Regge remainder evaluated along the straight line of vertex potentials t ↦ t·ξ equals the composition of the full remainder map with the continuous-linear line map. Analysts proving the local cubic Taylor bound for the nonlinear Regge action cite this identity to unlock the chain rule on third derivatives. The proof is a one-line extensionality plus the pointwise equality of the line map and the line potential.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation and let $\xi$ be a vertex potential on $K$. Write $R$ for the canonical Regge-action remainder (relative to the canonical Hessian). Then the real function $t \mapsto R(t\cdot\xi)$ equals the composition $R \circ L_\xi$, where $L_\xi$ is the continuous-linear map sending $t$ to the line potential $t\cdot\xi$.
background
The module isolates the final analytic Taylor theorem needed once the nonlinear Hessian of the Regge action has been identified. The ambient space is the finite-dimensional vector space of vertex potentials on a fixed 3D triangulation $K$; the remainder $R$ is the difference between the full nonlinear Regge action and its quadratic Hessian approximation at the flat configuration.
A line potential is the straight-line path $t \mapsto t\cdot\xi$ through a fixed potential $\xi$. The continuous-linear map version of that path (denoted lineCLM in the development) is the same object viewed as an element of $\mathrm{CLM}(\mathbb{R},\mathrm{VertexPotential},K)$, so that Mathlib's iterated-derivative chain-rule API applies directly.
The identity proved here is the bookkeeping step that lets later lemmas treat the restricted remainder as a genuine composition $R\circ L_\xi$ rather than an ad-hoc real function of $t$.
proof idea
Term-mode proof by function extensionality on $t:\mathbb{R}$. After funext, the goal reduces to pointwise equality of the remainder at the line potential versus at the continuous-linear line map evaluated at $t$. A single rewrite with the already-proved lemma equating those two maps discharges the goal.
why it matters
Inside the cubic-Taylor pipeline for the nonlinear Regge remainder, this identity is the algebraic prerequisite for the localized chain-rule bound (sub-target (a) in the same module): once the line-restricted remainder is literally $R\circ L_\xi$, the third iterated derivative along the segment becomes $(D^3 R)(t\cdot\xi)$ composed with three copies of $L_\xi$, yielding the estimate $|D^3(R\circ L_\xi)(t)|\le|D^3 R(t\cdot\xi)|,|\xi|^3$ inside a small ball where $R$ is $C^3$.
That bound is the analytic engine of the module's main cubic Taylor theorem for the Regge action after the Hessian has been fixed. In the broader Recognition Geometry stack it supplies the controlled remainder needed to pass from discrete curvature (Regge) to continuum Einstein–Hilbert behaviour. No downstream consumers are recorded yet; the immediate consumers are the sibling chain-rule and cubic-estimate targets in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.