functionUpdate_hasDerivAt_single
plain-language theorem explainer
The path that replaces the k-th entry of a six-component real vector a by a scalar t is differentiable at t = a(k), with derivative the standard basis vector e_k in R^6. Anyone computing single-edge directional derivatives of tetrahedron edge data or dihedral quantities cites this. The proof is a componentwise case split after reducing through the product rule for HasDerivAt.
Claim. For any $a:\{0,\ldots,5\}\to\mathbb{R}$ and any index $k$, the map $t\mapsto a[k\mapsto t]$ (replace only the $k$-th component by $t$) has derivative at $t=a(k)$ equal to the standard basis vector $e_k\in\mathbb{R}^6$.
background
This module develops the analytic first variation of the nonlinear Regge action on tetrahedra, aiming at vanishing of that variation at the flat conformal potential via Schläfli cancellation and zero deficit.
A tetrahedron has six edges, so edge (or squared-edge) data live in maps $\mathrm{Fin},6\to\mathbb{R}$. Function.update a k t is the vector that agrees with $a$ off $k$ and equals $t$ at $k$. HasDerivAt f f' x is Mathlib's predicate that $f$ is differentiable at $x$ with derivative $f'$. Pi.single k 1 is the coordinate basis vector $e_k$ in the product space $\mathbb{R}^6$.
The lemma is pure finite-dimensional calculus: it equips single-edge parameter paths with an explicit derivative, so later Fréchet derivatives of dihedral and action functionals can be evaluated on those directions.
proof idea
Apply hasDerivAt_pi to reduce differentiability in $\mathbb{R}^6$ to six scalar claims, one per coordinate $i$.
If $i=k$, substitution shows the $i$-th component of the update path is the identity map on $\mathbb{R}$, so hasDerivAt_id supplies derivative $1$, matching the $k$-th slot of $e_k$.
If $i\neq k$, the $i$-th component is independent of $t$ (equal to the constant $a(i)$). Rewrite by funext and Function.update, then apply hasDerivAt_const; the off-diagonal slots of Pi.single vanish, so both sides match.
why it matters
Downstream, fderiv_dihedralAngle3Sq_apply_single evaluates the Fréchet derivative of the squared dihedral-angle map on a single-edge basis vector; that theorem applies this lemma to justify differentiating under the edge-update path.
In the module's program, single-edge directional derivatives are the elementary inputs to the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric content is Schläfli cancellation plus zero deficit; this calculus fact is the analytic hinge that lets those identities act on concrete tangent vectors in squared-edge space.
It does not itself invoke Recognition-Science forcing landmarks (T5–T8, RCL, $\phi$), but it sits in the geometry layer that supports Regge/TT hinge analysis feeding continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.