linePotential_contDiffAt_zero
plain-language theorem explainer
The straight-line path of vertex conformal potentials through the flat configuration, in any fixed direction ξ, is C^∞ as a map ℝ → (vertices → ℝ) at t = 0. Anyone building second-variation or Hessian arguments for the nonlinear Regge action cites this to justify differentiating under the action along that ray. The proof is a short term-mode argument: componentwise ContDiffAt plus Mathlib's fun_prop on scalar multiplication.
Claim. For any finite 3D triangulation $K$ and any vertex conformal potential $\xi$, the map $t \mapsto (i \mapsto t\,\xi_i)$ from $\mathbb{R}$ into the space of vertex potentials is infinitely differentiable at $t = 0$.
background
In the Regge geometry stack, a Triangulation3D is a finite abstract 3-complex with incidence data and nondegenerate squared edge lengths on each tetrahedron. A vertex conformal potential is simply a real assignment to each vertex (type Fin nV → ℝ). The zero assignment is the flat configuration.
The line potential is the straight ray through that flat point in direction $\xi$: at parameter $t$ one multiplies every component of $\xi$ by $t$. First- and second-variation modules both use this ray so that directional derivatives of the Regge action reduce to ordinary one-variable calculus in $t$.
This module isolates the remaining hard step of the nonlinear Hessian program: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Infinite differentiability of the ray itself is the elementary analytic prerequisite before the action composition can be differentiated.
proof idea
Term-mode, four steps. Rewrite the goal with contDiffAt_pi so ContDiffAt of a product-valued map becomes ContDiffAt of each coordinate. Introduce the vertex index $i$. Unfold the definition of the line potential, exposing the map $t \mapsto t \cdot \xi_i$. Discharge the resulting scalar multiplication goal by Mathlib's fun_prop automation, which knows that multiplication by a fixed real is $C^\infty$.
why it matters
Feeds directly into actionAlongLine_contDiffAt_zero_of_flatConfiguration, which lifts ContDiffAt from the potential ray to the full nonlinear Regge action along that ray (under incidence consistency and flatness). That smoothness is required before one can form first and second derivatives of the action at $t = 0$ and identify the second derivative with the canonical incidence Hessian.
In the module's own framing, this is not a new physical hypothesis: it is bookkeeping that lets the second chain-rule calculation close, after which ReggeActionSecondVariationInput follows. Within Recognition Science geometry, the nonlinear Hessian at the flat conformal potential is the bridge from discrete Regge calculus to continuum curvature response; without $C^\infty$ of the ray, the directional Hessian is not even defined in the Lean development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.