IndisputableMonolith.Geometry.CofactorDerivatives
Canonical Fréchet and directional derivatives of tetrahedral Cayley-Menger cofactors, written as explicit polynomials in the six squared edge lengths. Supplies closed-form derivatives of the dihedral cosine numerator, denominator, and squared cosine along edge charts. Downstream dihedral-angle and Regge-action smoothness proofs cite these lemmas instead of opaque fderiv terms. Proofs reduce to polynomial differentiation and the quotient/chain rules on the realisability cone.
claimOn the open realisability cone of squared edge lengths $s\in\mathbb{R}^6$, the third-order Cayley-Menger cofactor $C_3(s)$ is Fréchet differentiable, with derivative equal to the gradient of its explicit polynomial expansion. Along any $C^1$ edge path, the dihedral cosine squared $\cos^2\theta_e=N/D$ (cofactor numerator over cofactor denominator) admits an explicit directional derivative obtained by the quotient rule.
background
Tetrahedral geometry in the Recognition stack is encoded by the $5\times 5$ Cayley-Menger matrix in the six squared edge coordinates. Cofactors of that matrix give volumes and, via the classical identity, the cosines of dihedral angles: for an edge $e$, if $N$ and $D$ are the appropriate cofactor combinations then $\cos^2\theta_e=N/D$ on the nondegenerate locus.
The sibling module CofactorPolynomial expands every such cofactor into an explicit multivariate polynomial in the six squared edges, so partial derivatives become ordinary polynomial calculus rather than abstract fderiv terms. DihedralCayleyMenger defines the cosine itself from those cofactors. RealisabilityCone fixes the open domain of squared-edge tuples on which the tetrahedron is nondegenerate and the formulas are intended to apply.
This module sits between those definitions and the analytic layer: it records the Fréchet derivative of the cofactor polynomial and the directional derivatives of the dihedral numerator, denominator, and squared cosine along edge charts.
proof idea
Definition-and-lemma module, not a single theorem. The cofactor is identified with its explicit polynomial; Fréchet differentiability and the derivative formula follow from polynomial calculus (Mathlib HasFDerivAt for polynomials and arithmetic). Directional derivatives of the dihedral numerator and the two diagonal cofactor factors are closed-form polynomial gradients contracted with the path velocity. The denominator and $\cos^2\theta$ derivatives are then the quotient rule (and a short hasDerivAt_div helper) on the cone where the denominator is nonzero. Several lemmas package the same identities evaluated on a closed-form path rather than a generic chart.
why it matters in Recognition Science
Dihedral-angle calculus needs $d(\cos\theta)$ before it can form $d\theta=-(1-\cos^2\theta)^{-1/2},d(\cos\theta)$. The downstream module on dihedral derivatives isolates exactly that analytic step and imports these cofactor derivatives as its input. Regge-action smoothness further requires that the nonlinear action stay $C^\infty$ on the nondegenerate cone with arccos arguments bounded away from $\pm 1$; explicit cofactor derivatives are the first link in that chain, feeding the conformal edge chart and the finite Regge action at the flat potential. Without named polynomial partials, those arguments would be stuck with opaque Fréchet terms.
scope and limits
- Does not define dihedral angles or prove $d\theta$ from $d(\cos\theta)$.
- Does not establish smoothness of the full nonlinear Regge action.
- Does not treat degenerate or flat tetrahedra outside the realisability cone.
- Does not derive volume or Gram-matrix identities beyond cofactor differentiation.
- Does not address higher than first directional derivatives along edge paths.
used by (2)
depends on (3)
declarations in this module (34)
-
def
cmCofactor3FDeriv -
theorem
hasFDerivAt_cmCofactor3 -
theorem
hasDerivAt_div -
theorem
hasDerivAt_dihedralCos3Sq_along -
theorem
hasDerivAt_dihedralDenom3_along -
def
dihedralDenom3DerivValue -
def
dihedralCos3SqDerivValue -
def
dihedralNumeratorClosedDeriv -
def
dihedralLeftDiagClosedDeriv -
def
dihedralRightDiagClosedDeriv -
def
dihedralDenom3ClosedDerivValue -
def
dihedralCos3SqClosedFormDeriv -
def
dihedralDenom3Poly -
def
dihedralCofactorProductPoly -
def
dihedralCofactorNumeratorPoly -
def
dihedralCos3SqPoly -
def
dihedralDenom3PolyClosedDerivValue -
def
dihedralCos3SqPolyClosedFormDeriv -
theorem
dihedralDenom3_eq_poly -
theorem
dihedralCos3Sq_eq_poly -
theorem
dihedralDenom3ClosedDerivValue_eq_poly -
theorem
dihedralCos3SqClosedFormDeriv_eq_poly -
theorem
dihedralCofactorPoly_discriminant_eq -
theorem
dihedralDenom3Poly_sq -
theorem
one_sub_dihedralCos3SqPoly_sq_eq -
theorem
sqrt_one_sub_dihedralCos3SqPoly_sq_eq -
theorem
dihedralCofactorProductPoly_pos_of_nonDegenerate -
theorem
dihedralCofactorProductPoly_nonneg_of_nonDegenerate -
theorem
dihedralCofactorProductPoly_ne_zero_of_nonDegenerate -
theorem
dihedralDenom3Poly_pos_of_nonDegenerate -
theorem
dihedralDenom3Poly_ne_zero_of_nonDegenerate -
theorem
dihedralCos3SqClosedFormDeriv_eq_generic -
theorem
hasDerivAt_dihedralCos3Sq_from_cofactors -
theorem
hasDerivAt_dihedralCos3Sq_explicit