hasDerivAt_cmCofactor3Poly_34_along_coord
plain-language theorem explainer
Along any single squared-edge coordinate, the explicit (3,4) Cayley–Menger cofactor polynomial is differentiable, and its derivative equals the named closed-form partial. Anyone computing tetrahedral dihedral gradients from cofactor polynomials cites this. The proof rewrites the coordinate slice as a shifted cubic via the Taylor polyform, then applies the standard shifted-cubic derivative lemma.
Claim. For every edge index $k \in \{0,\ldots,5\}$ and every squared-edge assignment $a$, the map $t \mapsto P_{3,4}(a[k\mapsto t])$ is differentiable at $t = a_k$, and its derivative equals the explicit partial $\partial_k P_{3,4}(a)$. Here $P_{3,4}$ is the closed-form polynomial for the Cayley–Menger cofactor of index $(3,4)$.
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 is that normal-form polynomial for cofactor $(r,c)$. The companion cmCofactorPartial r c k is the symbolic partial of that polynomial in the $k$-th squared edge. For the $(3,4)$ entry, the update identity cmCofactor3Poly_34_update_polyform already gives the exact Taylor expansion along one coordinate: constant term plus linear partial times $t$, plus a quadratic coefficient that is $-1$ only when $k=0$ and $0$ otherwise, and a vanishing cubic term.
The calculus engine is the local helper hasDerivAt_shifted_cubic: any real cubic written as $A + B(x-x_0) + C(x-x_0)^2 + D(x-x_0)^3$ has derivative $B$ at the base point $x_0$.
proof idea
First prove functional equality: the coordinate slice $t \mapsto P_{3,4}(a[k\mapsto t])$ coincides with the shifted cubic whose coefficients are the base value, the named partial, the quadratic coefficient (if k = 0 then -1 else 0), and cubic coefficient $0$. This is funext plus cmCofactor3Poly_34_update_polyform after the trivial rewrite $a_k + (t-a_k) = t$.
Rewrite the goal along that equality, then apply hasDerivAt_shifted_cubic at base point $a_k$. The linear coefficient is exactly cmCofactorPartial 3 4 k a, which is the claimed derivative.
why it matters
This is the polynomial-side derivative for cofactor $(3,4)$. The immediate parent hasDerivAt_cmCofactor3_34_along_coord transports it to the actual determinant cofactor via the agreement lemma cmCofactor3_34_eq_poly, so dihedral-angle gradients can differentiate the geometric cofactor rather than only its polynomial normal form.
In the broader Recognition geometry stack the module is the cofactor analogue of CayleyMengerDerivatives: explicit partials replace opaque fderiv terms when one differentiates tetrahedral volume and dihedral data with respect to squared edge lengths. The result is pure Euclidean 3-geometry infrastructure; it does not itself invoke the forcing chain (T0–T8), but it supplies the coordinate calculus those geometric identities rely on once edge lengths sit on the $\varphi$-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.