singlePerturb_at
plain-language theorem explainer
Evaluating a single-edge squared-length perturbation at the edge it targets recovers the scalar step size. Anyone deriving one-dimensional restrictions of the Cayley–Menger Taylor formula cites this. The proof is a one-line unfold of the piecewise definition followed by simplification of the equality branch.
Claim. For every edge index $i \in \{0,\ldots,5\}$ and every real step $t$, the single-coordinate perturbation that equals $t$ at edge $i$ and $0$ on all other edges evaluates to $t$ when read at index $i$.
background
This module works with the Cayley–Menger polynomial $\mathrm{CM}_3$ on six squared edge lengths of a tetrahedron (type SqEdges). The edge ordering is fixed: edges $0..5$ are $(0,1)$, $(0,2)$, $(0,3)$, $(1,2)$, $(1,3)$, $(2,3)$. Formal $C^\infty$ differentiability of $\mathrm{cm}_3$ is already available; the module’s job is the explicit gradient and the polynomial Taylor identity for $\mathrm{cm}_3(a+h)$.
The single-coordinate perturbation is the SqEdges-valued map that places a real scalar $t$ at one chosen index $i$ and zero elsewhere. It is the elementary direction used to restrict the multivariable Taylor expansion of $\mathrm{cm}_3$ to a single edge update, which is how the six partial derivatives are extracted.
proof idea
One-line wrapper. Unfold the definition of the single-coordinate perturbation (the piecewise map if j = i then t else 0) and simplify at j = i; the equality branch yields t immediately. No external lemmas are required.
why it matters
The result is the evaluation identity needed by cm3_update_taylor, the specialised corollary of the multivariable Taylor identity when only the $i$-th squared length is shifted. That corollary collapses $\mathrm{cm}_3$ along one coordinate to gradient term plus quadratic and cubic remainders in the single-edge step, and it is what feeds the six per-edge partial-derivative theorems.
Those partials are the geometric input to the Regge second-variation matrix $M_{ij}$ compared to face areas under the conformal edge ansatz. In the Recognition geometry stack this is infrastructure for the discrete curvature / second-variation side of the forcing chain, not a landmark (T0–T8) statement itself. The declaration is fully proved scaffolding for the closed-form gradient API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.