canonicalRemainderLineContDiff_of_flatConfiguration
plain-language theorem explainer
Under a flat configuration of an incidence-consistent 3D triangulation, the canonical Regge-action remainder along any short affine path from the zero vertex potential is thrice continuously differentiable on [0,1]. Discrete-gravity and Regge-calculus analysts cite this to underwrite cubic Taylor expansions of the nonlinear remainder. The argument reduces infinite-order smoothness at the origin to a C³ neighborhood, then composes with the line map while a norm bound keeps the segment inside that ball.
Claim. Let $K$ be an incidence-consistent three-dimensional triangulation admitting a flat configuration. Then there exists $r>0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$, the scalar map $t\mapsto R_K(\mathrm{line}(\xi,t))$ is $C^3$ on $[0,1]$, where $R_K$ is the canonical Regge-action remainder relative to the canonical Regge Hessian and $\mathrm{line}(\xi,t)$ is the affine path from the zero potential to $\xi$.
background
This module isolates the final analytic Taylor step after the nonlinear Hessian of the Regge action has been identified. The ambient space is the finite-dimensional vector space of vertex potentials on a 3D triangulation $K$; the object of study is the nonlinear remainder $R_K$ obtained by subtracting the quadratic form of the canonical Regge Hessian from the full Regge action.
A flat configuration means the discrete geometry sits at a critical point where deficit angles vanish in the usual Regge sense, so the first variation of the remainder is zero at the origin. The target predicate asserts existence of a radius $r>0$ such that, for every $\xi$ inside the ball of radius $r$, the composite $t\mapsto R_K(\mathrm{line}(\xi,t))$ is $C^3$ on the compact interval $[0,1]$.
Upstream, infinite-order smoothness of $R_K$ at the zero potential under flatness is already available (canonicalRemainder_contDiffAt_zero_of_flatConfiguration). A companion norm bound controls $|\mathrm{line}(\xi,t)|$ for $t\in[0,1]$, keeping short segments inside any neighborhood of the origin.
proof idea
Define $R(\xi)=R_K(\xi)$ via the canonical Hessian. Invoke the upstream fact that $R$ is $C^\infty$ at the zero potential under flatness, then restrict to order $3$ on some open neighborhood $u$ of zero. Extract a metric ball of radius $\varepsilon>0$ inside $u$.
For any $\xi$ with $|\xi|<\varepsilon$, the affine line $t\mapsto\mathrm{line}(\xi,t)$ is $C^\infty$ (componentwise, by contDiffOn_pi and fun_prop). The norm bound on the line shows that the image of $[0,1]$ lands in the ball, hence in $u$. Compose the $C^3$ restriction of $R$ on $u$ with this line map to obtain $C^3$ of the composite on $[0,1]$. Package $\varepsilon$ as the required radius.
why it matters
The cubic Taylor program for the nonlinear Regge remainder needs $C^3$ regularity along rays before jet data, chain-rule identities, and local-norm estimates can be assembled. This theorem discharges the ContDiff leg of that package.
It is wired directly into canonicalRemainderAnalyticClosureCert (the line_contDiff_from_flat field), into the composite assembly theorem that builds full line-Taylor data from the four sub-targets, and into the local Hessian-Taylor input constructor used downstream. Together these close the analytic half of the cubic remainder bound after the Hessian identification step.
In the broader Recognition geometry stack this is pure discrete-gravity analysis: it does not touch the forcing chain (T5–T8), RCL, or the $\varphi$-ladder, but it supplies the smoothness needed for any later continuum or curvature-limit argument that expands the Regge action past quadratic order on flat backgrounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.