cmCofactor3Poly_update_polyform
plain-language theorem explainer
Along any single squared-edge coordinate, every tetrahedral Cayley–Menger cofactor expands exactly as a quadratic Taylor polynomial: constant term plus linear partial times t plus quadratic coefficient times t², with vanishing cubic term. Geometers and anyone differentiating dihedral angles via CM cofactors cite this identity. The proof is exhaustive case analysis on the five-by-five cofactor indices and the six edge slots, followed by simplification and ring normalization.
Claim. For every cofactor index pair $(r,c)\in\{0,\ldots,4\}^2$, every squared-edge index $k\in\{0,\ldots,5\}$, every squared-edge assignment $a$, and every real increment $t$, the cofactor polynomial evaluated after replacing the $k$-th squared edge by $a_k+t$ equals $P(a)+(\partial_k P)(a)\,t+Q_k(a)\,t^2+0\cdot t^3$, where $P$ is the explicit cofactor polynomial, $\partial_k P$ its named partial in coordinate $k$, and $Q_k$ the quadratic coefficient of that one-coordinate restriction.
background
The module expands every tetrahedral Cayley–Menger cofactor as an explicit polynomial in the six squared edge lengths (SqEdges := Fin 6 → ℝ). Downstream dihedral-angle calculus can then quote named polynomial partials instead of opaque Fréchet derivatives.
cmCofactor3Poly r c a is the closed-form polynomial for the $(r,c)$ entry of the 5×5 CM cofactor array. Because each cofactor is at most quadratic in any single squared-edge coordinate, the one-variable restriction admits an exact degree-2 Taylor expansion. The linear coefficient is packaged as cmCofactorPartial r c k a (explicit partial in edge $k$), and the quadratic coefficient as cmCofactorQuadraticCoeff r c k a.
The identity records that expansion after the coordinate update $a_k\mapsto a_k+t$, with the cubic coefficient written as the literal zero to make the polynomial form uniform for later derivative extraction.
proof idea
Pure case explosion and algebra. The proof runs fin_cases on the cofactor row $r$, column $c$, and edge index $k$, covering all $5\times5\times6$ combinations. In each branch it unfolds the three match-defined polynomials (cmCofactor3Poly, cmCofactorPartial, cmCofactorQuadraticCoeff) together with Function.update, then finishes by ring_nf, which verifies the quadratic identity and the vanishing of the $t^3$ term. No external lemmas beyond the definitions themselves are required.
why it matters
This is the algebraic bridge from static cofactor polynomials to differentiable geometry of tetrahedra. The sole recorded consumer is hasDerivAt_cmCofactor3Poly_along_coord, whose doc-comment announces a “closed-form coordinate derivative of every cofactor polynomial.” That derivative theorem rewrites the one-parameter family as the Taylor form proved here, then reads off HasDerivAt with derivative equal to the named partial.
In the broader Recognition geometry stack the module is the cofactor analogue of CayleyMengerDerivatives: once every cofactor is known to be a quadratic polynomial along each edge, dihedral-angle formulas built from CM minors become elementary rational functions with explicit gradients. The result does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure Euclidean infrastructure that those later geometric claims rely on when they differentiate volumes or angles with respect to edge lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.