linePotential_eq_smul
plain-language theorem explainer
The straight-line path through the flat conformal potential in direction ξ at real parameter t equals the scalar multiple t ξ in vertex-potential space. Cubic-Taylor and second-variation arguments for the nonlinear Regge action cite it to rewrite line maps as ordinary scalar multiplication. Proof is pointwise function extensionality plus unfolding the definition.
Claim. For any finite 3D Regge triangulation $K$, any vertex conformal potential $\xi\colon V(K)\to\mathbb{R}$, and any $t\in\mathbb{R}$, the line through the zero potential in direction $\xi$ satisfies $\gamma_\xi(t)=t\,\xi$ in the finite-dimensional space of vertex potentials.
background
This module isolates the local third-order Taylor bound on the nonlinear Regge remainder once the Hessian has been identified. The ambient space is the finite-dimensional vector space of vertex conformal potentials on a 3D triangulation $K$: real assignments to the $n_V$ vertices.
The line potential is the straight path through the flat (zero) potential in a fixed direction $\xi$. In the first- and second-variation modules it is defined pointwise by $(\gamma_\xi(t))(i)=t,\xi(i)$. Scalar multiplication on $\mathrm{Fin},n_V\to\mathbb{R}$ is the same pointwise product, so the two writings of the path are definitionally identical once both notations are available.
The triangulation structure supplies only incidence and nondegenerate squared-edge data; no curvature hypothesis enters this identity.
proof idea
Pointwise function extensionality on the vertex index, followed by simplification with the definition of the line potential. Both sides evaluate to $t\cdot\xi(i)$ at each vertex, so the equality is immediate. No external lemmas are required.
why it matters
Serves as the notational bridge inside the cubic Taylor program for the nonlinear Regge remainder. Downstream it rewrites the path so that hasDerivAt_linePotential can quote the standard derivative of $t\mapsto t,\xi$, so that the continuous-linear-map form of the line coincides with the potential form, and so that the unit-interval norm bound reduces to $|t|\le 1$.
Further downstream, the physical six-tetrahedron cubic Dirichlet instance uses the scalar form when proving that the spacing-scaled second-order Regge action, divided by $|a|^2$, equals the quadratic form $\tfrac12 H(\xi,\xi)$ on $a,\xi$ whenever the flat action is normalized to zero. The identity itself is pure linear algebra; its value is that every later analytic estimate may treat the path as ordinary scalar multiplication in a finite-dimensional normed space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.