IndisputableMonolith.Geometry.CofactorDerivatives

   1import Mathlib.Analysis.Calculus.Deriv.Basic
   2import Mathlib.Analysis.Calculus.Deriv.Inv
   3import Mathlib.Analysis.SpecialFunctions.Sqrt
   4import Mathlib.Tactic
   5import IndisputableMonolith.Geometry.DihedralCayleyMenger
   6import IndisputableMonolith.Geometry.RealisabilityCone
   7import IndisputableMonolith.Geometry.CofactorPolynomial
   8
   9/-!
  10# Cayley-Menger Cofactor Derivative Interfaces
  11
  12This module exposes derivative hooks for Cayley-Menger cofactors and the
  13dihedral cofactor ratio.  The hard symbolic derivative simplifications
  14are still downstream, but the calculus layer is no longer implicit.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Geometry
  19namespace CofactorDerivatives
  20
  21open CayleyMengerPolynomial
  22open CayleyMengerMatrix
  23open DihedralCayleyMenger
  24open CofactorPolynomial
  25
  26noncomputable section
  27
  28/-- Canonical Fréchet derivative of a Cayley-Menger cofactor. -/
  29def cmCofactor3FDeriv (r c : Fin 5) (a : SqEdges) : SqEdges →L[ℝ] ℝ :=
  30  fderiv ℝ (fun x : SqEdges => cmCofactor3 x r c) a
  31
  32/-- Cofactors are differentiable everywhere because they are smooth
  33polynomial functions of the squared-edge coordinates. -/
  34theorem hasFDerivAt_cmCofactor3 (r c : Fin 5) (a : SqEdges) :
  35    HasFDerivAt (fun x : SqEdges => cmCofactor3 x r c)
  36      (cmCofactor3FDeriv r c a) a := by
  37  unfold cmCofactor3FDeriv
  38  exact ((cmCofactor3_contDiff 1 r c).differentiable_one a).hasFDerivAt
  39
  40/-- Generic derivative of a quotient `num / den` along a real parameter. -/
  41theorem hasDerivAt_div
  42    {num den : ℝ → ℝ} {num' den' x : ℝ}
  43    (hnum : HasDerivAt num num' x)
  44    (hden : HasDerivAt den den' x)
  45    (hden_ne : den x ≠ 0) :
  46    HasDerivAt (fun t : ℝ => num t / den t)
  47      ((num' * den x - num x * den') / (den x) ^ 2) x := by
  48  have h := hnum.div hden hden_ne
  49  convert h using 1
  50
  51/-- Derivative of `dihedralCos3Sq` along a squared-edge path, provided the
  52numerator and denominator derivatives along that path. -/
  53theorem hasDerivAt_dihedralCos3Sq_along
  54    {γ : ℝ → SqEdges} {x num' den' : ℝ} (e : Fin 6)
  55    (hnum : HasDerivAt
  56      (fun t : ℝ =>
  57        let p := (oppositeCMVertices e).1
  58        let q := (oppositeCMVertices e).2
  59        cmCofactor3 (γ t) p q) num' x)
  60    (hden : HasDerivAt (fun t : ℝ => dihedralDenom3 (γ t) e) den' x)
  61    (hden_ne : dihedralDenom3 (γ x) e ≠ 0) :
  62    HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e)
  63      ((num' * dihedralDenom3 (γ x) e -
  64          (let p := (oppositeCMVertices e).1
  65           let q := (oppositeCMVertices e).2
  66           cmCofactor3 (γ x) p q) * den') /
  67        (dihedralDenom3 (γ x) e) ^ 2) x := by
  68  unfold dihedralCos3Sq
  69  exact hasDerivAt_div hnum hden hden_ne
  70
  71/-- Derivative of the square-root denominator
  72`sqrt(C_pp * C_qq)` along a squared-edge path. -/
  73theorem hasDerivAt_dihedralDenom3_along
  74    {γ : ℝ → SqEdges} {x pp' qq' : ℝ} (e : Fin 6)
  75    (hpp : HasDerivAt
  76      (fun t : ℝ =>
  77        let p := (oppositeCMVertices e).1
  78        cmCofactor3 (γ t) p p) pp' x)
  79    (hqq : HasDerivAt
  80      (fun t : ℝ =>
  81        let q := (oppositeCMVertices e).2
  82        cmCofactor3 (γ t) q q) qq' x)
  83    (hprod_ne :
  84      (let p := (oppositeCMVertices e).1
  85       let q := (oppositeCMVertices e).2
  86       cmCofactor3 (γ x) p p * cmCofactor3 (γ x) q q) ≠ 0) :
  87    HasDerivAt (fun t : ℝ => dihedralDenom3 (γ t) e)
  88      (((let p := (oppositeCMVertices e).1
  89         let q := (oppositeCMVertices e).2
  90         pp' * cmCofactor3 (γ x) q q +
  91           cmCofactor3 (γ x) p p * qq') /
  92        (2 * dihedralDenom3 (γ x) e))) x := by
  93  unfold dihedralDenom3
  94  let p := (oppositeCMVertices e).1
  95  let q := (oppositeCMVertices e).2
  96  have hprod : HasDerivAt
  97      (fun t : ℝ => cmCofactor3 (γ t) p p * cmCofactor3 (γ t) q q)
  98      (pp' * cmCofactor3 (γ x) q q + cmCofactor3 (γ x) p p * qq') x := by
  99    exact hpp.mul hqq
 100  have hsqrt := Real.hasDerivAt_sqrt hprod_ne
 101  have hcomp := hsqrt.comp x hprod
 102  simpa [p, q, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using hcomp
 103
 104/-- Value of the derivative of the cofactor denominator along a path, given
 105the derivatives of the two diagonal cofactors. -/
 106def dihedralDenom3DerivValue
 107    (γ : ℝ → SqEdges) (x pp' qq' : ℝ) (e : Fin 6) : ℝ :=
 108  let p := (oppositeCMVertices e).1
 109  let q := (oppositeCMVertices e).2
 110  (pp' * cmCofactor3 (γ x) q q + cmCofactor3 (γ x) p p * qq') /
 111    (2 * dihedralDenom3 (γ x) e)
 112
 113/-- Value of the derivative of the cofactor-ratio cosine along a path. -/
 114def dihedralCos3SqDerivValue
 115    (γ : ℝ → SqEdges) (x num' den' : ℝ) (e : Fin 6) : ℝ :=
 116  let p := (oppositeCMVertices e).1
 117  let q := (oppositeCMVertices e).2
 118  (num' * dihedralDenom3 (γ x) e - cmCofactor3 (γ x) p q * den') /
 119    (dihedralDenom3 (γ x) e) ^ 2
 120
 121/-! ## Closed-form coordinate derivative values
 122
 123The next definitions specialize the abstract numerator/denominator derivative
 124values above to the explicit cofactor partial polynomials from
 125`CofactorPolynomial`.  They are the concrete expressions used by the
 126Schläfli and Hessian closure targets.
 127-/
 128
 129/-- Closed-form derivative of the numerator cofactor for edge `e` with
 130respect to squared-edge coordinate `k`. -/
 131def dihedralNumeratorClosedDeriv (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 132  let p := (oppositeCMVertices e).1
 133  let q := (oppositeCMVertices e).2
 134  cmCofactorPartial p q k a
 135
 136/-- Closed-form derivative of the left diagonal denominator cofactor. -/
 137def dihedralLeftDiagClosedDeriv (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 138  let p := (oppositeCMVertices e).1
 139  cmCofactorPartial p p k a
 140
 141/-- Closed-form derivative of the right diagonal denominator cofactor. -/
 142def dihedralRightDiagClosedDeriv (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 143  let q := (oppositeCMVertices e).2
 144  cmCofactorPartial q q k a
 145
 146/-- Closed-form derivative of the square-root cofactor denominator. -/
 147def dihedralDenom3ClosedDerivValue (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 148  let p := (oppositeCMVertices e).1
 149  let q := (oppositeCMVertices e).2
 150  (dihedralLeftDiagClosedDeriv a e k * cmCofactor3 a q q +
 151      cmCofactor3 a p p * dihedralRightDiagClosedDeriv a e k) /
 152    (2 * dihedralDenom3 a e)
 153
 154/-- Closed-form coordinate derivative value for the cofactor-ratio cosine. -/
 155def dihedralCos3SqClosedFormDeriv (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 156  let p := (oppositeCMVertices e).1
 157  let q := (oppositeCMVertices e).2
 158  (dihedralNumeratorClosedDeriv a e k * dihedralDenom3 a e -
 159      cmCofactor3 a p q * dihedralDenom3ClosedDerivValue a e k) /
 160    (dihedralDenom3 a e) ^ 2
 161
 162/-- Polynomial-cofactor denominator for the same cofactor cosine.  This is
 163definitionally lighter than `dihedralDenom3` because it avoids determinant
 164normalization. -/
 165def dihedralDenom3Poly (a : SqEdges) (e : Fin 6) : ℝ :=
 166  let p := (oppositeCMVertices e).1
 167  let q := (oppositeCMVertices e).2
 168  Real.sqrt (cmCofactor3Poly p p a * cmCofactor3Poly q q a)
 169
 170/-- Product of the two diagonal polynomial cofactors used in a dihedral
 171cosine denominator. -/
 172def dihedralCofactorProductPoly (a : SqEdges) (e : Fin 6) : ℝ :=
 173  let p := (oppositeCMVertices e).1
 174  let q := (oppositeCMVertices e).2
 175  cmCofactor3Poly p p a * cmCofactor3Poly q q a
 176
 177/-- Numerator polynomial cofactor used in a dihedral cosine. -/
 178def dihedralCofactorNumeratorPoly (a : SqEdges) (e : Fin 6) : ℝ :=
 179  let p := (oppositeCMVertices e).1
 180  let q := (oppositeCMVertices e).2
 181  cmCofactor3Poly p q a
 182
 183/-- Polynomial-cofactor cosine, avoiding determinant normalization. -/
 184def dihedralCos3SqPoly (a : SqEdges) (e : Fin 6) : ℝ :=
 185  dihedralCofactorNumeratorPoly a e / dihedralDenom3Poly a e
 186
 187/-- Polynomial-cofactor derivative of the square-root denominator. -/
 188def dihedralDenom3PolyClosedDerivValue (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 189  let p := (oppositeCMVertices e).1
 190  let q := (oppositeCMVertices e).2
 191  (cmCofactorPartial p p k a * cmCofactor3Poly q q a +
 192      cmCofactor3Poly p p a * cmCofactorPartial q q k a) /
 193    (2 * dihedralDenom3Poly a e)
 194
 195/-- Polynomial-cofactor closed-form derivative of the cofactor-ratio cosine. -/
 196def dihedralCos3SqPolyClosedFormDeriv (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 197  let p := (oppositeCMVertices e).1
 198  let q := (oppositeCMVertices e).2
 199  (cmCofactorPartial p q k a * dihedralDenom3Poly a e -
 200      cmCofactor3Poly p q a * dihedralDenom3PolyClosedDerivValue a e k) /
 201    (dihedralDenom3Poly a e) ^ 2
 202
 203theorem dihedralDenom3_eq_poly (a : SqEdges) (e : Fin 6) :
 204    dihedralDenom3 a e = dihedralDenom3Poly a e := by
 205  unfold dihedralDenom3 dihedralDenom3Poly
 206  simp_rw [cmCofactor3_eq_poly]
 207
 208theorem dihedralCos3Sq_eq_poly (a : SqEdges) (e : Fin 6) :
 209    dihedralCos3Sq a e = dihedralCos3SqPoly a e := by
 210  unfold dihedralCos3Sq dihedralCos3SqPoly dihedralCofactorNumeratorPoly
 211  rw [dihedralDenom3_eq_poly]
 212  simp_rw [cmCofactor3_eq_poly]
 213
 214theorem dihedralDenom3ClosedDerivValue_eq_poly (a : SqEdges) (e : Fin 6) (k : Fin 6) :
 215    dihedralDenom3ClosedDerivValue a e k =
 216      dihedralDenom3PolyClosedDerivValue a e k := by
 217  unfold dihedralDenom3ClosedDerivValue dihedralDenom3PolyClosedDerivValue
 218    dihedralLeftDiagClosedDeriv dihedralRightDiagClosedDeriv
 219  rw [dihedralDenom3_eq_poly]
 220  simp_rw [cmCofactor3_eq_poly]
 221
 222theorem dihedralCos3SqClosedFormDeriv_eq_poly (a : SqEdges) (e : Fin 6) (k : Fin 6) :
 223    dihedralCos3SqClosedFormDeriv a e k =
 224      dihedralCos3SqPolyClosedFormDeriv a e k := by
 225  unfold dihedralCos3SqClosedFormDeriv dihedralCos3SqPolyClosedFormDeriv
 226    dihedralNumeratorClosedDeriv
 227  rw [dihedralDenom3_eq_poly, dihedralDenom3ClosedDerivValue_eq_poly]
 228  simp_rw [cmCofactor3_eq_poly]
 229
 230/-- Polynomial cofactor discriminant written in the notation of an edge's
 231cofactor cosine denominator. -/
 232theorem dihedralCofactorPoly_discriminant_eq (a : SqEdges) (e : Fin 6) :
 233    let p := (oppositeCMVertices e).1
 234    let q := (oppositeCMVertices e).2
 235    cmCofactor3Poly p p a * cmCofactor3Poly q q a -
 236        cmCofactor3Poly p q a ^ 2 =
 237      2 * cm3 a * a e :=
 238  cmCofactor_discriminant_eq a e
 239
 240theorem dihedralDenom3Poly_sq
 241    (a : SqEdges) (e : Fin 6)
 242    (hprod_nonneg : 0 ≤ dihedralCofactorProductPoly a e) :
 243    dihedralDenom3Poly a e ^ 2 = dihedralCofactorProductPoly a e := by
 244  unfold dihedralDenom3Poly dihedralCofactorProductPoly
 245  exact Real.sq_sqrt hprod_nonneg
 246
 247/-- Radical-free expression for `1 - cos^2` using the Cayley cofactor
 248discriminant identity. -/
 249theorem one_sub_dihedralCos3SqPoly_sq_eq
 250    (a : SqEdges) (e : Fin 6)
 251    (hprod_nonneg : 0 ≤ dihedralCofactorProductPoly a e)
 252    (hprod_ne : dihedralCofactorProductPoly a e ≠ 0)
 253    (hden_ne : dihedralDenom3Poly a e ≠ 0) :
 254    1 - (dihedralCos3SqPoly a e) ^ 2 =
 255      (2 * cm3 a * a e) / dihedralCofactorProductPoly a e := by
 256  have hden_sq := dihedralDenom3Poly_sq a e hprod_nonneg
 257  unfold dihedralCos3SqPoly dihedralCofactorNumeratorPoly
 258  calc
 259    1 - (dihedralCofactorNumeratorPoly a e / dihedralDenom3Poly a e) ^ 2
 260        = (dihedralCofactorProductPoly a e - dihedralCofactorNumeratorPoly a e ^ 2) /
 261            dihedralCofactorProductPoly a e := by
 262          field_simp [hden_ne, hprod_ne]
 263          rw [← hden_sq]
 264          ring
 265    _ = (2 * cm3 a * a e) / dihedralCofactorProductPoly a e := by
 266          unfold dihedralCofactorProductPoly dihedralCofactorNumeratorPoly
 267          rw [dihedralCofactorPoly_discriminant_eq]
 268
 269/-- Square-root normalization of the arccos denominator after applying the
 270Cayley cofactor discriminant identity. -/
 271theorem sqrt_one_sub_dihedralCos3SqPoly_sq_eq
 272    (a : SqEdges) (e : Fin 6)
 273    (hprod_nonneg : 0 ≤ dihedralCofactorProductPoly a e)
 274    (hprod_ne : dihedralCofactorProductPoly a e ≠ 0)
 275    (hden_ne : dihedralDenom3Poly a e ≠ 0)
 276    (hnum_nonneg : 0 ≤ 2 * cm3 a * a e) :
 277    Real.sqrt (1 - (dihedralCos3SqPoly a e) ^ 2) =
 278      Real.sqrt (2 * cm3 a * a e) / dihedralDenom3Poly a e := by
 279  rw [one_sub_dihedralCos3SqPoly_sq_eq a e hprod_nonneg hprod_ne hden_ne]
 280  rw [Real.sqrt_div hnum_nonneg]
 281  simp [dihedralDenom3Poly, dihedralCofactorProductPoly]
 282
 283/-- Nondegenerate tetrahedra have positive polynomial cofactor denominator
 284products for every dihedral edge. -/
 285theorem dihedralCofactorProductPoly_pos_of_nonDegenerate
 286    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
 287    0 < dihedralCofactorProductPoly T.sqEdge e := by
 288  have hdisc := dihedralCofactorPoly_discriminant_eq T.sqEdge e
 289  have hdisc' :
 290      dihedralCofactorProductPoly T.sqEdge e -
 291          dihedralCofactorNumeratorPoly T.sqEdge e ^ 2 =
 292        2 * cm3 T.sqEdge * T.sqEdge e := by
 293    simpa [dihedralCofactorProductPoly, dihedralCofactorNumeratorPoly] using hdisc
 294  have hpos : 0 < 2 * cm3 T.sqEdge * T.sqEdge e := by
 295    nlinarith [T.cm_pos, T.sqEdge_pos e]
 296  have hsq : 0 ≤ dihedralCofactorNumeratorPoly T.sqEdge e ^ 2 := sq_nonneg _
 297  nlinarith
 298
 299theorem dihedralCofactorProductPoly_nonneg_of_nonDegenerate
 300    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
 301    0 ≤ dihedralCofactorProductPoly T.sqEdge e :=
 302  le_of_lt (dihedralCofactorProductPoly_pos_of_nonDegenerate T e)
 303
 304theorem dihedralCofactorProductPoly_ne_zero_of_nonDegenerate
 305    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
 306    dihedralCofactorProductPoly T.sqEdge e ≠ 0 :=
 307  ne_of_gt (dihedralCofactorProductPoly_pos_of_nonDegenerate T e)
 308
 309theorem dihedralDenom3Poly_pos_of_nonDegenerate
 310    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
 311    0 < dihedralDenom3Poly T.sqEdge e := by
 312  unfold dihedralDenom3Poly
 313  rw [Real.sqrt_pos]
 314  simpa [dihedralCofactorProductPoly] using
 315    dihedralCofactorProductPoly_pos_of_nonDegenerate T e
 316
 317theorem dihedralDenom3Poly_ne_zero_of_nonDegenerate
 318    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
 319    dihedralDenom3Poly T.sqEdge e ≠ 0 :=
 320  ne_of_gt (dihedralDenom3Poly_pos_of_nonDegenerate T e)
 321
 322/-- The closed-form cosine derivative is exactly the generic quotient
 323derivative value after substituting the explicit cofactor partials. -/
 324theorem dihedralCos3SqClosedFormDeriv_eq_generic
 325    (a : SqEdges) (e : Fin 6) (k : Fin 6) :
 326    dihedralCos3SqClosedFormDeriv a e k =
 327      dihedralCos3SqDerivValue (fun _ : ℝ => a) 0
 328        (dihedralNumeratorClosedDeriv a e k)
 329        (dihedralDenom3ClosedDerivValue a e k) e := by
 330  unfold dihedralCos3SqClosedFormDeriv dihedralCos3SqDerivValue
 331  simp
 332
 333/-- Dihedral cosine derivative from the numerator and diagonal cofactor
 334derivatives. -/
 335theorem hasDerivAt_dihedralCos3Sq_from_cofactors
 336    {γ : ℝ → SqEdges} {x num' pp' qq' : ℝ} (e : Fin 6)
 337    (hnum : HasDerivAt
 338      (fun t : ℝ =>
 339        let p := (oppositeCMVertices e).1
 340        let q := (oppositeCMVertices e).2
 341        cmCofactor3 (γ t) p q) num' x)
 342    (hpp : HasDerivAt
 343      (fun t : ℝ =>
 344        let p := (oppositeCMVertices e).1
 345        cmCofactor3 (γ t) p p) pp' x)
 346    (hqq : HasDerivAt
 347      (fun t : ℝ =>
 348        let q := (oppositeCMVertices e).2
 349        cmCofactor3 (γ t) q q) qq' x)
 350    (hprod_ne :
 351      (let p := (oppositeCMVertices e).1
 352       let q := (oppositeCMVertices e).2
 353       cmCofactor3 (γ x) p p * cmCofactor3 (γ x) q q) ≠ 0)
 354    (hden_ne : dihedralDenom3 (γ x) e ≠ 0) :
 355    HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e)
 356      (dihedralCos3SqDerivValue γ x num'
 357        (dihedralDenom3DerivValue γ x pp' qq' e) e) x := by
 358  refine hasDerivAt_dihedralCos3Sq_along e hnum ?_ hden_ne
 359  simpa [dihedralDenom3DerivValue] using
 360    hasDerivAt_dihedralDenom3_along e hpp hqq hprod_ne
 361
 362/-- Explicit coordinate derivative of the Cayley-Menger cofactor cosine. -/
 363theorem hasDerivAt_dihedralCos3Sq_explicit
 364    (a : SqEdges) (e k : Fin 6)
 365    (hprod_ne :
 366      (let p := (oppositeCMVertices e).1
 367       let q := (oppositeCMVertices e).2
 368       cmCofactor3 a p p * cmCofactor3 a q q) ≠ 0)
 369    (hden_ne : dihedralDenom3 a e ≠ 0) :
 370    HasDerivAt (fun t : ℝ => dihedralCos3Sq (Function.update a k t) e)
 371      (dihedralCos3SqClosedFormDeriv a e k) (a k) := by
 372  let p := (oppositeCMVertices e).1
 373  let q := (oppositeCMVertices e).2
 374  have hnum :
 375      HasDerivAt
 376        (fun t : ℝ =>
 377          let p := (oppositeCMVertices e).1
 378          let q := (oppositeCMVertices e).2
 379          cmCofactor3 (Function.update a k t) p q)
 380        (dihedralNumeratorClosedDeriv a e k) (a k) := by
 381    simpa [dihedralNumeratorClosedDeriv, p, q] using
 382      hasDerivAt_cmCofactor3_along_coord p q k a
 383  have hpp :
 384      HasDerivAt
 385        (fun t : ℝ =>
 386          let p := (oppositeCMVertices e).1
 387          cmCofactor3 (Function.update a k t) p p)
 388        (dihedralLeftDiagClosedDeriv a e k) (a k) := by
 389    simpa [dihedralLeftDiagClosedDeriv, p] using
 390      hasDerivAt_cmCofactor3_along_coord p p k a
 391  have hqq :
 392      HasDerivAt
 393        (fun t : ℝ =>
 394          let q := (oppositeCMVertices e).2
 395          cmCofactor3 (Function.update a k t) q q)
 396        (dihedralRightDiagClosedDeriv a e k) (a k) := by
 397    simpa [dihedralRightDiagClosedDeriv, q] using
 398      hasDerivAt_cmCofactor3_along_coord q q k a
 399  have hbase :
 400      Function.update a k (a k) = a := by
 401    funext i
 402    by_cases hi : i = k <;> simp [Function.update, hi]
 403  have h :=
 404    hasDerivAt_dihedralCos3Sq_from_cofactors
 405      (γ := fun t : ℝ => Function.update a k t) (x := a k)
 406      (num' := dihedralNumeratorClosedDeriv a e k)
 407      (pp' := dihedralLeftDiagClosedDeriv a e k)
 408      (qq' := dihedralRightDiagClosedDeriv a e k)
 409      e hnum hpp hqq ?_ ?_
 410  · simpa [dihedralCos3SqClosedFormDeriv, dihedralCos3SqDerivValue,
 411      dihedralDenom3ClosedDerivValue, dihedralDenom3DerivValue,
 412      dihedralNumeratorClosedDeriv, dihedralLeftDiagClosedDeriv,
 413      dihedralRightDiagClosedDeriv, hbase, p, q] using h
 414  · simpa [hbase, p, q] using hprod_ne
 415  · simpa [hbase] using hden_ne
 416
 417end
 418
 419end CofactorDerivatives
 420end Geometry
 421end IndisputableMonolith
 422