linePotential_zero
plain-language theorem explainer
At parameter zero, the straight-line path through conformal vertex potentials on a 3D triangulation recovers the zero (flat) potential. Anyone evaluating the Regge action, its remainder, or directional derivatives along a ray from the flat background cites this identity. The proof is pointwise extensionality plus unfolding of the two definitions.
Claim. For any 3-dimensional triangulation $K$ and any vertex potential $\eta$, the affine line path $t \mapsto \Phi_{K,\eta}(t)$ in the space of conformal vertex potentials satisfies $\Phi_{K,\eta}(0) = 0_K$, where $0_K$ denotes the zero potential on $K$.
background
This module develops the first variation of the full nonlinear Regge action on a 3D triangulation. The geometric target is vanishing of that first variation at the flat conformal potential, via Schläfli cancellation together with zero deficit; the analytic work packages directional derivatives of edge lengths, dihedral angles, and the action along straight lines in potential space.
A vertex potential assigns a real conformal weight to each vertex of $K$. The zero potential is the flat background. The line potential is the affine path $t \mapsto (1-t)\cdot 0 + t\cdot\eta$ (equivalently, scale $\eta$ by $t$) through that space, so every directional derivative of a geometric functional is realized as an ordinary one-variable derivative at $t=0$ along this path.
The identity here is the base-point normalization of that path: at $t=0$ one sits exactly on the zero potential, independent of the direction $\eta$.
proof idea
Term-mode proof by function extensionality on the vertices of $K$. After funext, both sides reduce by simp unfolding the definitions of the line potential and the zero potential; the $t=0$ specialization is then definitional equality at each vertex.
why it matters
This is the base-point lemma for every line-restricted calculation in the Regge first-variation and cubic-Taylor stack. Downstream, canonicalRemainderLine_value_at_zero rewrites the remainder at the line potential of parameter zero to the remainder at the zero potential and obtains zero. The same rewrite feeds ContDiffAt and HasDerivAt statements for the canonical remainder line, the action-along-line smoothness used in the nonlinear Hessian proof, and the flat-configuration packages that build local dihedral and squared-angle chain-rule data for the directional first-variation formula.
In the module's program, those packages are the named analytic inputs until the full derivative expansion from closed-form local Schläfli identities is complete. The lemma itself is purely kinematic (no curvature or deficit hypothesis), which is why it is available before flatness is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.