IndisputableMonolith.Geometry.DihedralDerivatives

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.Calculus.Deriv.Basic
   3import Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
   4import IndisputableMonolith.Geometry.CofactorDerivatives
   5import IndisputableMonolith.Geometry.DihedralCayleyMenger
   6import IndisputableMonolith.Geometry.DihedralCofactorFormula
   7
   8/-!
   9# Dihedral Angle Derivatives
  10
  11This module isolates the analytic part of the dihedral derivative:
  12once the Cayley-Menger cofactor cosine has a derivative, the angle
  13`θ = arccos(cos θ)` has the standard derivative
  14
  15```
  16dθ = -(1 / sqrt (1 - cos^2)) · d(cos θ).
  17```
  18
  19The remaining hard work is algebraic/geometric: computing the derivative
  20of `dihedralCos3Sq` from the cofactor minors.  That computation belongs
  21to the cofactor derivative layer.  This module provides the exact
  22calculus interface that layer must feed.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Geometry
  27namespace DihedralDerivatives
  28
  29open DihedralCayleyMenger
  30open CofactorDerivatives
  31open DihedralCofactorFormula
  32
  33noncomputable section
  34
  35/-- Dihedral angle as a function of squared edge data. -/
  36def dihedralAngle3Sq (a : CayleyMengerPolynomial.SqEdges) (e : Fin 6) : ℝ :=
  37  Real.arccos (dihedralCos3Sq a e)
  38
  39/-- Generic derivative of `arccos ∘ f`. -/
  40theorem hasDerivAt_arccos_comp
  41    {f : ℝ → ℝ} {f' x : ℝ}
  42    (hf : HasDerivAt f f' x)
  43    (hm : f x ≠ -1) (hp : f x ≠ 1) :
  44    HasDerivAt (fun t : ℝ => Real.arccos (f t))
  45      (-(1 / Real.sqrt (1 - (f x) ^ 2)) * f') x := by
  46  have hacos := Real.hasDerivAt_arccos hm hp
  47  simpa [mul_comm, mul_left_comm, mul_assoc] using hacos.comp x hf
  48
  49/-- Derivative of a dihedral angle along any one-parameter squared-edge path,
  50assuming the cofactor cosine derivative along that path is known and the
  51cosine stays away from the arccos endpoints at the base point. -/
  52theorem hasDerivAt_dihedralAngle3Sq_along
  53    {γ : ℝ → CayleyMengerPolynomial.SqEdges} {x cosDeriv : ℝ} (e : Fin 6)
  54    (hcos : HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e) cosDeriv x)
  55    (hm : dihedralCos3Sq (γ x) e ≠ -1)
  56    (hp : dihedralCos3Sq (γ x) e ≠ 1) :
  57    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (γ t) e)
  58      (-(1 / Real.sqrt (1 - (dihedralCos3Sq (γ x) e) ^ 2)) * cosDeriv) x := by
  59  exact hasDerivAt_arccos_comp hcos hm hp
  60
  61/-- The local derivative package needed for a single dihedral angle. -/
  62structure DihedralAngleDerivativeAlong
  63    (γ : ℝ → CayleyMengerPolynomial.SqEdges) (e : Fin 6) (x : ℝ) where
  64  cosDeriv : ℝ
  65  cos_hasDerivAt :
  66    HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e) cosDeriv x
  67  cos_ne_neg_one : dihedralCos3Sq (γ x) e ≠ -1
  68  cos_ne_one : dihedralCos3Sq (γ x) e ≠ 1
  69
  70/-- A packaged derivative theorem for downstream Regge modules. -/
  71theorem DihedralAngleDerivativeAlong.angle_hasDerivAt
  72    {γ : ℝ → CayleyMengerPolynomial.SqEdges} {e : Fin 6} {x : ℝ}
  73    (D : DihedralAngleDerivativeAlong γ e x) :
  74    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (γ t) e)
  75      (-(1 / Real.sqrt (1 - (dihedralCos3Sq (γ x) e) ^ 2)) * D.cosDeriv) x :=
  76  hasDerivAt_dihedralAngle3Sq_along e D.cos_hasDerivAt D.cos_ne_neg_one D.cos_ne_one
  77
  78/-- Interior range is enough to satisfy the endpoint hypotheses for arccos. -/
  79theorem arccos_endpoint_hypotheses_of_interior {c : ℝ}
  80    (hlo : -1 < c) (hhi : c < 1) : c ≠ -1 ∧ c ≠ 1 := by
  81  constructor
  82  · intro h
  83    linarith
  84  · intro h
  85    linarith
  86
  87/-- Endpoint hypotheses for a cofactor cosine coming from a realized
  88tetrahedron, provided the endpoint cases are excluded. -/
  89theorem arccos_endpoint_hypotheses_of_realized_ne_endpoints
  90    (T : TetrahedronRealization.RealizedTet) (e : Fin 6)
  91    (hneg : dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ -1)
  92    (hpos : dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ 1) :
  93    dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ -1 ∧
  94      dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ 1 :=
  95  ⟨hneg, hpos⟩
  96
  97/-- Dihedral angle derivative generated directly from Cayley-Menger cofactor
  98derivatives for the numerator and the two diagonal denominator cofactors. -/
  99theorem hasDerivAt_dihedralAngle3Sq_from_cofactors
 100    {γ : ℝ → CayleyMengerPolynomial.SqEdges} {x num' pp' qq' : ℝ} (e : Fin 6)
 101    (hnum : HasDerivAt
 102      (fun t : ℝ =>
 103        let p := (oppositeCMVertices e).1
 104        let q := (oppositeCMVertices e).2
 105        CayleyMengerMatrix.cmCofactor3 (γ t) p q) num' x)
 106    (hpp : HasDerivAt
 107      (fun t : ℝ =>
 108        let p := (oppositeCMVertices e).1
 109        CayleyMengerMatrix.cmCofactor3 (γ t) p p) pp' x)
 110    (hqq : HasDerivAt
 111      (fun t : ℝ =>
 112        let q := (oppositeCMVertices e).2
 113        CayleyMengerMatrix.cmCofactor3 (γ t) q q) qq' x)
 114    (hprod_ne :
 115      (let p := (oppositeCMVertices e).1
 116       let q := (oppositeCMVertices e).2
 117       CayleyMengerMatrix.cmCofactor3 (γ x) p p *
 118         CayleyMengerMatrix.cmCofactor3 (γ x) q q) ≠ 0)
 119    (hden_ne : dihedralDenom3 (γ x) e ≠ 0)
 120    (hm : dihedralCos3Sq (γ x) e ≠ -1)
 121    (hp : dihedralCos3Sq (γ x) e ≠ 1) :
 122    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (γ t) e)
 123      (-(1 / Real.sqrt (1 - (dihedralCos3Sq (γ x) e) ^ 2)) *
 124        dihedralCos3SqDerivValue γ x num'
 125          (dihedralDenom3DerivValue γ x pp' qq' e) e) x := by
 126  exact hasDerivAt_dihedralAngle3Sq_along e
 127    (hasDerivAt_dihedralCos3Sq_from_cofactors e hnum hpp hqq hprod_ne hden_ne)
 128    hm hp
 129
 130/-! ## Closed-form derivative values
 131
 132The next definition is the concrete arccos-chain-rule value obtained after
 133substituting the cofactor partial polynomials exposed in
 134`CofactorDerivatives`.  The actual `HasDerivAt` theorem reduces to proving
 135the cofactor-polynomial coordinate derivative for the needed minors.
 136-/
 137
 138/-- Closed-form coordinate derivative value for the tetrahedral dihedral
 139angle, as a function of squared edge coordinates. -/
 140def dihedralAngle3SqClosedFormDeriv
 141    (a : CayleyMengerPolynomial.SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
 142  -(1 / Real.sqrt (1 - (dihedralCos3Sq a e) ^ 2)) *
 143    dihedralCos3SqClosedFormDeriv a e k
 144
 145/-- The closed-form angle derivative is the arccos chain-rule multiplier
 146applied to the closed-form cofactor-ratio derivative. -/
 147theorem dihedralAngle3SqClosedFormDeriv_def
 148    (a : CayleyMengerPolynomial.SqEdges) (e : Fin 6) (k : Fin 6) :
 149    dihedralAngle3SqClosedFormDeriv a e k =
 150      -(1 / Real.sqrt (1 - (dihedralCos3Sq a e) ^ 2)) *
 151        dihedralCos3SqClosedFormDeriv a e k := rfl
 152
 153/-- Explicit coordinate derivative of the cofactor-defined tetrahedral
 154dihedral angle. -/
 155theorem hasDerivAt_dihedralAngle3Sq_explicit
 156    (a : CayleyMengerPolynomial.SqEdges) (e k : Fin 6)
 157    (hprod_ne :
 158      (let p := (oppositeCMVertices e).1
 159       let q := (oppositeCMVertices e).2
 160       CayleyMengerMatrix.cmCofactor3 a p p *
 161         CayleyMengerMatrix.cmCofactor3 a q q) ≠ 0)
 162    (hden_ne : dihedralDenom3 a e ≠ 0)
 163    (hm : dihedralCos3Sq a e ≠ -1)
 164    (hp : dihedralCos3Sq a e ≠ 1) :
 165    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (Function.update a k t) e)
 166      (dihedralAngle3SqClosedFormDeriv a e k) (a k) := by
 167  have hbase :
 168      Function.update a k (a k) = a := by
 169    funext i
 170    by_cases hi : i = k <;> simp [Function.update, hi]
 171  have hm' : dihedralCos3Sq (Function.update a k (a k)) e ≠ -1 := by
 172    simpa [hbase] using hm
 173  have hp' : dihedralCos3Sq (Function.update a k (a k)) e ≠ 1 := by
 174    simpa [hbase] using hp
 175  simpa [dihedralAngle3SqClosedFormDeriv] using
 176    hasDerivAt_dihedralAngle3Sq_along e
 177      (hasDerivAt_dihedralCos3Sq_explicit a e k hprod_ne hden_ne)
 178      hm' hp'
 179
 180end
 181
 182end DihedralDerivatives
 183end Geometry
 184end IndisputableMonolith
 185