linePotential_one
plain-language theorem explainer
On any finite 3D Regge triangulation, the straight-line path through the flat conformal potential in direction ξ returns ξ itself at parameter value 1. Analysts bounding the cubic remainder of the nonlinear Regge action cite this as the endpoint normalization of the ray. The proof is function extensionality plus unfolding the pointwise scaling definition.
Claim. Let $K$ be a finite 3D Regge triangulation and let $\xi$ be a vertex conformal potential on $K$. The straight-line path $t\mapsto t\cdot\xi$ through the flat configuration satisfies $\mathrm{line}_K(\xi,1)=\xi$.
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 conformal potentials.
A Triangulation3D is a finite abstract 3D Regge complex (vertex, edge, and tetrahedron counts plus incidence data) with nondegenerate squared-edge lengths on every tetrahedron. A vertex conformal potential is a real assignment to the finitely many vertices, i.e. a map $\mathrm{Fin},n_V\to\mathbb{R}$.
The line potential (defined identically in the first- and second-variation modules) is the straight ray through the flat configuration: $\mathrm{line}_K(\xi,t)(i)=t,\xi(i)$. It is the standard one-parameter family used to reduce jet and remainder estimates on the full potential space to ordinary one-variable calculus along rays.
proof idea
Pointwise function extensionality reduces the equality of potentials to an equality of real numbers at each vertex index $i$. Unfolding the definition of the line potential then yields $1\cdot\xi(i)=\xi(i)$, which closes by the ring identity for the unit scalar.
why it matters
The cubic Taylor package for the nonlinear Regge remainder works with raywise estimates of the form $\lvert R(t\xi)\rvert\le C\lVert\xi\rVert^3$ for small $t$. Normalizing the ray so that $t=1$ recovers the full potential $\xi$ is the elementary endpoint identity needed when those estimates are reassembled into a neighborhood bound on the whole vertex-potential space.
Downstream, nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate consumes a packaged line-cubic estimate and produces the full nonlinear cubic Taylor theorem; the present identity is the trivial but necessary calibration that the line at unit parameter is the original potential. It sits after Hessian identification and before the global remainder bound that feeds discrete gravity / Regge calculus comparisons in the geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.