linePotential
plain-language theorem explainer
The affine line through the zero conformal potential in a fixed vertex-potential direction, scaled by a real parameter t. First-variation and cubic-Taylor modules cite it to restrict the nonlinear Regge action and its remainder to one-dimensional slices. The body is the pointwise product of t with the direction field on vertices.
Claim. For a finite 3D triangulation $K$ and a vertex conformal potential $\eta$, the line potential at parameter $t\in\mathbb{R}$ is the vertex potential $i\mapsto t\cdot\eta(i)$.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential, via Schläfli cancellation plus zero deficit. A finite 3D Regge triangulation carries abstract incidence data and a nondegenerate squared-edge tuple on every tetrahedron. Vertex conformal potentials are real assignments to the finitely many vertices: maps $\mathrm{Fin},n_V\to\mathbb{R}$.
The second-variation module already defines the same line construction (through the flat potential in a direction $\xi$). This local copy exists so the first-variation development does not import that module. Downstream cubic-Taylor work restricts the canonical remainder along $t\mapsto t\xi$ and needs a uniform name for that path.
proof idea
Pure definition: the returned potential is the function sending each vertex index $i$ to the scalar product $t\cdot\eta(i)$. No lemmas or tactics; it is the standard ray through the origin in the finite-dimensional space of vertex potentials.
why it matters
Almost every line-restricted estimate in the cubic Taylor bound module is stated in terms of this path: ContDiff of the remainder along the line, the chain-rule bound on third derivatives on $[0,1]$ inside a small ball about the flat point, and the one-dimensional cubic remainder estimate $|R(t\xi)|\le C|\xi|^3$ at $t=1$. Those targets reduce the full Fréchet remainder to ordinary one-variable Taylor calculus once value, first variation, and Hessian vanish at the flat configuration. In the broader Regge program this is the standard device that turns the geometric first-variation claim (Schläfli plus zero deficit at flat conformal data) into analytic derivative statements along rays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.