linePotential_hasDerivAt_zero
plain-language theorem explainer
The straight-line path t ↦ t·η through vertex conformal potentials is differentiable at t = 0, with derivative exactly η. First-variation arguments for the nonlinear Regge action cite this to justify differentiating along conformal rays from the flat potential. The proof is a componentwise reduction: product rule on t ↦ t·η_i after rewriting HasDerivAt on the product space.
Claim. For any finite 3D triangulation $K$ and any vertex conformal potential $\eta : \mathrm{Fin}\,n_V(K) \to \mathbb{R}$, the path $t \mapsto t\cdot\eta$ in the space of vertex potentials is differentiable at $t = 0$ with derivative $\eta$.
background
This module develops the first variation of the nonlinear Regge action on a finite 3D triangulation. The target is vanishing of that first variation at the flat conformal potential, via Schläfli cancellation plus zero deficit.
A Triangulation3D carries finite vertex/edge/tet counts and incidence data with nondegenerate squared-edge data on each tetrahedron. A vertex conformal potential is a real assignment to vertices (Fin nV → ℝ). The local linePotential is the ray through the origin in direction η: $(t·η)_i = t·η_i$. This copy lives in the first-variation module so it does not depend on the second-variation file.
Differentiating the Regge action (or local dihedral angles) along such rays requires that the path itself be differentiable at $t = 0$ in the product topology on vertex potentials.
proof idea
Term-mode, four steps. Rewrite HasDerivAt on the product space Fin nV → ℝ via hasDerivAt_pi, reducing to one real coordinate per vertex. Unfold linePotential to the scalar map $t ↦ t·η_i$. Apply the product rule identity (hasDerivAt_id 0).mul_const (η i), which says $t ↦ t·c$ has derivative $c$ at $0$. simpa closes the component.
why it matters
This is the elementary differentiability fact that lets the module treat conformal rays as legitimate variation paths. Downstream, reggeAction_along_line_hasDerivAt_fderiv uses it to identify the derivative of the Regge action along the ray with the Fréchet derivative of the action at the zero potential applied to η. The package localDihedralDirectionalDerivativePackage_of_flat defines angle derivatives as ordinary deriv of dihedral angles under the same line potential, so those directional derivatives inherit well-definedness from this lemma.
In the broader Recognition geometry stack, first variation at the flat conformal potential is the analytic half of the Schläfli-plus-zero-deficit argument for criticality of flat configurations. The lemma itself is pure real analysis on finite products; the physics enters only through how parents assemble dihedral and action derivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.