canonicalRemainderLine_contDiffAt_zero_of_flatConfiguration
plain-language theorem explainer
On a flat, incidence-consistent 3D triangulation, the Regge action remainder restricted to the ray t ↦ t·ξ through any vertex potential is C^∞ at t = 0. Analysts proving the cubic Taylor bound along line segments cite this smoothness. The proof composes full-space remainder smoothness at the zero potential with smoothness of the linear path map.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat, and let $\xi$ be any vertex potential on $K$. Then the real function $t \mapsto R_K\bigl(H^{\mathrm{can}}_K,\, t\xi\bigr)$, where $R_K$ is the Regge action remainder relative to the canonical graph-Laplacian Hessian and $t\xi$ is the line potential, is $C^\infty$ at $t = 0$.
background
The module isolates the final analytic Taylor theorem for the nonlinear Regge remainder after the Hessian has been identified: a local third-order bound in the finite-dimensional space of vertex potentials on a 3D triangulation.
The canonical Regge Hessian is the graph-Laplacian built from incidence dual weights. The remainder $R_K(H^{\mathrm{can}},\xi)$ is the nonlinear Regge action minus its quadratic Hessian piece. A flat configuration means the discrete geometry sits at the zero-curvature basepoint where that expansion is taken. The line potential is the straight ray $t\mapsto t\xi$ in vertex-potential space, so the line-restricted remainder is the scalar path $t\mapsto R_K(H^{\mathrm{can}}, t\xi)$.
Upstream, canonicalRemainder_contDiffAt_zero_of_flatConfiguration already gives $C^\infty$ of the full remainder map $\xi'\mapsto R_K(H^{\mathrm{can}},\xi')$ at the zero potential under flatness. The present statement is the restriction of that smoothness to every linear ray through the origin.
proof idea
Apply the full-space result: the remainder map is ContDiffAt $\top$ at the zero potential under flatness. Separately, the path $t\mapsto$ linePotential$(K,\xi,t)$ is ContDiffAt $\top$ at $0$, proved componentwise via contDiffAt_pi and fun_prop on each scalar map $t\mapsto t\cdot\xi_i$. Rewrite the evaluation point using linePotential_zero, so linePotential at $0$ equals the zero potential, and transport the full-space ContDiffAt hypothesis to that point. Finish by ContDiffAt composition of the remainder map with the line path at $t=0$.
why it matters
Cubic Taylor control of the nonlinear Regge remainder is the analytic endpoint of the geometry stack in this module. Smoothness of the line restriction at $t=0$ is the first jet input needed before vanishing of low-order derivatives can be stated.
It feeds directly into iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs (first line derivative vanishes given the first-variation input) and iteratedDerivWithin_two_canonicalRemainderLine_of_jetInputs (second line derivative vanishes given the second-variation input). Those jet vanishings, together with a third-order bound, close the cubic Taylor theorem for the remainder along $[0,1]$.
In the broader Recognition geometry program this is discrete-curvature analysis on triangulations (Regge calculus), not a forcing-chain step (T5–T8). It supplies the $C^\infty$ hypothesis that lets the cubic remainder estimate be stated rigorously in finite dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.