canonicalRemainder_contDiffAt_zero_of_flatConfiguration
plain-language theorem explainer
On any incidence-consistent 3D triangulation with a flat configuration, the canonical Regge action remainder (action minus its value at zero minus half the canonical Hessian quadratic) is C^∞ at the zero vertex potential. Analysts proving the cubic Taylor bound for the nonlinear Regge remainder cite this smoothness seed. The proof unfolds the remainder and subtracts three ContDiffAt facts: flat action smoothness, a constant map, and the Hessian quadratic via fun_prop.
Claim. Let $K$ be a 3-dimensional triangulation that is incidence-consistent and admits a flat configuration. Then the map sending a vertex potential $\xi$ to the canonical Regge action remainder of $\xi$ (Regge action of $\xi$ minus its value at the zero potential minus half the quadratic form of the canonical Regge Hessian) is infinitely differentiable at the zero potential: $\mathrm{ContDiffAt}\,\mathbb{R}\,\top$ at $0$.
background
This module isolates the last analytic step after the nonlinear Hessian is identified: a local third-order bound on the Regge remainder in the finite-dimensional space of vertex potentials. The remainder is the nonlinear action minus its constant term at the flat (zero) potential minus the quadratic form built from the canonical Regge Hessian.
A flat configuration supplies smoothness of the full Regge action at zero potential (action_contDiff_at_zero). Vertex potentials are the discrete degrees of freedom on the triangulation; the zero potential is the flat reference. The canonical Hessian is the second-variation operator already fixed upstream in the nonlinear Hessian development.
The local setting is pure finite-dimensional real calculus on that potential space: once the remainder is known to be $C^\infty$ at zero, standard Taylor theory can convert vanishing 0-, 1-, and 2-jets into an $O(|\xi|^3)$ estimate.
proof idea
Unfold the remainder definition so the claim is ContDiffAt of $A(\xi) - A(0) - \tfrac12 Q_H(\xi)$ at zero, where $A$ is the Regge action and $Q_H$ the canonical Hessian quadratic.
From the flat-configuration hypothesis, take action_contDiff_at_zero for $A$. The constant map $\xi \mapsto A(0)$ is ContDiffAt by contDiffAt_const. The quadratic term is ContDiffAt after unfolding hessianQuadratic and applying fun_prop.
Close by subtracting twice: $(h_A - h_{\mathrm{const}}) - h_{\mathrm{quad}}$, using ContDiffAt closed under subtraction.
why it matters
This is the smoothness seed for the cubic Taylor package on the nonlinear Regge remainder. Downstream closures use it directly: the local bound on the third iterated Fréchet derivative at zero (canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration), the line-restricted ContDiffAt and ContDiff targets, the chain-rule bound on rays $t\mapsto t\cdot\xi$, and the assembly of local Hessian-Taylor inputs.
The module doc frames the exact remaining finite-dimensional Taylor theorem: the canonical remainder is already smooth at the flat point with value zero; connecting zero first and second variations to a local $O(|\xi|^3)$ bound is the analytic content isolated here without new axioms. In the broader Recognition geometry stack this underwrites controlled discrete curvature expansions around flat configurations on 3D triangulations (the $D=3$ setting forced upstream), feeding nonlinear Regge analysis rather than continuum GR identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.