linePotential
plain-language theorem explainer
Defines the ray through the zero conformal potential in a fixed direction ξ on a finite 3D Regge triangulation: at parameter t the potential is tξ. Anyone proving one-variable Taylor or chain-rule bounds for the nonlinear Regge action along conformal lines cites this. The body is the pointwise scalar multiplication map.
Claim. Given a finite 3D Regge triangulation $K$, a vertex conformal potential $\xi$ on $K$, and a real parameter $t$, the line potential at $t$ is the vertex potential $i \mapsto t\,\xi_i$ (the ray through the flat potential in direction $\xi$).
background
The module develops second-variation and cubic-remainder targets for the nonlinear Regge action on finite 3D triangulations. Until the full Cayley–Menger/arccos expansion is in place, analytic hypotheses sit in named input structures; this definition supplies the standard one-parameter family used to reduce those targets to ordinary calculus in $t$.
A Triangulation3D carries finite vertex/edge/tet counts and incidence data with nondegenerate squared-edge tuples. A VertexPotential is a real assignment to vertices (conformal factors). The zero potential is the flat background. The same line construction already appears in the first-variation module so that module stays independent; this copy is the second-variation side’s local version.
Downstream cubic Taylor work restricts the canonical remainder $R$ to $t \mapsto R(t\xi)$ and applies one-variable ContDiff, derivative, and Taylor estimates at $t=0$.
proof idea
Pure definition: the returned potential is the function sending each vertex index $i$ to $t$ times $\xi_i$. No lemmas or tactics; it is the pointwise scalar multiple that realizes the affine line through the flat potential.
why it matters
This is the geometric path along which second variation and cubic remainder of the Regge action are tested. Downstream, CanonicalRemainderLineCubicEstimateTarget asks for a uniform cubic bound on the remainder at $t\xi$ for small $|\xi|$; ContDiff and chain-rule targets (CanonicalRemainderLineContDiffTarget, CanonicalRemainderLineChainRuleBoundTarget and their closure theorems under flat configurations) all compose the remainder with this line. It therefore turns the multi-vertex Fréchet problem into a one-variable Taylor problem with vanishing value, first, and second derivatives at the origin, which is the practical route to controlling the nonlinear Regge action near flat space in the Recognition geometry stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.