singlePerturb_ne
plain-language theorem explainer
Off-support coordinates of a single-edge squared-length perturbation vanish. Anyone restricting the Cayley-Menger Taylor identity to a one-parameter edge update cites this to collapse the six-edge shift to a pure i-th coordinate change. The proof is a one-line unfold-and-simp of the piecewise definition.
Claim. For indices $i,j\in\{0,\ldots,5\}$ with $j\neq i$ and any real $t$, the single-coordinate perturbation that places value $t$ at edge $i$ (and zero elsewhere) evaluates to $0$ at edge $j$.
background
This module works with the Cayley-Menger polynomial cm3 on six squared edge lengths of a tetrahedron (edges ordered (0,1), (0,2), (0,3), (1,2), (1,3), (2,3)). The goal is an explicit gradient and a polynomial Taylor identity for cm3(a+h), later fed into the Regge second-variation matrix via a conformal edge ansatz.
The single-coordinate perturbation is the SqEdges-valued map that equals a real parameter t at a chosen index i and equals zero at every other index. It is the standard way to restrict a multivariable polynomial identity to a pure one-edge update Function.update a i (a i + t).
Spatial dimension three (forced in the RS chain at T8) fixes the tetrahedron and thus the six-edge indexing; the present lemma is purely combinatorial on that finite index set.
proof idea
Unfold the definition of the single-coordinate perturbation (the piecewise if j = i then t else 0). Then simp with the hypothesis j ≠ i discharges the false branch and yields zero. No calculus or Cayley-Menger algebra is used.
why it matters
The immediate consumer is the specialised Taylor corollary cm3_update_taylor: when only the i-th squared length is shifted by t, the full multivariable expansion collapses to the 1-D restriction along that edge, with gradient term, quadratic form, and cubic remainder all evaluated on the single-coordinate perturbation. That corollary is what feeds the six per-edge partial-derivative theorems.
Those partials are the closed-form ingredients of the Regge second-variation matrix compared to face areas. The module already has formal contDiff of cm3; this tiny support lemma is the bookkeeping step that makes the single-edge update identity hold definitionally. Framework landmarks D=3 and the tetrahedron edge count sit upstream as the reason there are exactly six coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.