linePotential_zero
plain-language theorem explainer
At parameter zero, the straight-line path of vertex potentials in a fixed direction returns the zero potential on every vertex. First- and second-variation packages for the nonlinear Regge action cite this to pin the base point of directional expansions. The proof is function extensionality plus unfolding the two definitions.
Claim. For any 3-dimensional triangulation $K$ and any vertex potential $\xi$, the straight-line family of potentials through $\xi$ evaluates at $t=0$ to the identically zero potential on the vertices of $K$.
background
The module develops second-variation and cubic-remainder targets for the nonlinear Regge action on a 3D triangulation. Until the full Cayley–Menger/arccos chain-rule expansion is in place, analytic hypotheses sit in named input structures; this lemma is pure bookkeeping on those structures.
A vertex potential assigns a real number to each vertex. The line potential is the affine path $t \mapsto t,\xi$ in that space: at each vertex $i$, the value is $t$ times $\xi_i$. The zero potential is the configuration that assigns $0$ to every vertex. Evaluating the line at $t=0$ must recover that zero section; the lemma records exactly that identity.
It is imported from (and duplicated in) the first-variation module, where the same path is used to state directional derivatives of deficit angles and of the Regge action itself.
proof idea
Term-mode proof in two steps. Apply function extensionality over the vertex index $i$, reducing the claim to a pointwise equality of reals. Then simp unfolds the definitions of the line potential and the zero potential; both sides become $0$. No external lemmas are required.
why it matters
Every directional expansion of the Regge action or its remainder along a line needs a clean base point. Downstream, canonicalRemainderLine_value_at_zero rewrites the remainder at the line base point to zero via this identity; contDiff and first-derivative statements for the line-restricted remainder likewise start from $t=0$. First-variation packages (directional first-variation formula, local angle and dihedral derivative packages on flat configurations, action-along-line derivative) use the same anchor.
In the Recognition geometry stack this is scaffolding hygiene rather than a forcing-chain step: it keeps the second-variation and cubic-Taylor targets well-typed at the flat configuration so that Hessian comparisons and remainder bounds can be stated without ad-hoc case splits on the path parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.