hasDerivAt_div
plain-language theorem explainer
Quotient rule for real one-variable derivatives: if num and den are differentiable at x and den(x) ≠ 0, then num/den is differentiable with the classical formula (num' den − num den')/den². Geometry code that differentiates Cayley–Menger cofactor ratios cites it. Proof is a one-line Mathlib HasDerivAt.div application plus convert.
Claim. Let $\mathrm{num},\mathrm{den}:\mathbb{R}\to\mathbb{R}$ and $x,\mathrm{num}',\mathrm{den}'\in\mathbb{R}$. If $\mathrm{num}$ has derivative $\mathrm{num}'$ at $x$, $\mathrm{den}$ has derivative $\mathrm{den}'$ at $x$, and $\mathrm{den}(x)\neq 0$, then $t\mapsto \mathrm{num}(t)/\mathrm{den}(t)$ has derivative $(\mathrm{num}'\cdot\mathrm{den}(x)-\mathrm{num}(x)\cdot\mathrm{den}')/(\mathrm{den}(x))^2$ at $x$.
background
The module supplies calculus hooks for Cayley–Menger cofactors and the dihedral cofactor ratio. Hard symbolic simplifications sit downstream; this layer makes differentiability explicit rather than implicit.
The tetrahedral dihedral cosine is defined as a ratio of CM data: $\mathrm{dihedralCos3Sq}(a,e)=\mathrm{cmCofactor3}(a,p,q)/\mathrm{dihedralDenom3}(a,e)$ for opposite vertices $(p,q)$ of edge $e$. Differentiating that ratio along a squared-edge path therefore needs a clean quotient rule on $\mathbb{R}\to\mathbb{R}$.
Mathlib already provides HasDerivAt.div. This lemma packages that fact in the exact algebraic shape the cofactor path derivatives expect.
proof idea
Term-mode wrapper. Apply Mathlib's quotient rule HasDerivAt.div to the two given derivative hypotheses and the nonzero-denominator guard, obtaining differentiability of num/den at x. Then convert ... using 1 aligns the Mathlib derivative expression with the target formula (num' * den x - num x * den') / (den x)^2 (definitional equality of the two written forms).
why it matters
Immediate parent is hasDerivAt_dihedralCos3Sq_along, which differentiates the tetrahedral dihedral cosine along a squared-edge path once numerator and denominator path derivatives are known. That is the calculus step connecting CM cofactor polynomials to first-order variation of dihedral angles.
In the broader RS geometry stack, dihedral data from Cayley–Menger determinants feed realisability and continuum residual arguments. Making the quotient derivative an explicit proved interface (rather than an inline Mathlib call) keeps the cofactor-derivative module self-contained and matches the module goal: expose derivative hooks so later closed-form simplifications can cite a stable lemma.
No forcing-chain landmark (T5–T8, RCL, phi) is proved here; this is pure real calculus scaffolding under the geometry domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.