cmCofactor3Poly_34_update_polyform
plain-language theorem explainer
Taylor expansion of the (3,4) Cayley-Menger cofactor polynomial when one squared-edge coordinate is shifted by t. Dihedral-angle and Regge calculus work that needs explicit cofactor partials cites this identity. The proof case-splits on the six edge indices, unfolds the named polynomials, and finishes by ring normalization.
Claim. Let $a$ be six squared edge lengths of a tetrahedron, $k\in\{0,\ldots,5\}$, and $t\in\mathbb{R}$. Writing $C_{34}$ for the explicit $(3,4)$ Cayley-Menger cofactor polynomial and $\partial_k C_{34}$ for its partial in coordinate $k$, one has $C_{34}(a+t\,e_k)=C_{34}(a)+(\partial_k C_{34})(a)\,t+c_k t^2$, where $c_k=-1$ if $k=0$ and $c_k=0$ otherwise; the cubic coefficient vanishes for every $k$.
background
The module expands every tetrahedral Cayley-Menger cofactor as an explicit polynomial in the six squared edge lengths. Downstream dihedral-angle calculus can then quote named polynomial partials instead of opaque Fréchet derivatives. Squared edges are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$).
The object $C_{rc}$ is the explicit normal form cmCofactor3Poly r c: a multilinear combination of the six edge squares matching the corresponding cofactor of the $5\times5$ Cayley-Menger matrix. Its coordinate partials are likewise tabulated as cmCofactorPartial r c k. The present statement is the degree-$\le 2$ Taylor identity for the single entry $(r,c)=(3,4)$ along one edge coordinate.
Because each cofactor is at most quadratic in any single edge square (with a lone $t^2$ term only when that coordinate is edge $0$), the cubic remainder is identically zero. That algebraic fact is what the identity records.
proof idea
Term-mode proof by exhaustive case split: fin_cases k produces six goals, one per edge index. Each goal unfolds cmCofactor3Poly, cmCofactorPartial, and Function.update, then ring_nf equates the two polynomial expressions in the six edge squares and the shift $t$. No external lemmas beyond the definitions are required; the quadratic coefficient $-1$ appears only in the $k=0$ branch, and the $t^3$ coefficient is zero in every branch.
why it matters
Immediate consumer is hasDerivAt_cmCofactor3Poly_34_along_coord, the closed-form coordinate derivative of the same $(3,4)$ cofactor: the Taylor identity supplies the difference quotient whose $t\to 0$ limit is the tabulated partial. That derivative is the cofactor-side counterpart of the Cayley-Menger derivative suite, letting dihedral-angle formulas differentiate through named polynomials rather than opaque fderiv terms.
In the broader Recognition geometry stack this sits under tetrahedral edge calculus used by Regge-type hinge analysis. It does not itself touch the forcing chain (T5–T8) or the J-cost; it is pure classical algebraic geometry of the Cayley-Menger matrix, packaged so later RS gravity modules can cite a proved partial instead of a symbolic stub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.