IndisputableMonolith.Geometry.SchlaefliTetrahedron

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   3import Mathlib.Analysis.SpecialFunctions.Sqrt
   4import Mathlib.Analysis.Calculus.Deriv.Basic
   5import IndisputableMonolith.Geometry.CayleyMengerDerivatives
   6import IndisputableMonolith.Geometry.DihedralDerivatives
   7import IndisputableMonolith.Geometry.ReggeRigorousFoundation
   8
   9/-!
  10# Schläfli Identity for a Single Tetrahedron
  11
  12This module pins down the local tetrahedral Schläfli identity in the
  13notation used by the Regge component theorem.
  14
  15It proves the calculus pieces we need now:
  16
  17* the volume-squared relation `V² = cm3 / 288`;
  18* the derivative of `sqrt (cm3 / 288)` along a one-parameter path, assuming
  19  the Cayley-Menger derivative along that path is known;
  20* the exact Euclidean local Schläfli statement `Σ_e L_e dθ_e = 0` as a
  21  structure field.
  22
  23The remaining hard theorem is to fill that structure from the cofactor
  24dihedral derivatives.  This file makes that target precise and connects it
  25to the existing `ReggeRigorousFoundation.Schlaefli3DIdentity` statement.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Geometry
  30namespace SchlaefliTetrahedron
  31
  32open CayleyMengerPolynomial CayleyMengerDerivatives
  33open ReggeRigorousFoundation DihedralDerivatives
  34
  35noncomputable section
  36
  37/-- Tetrahedral volume as a function of squared edge data:
  38`V = sqrt (CM_3 / 288)`. -/
  39def volume3SqEdges (a : SqEdges) : ℝ :=
  40  Real.sqrt (cm3 a / 288)
  41
  42/-- The squared-volume identity, by definition of `volume3SqEdges`. -/
  43theorem volume3SqEdges_sq (a : SqEdges) (hcm : 0 ≤ cm3 a / 288) :
  44    volume3SqEdges a ^ 2 = cm3 a / 288 := by
  45  unfold volume3SqEdges
  46  exact Real.sq_sqrt hcm
  47
  48/-- Generic derivative of `sqrt (f / 288)` along a real parameter. -/
  49theorem hasDerivAt_volume3_of_hasDerivAt_cm3
  50    {f : ℝ → ℝ} {f' x : ℝ}
  51    (hf : HasDerivAt f f' x)
  52    (hpos : 0 < f x / 288) :
  53    HasDerivAt (fun t : ℝ => Real.sqrt (f t / 288))
  54      (f' / (576 * Real.sqrt (f x / 288))) x := by
  55  have hdiv : HasDerivAt (fun t : ℝ => f t / 288) (f' / 288) x := by
  56    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using
  57      hf.const_mul ((288 : ℝ)⁻¹)
  58  have hsqrt := Real.hasDerivAt_sqrt (ne_of_gt hpos)
  59  have hcomp := hsqrt.comp x hdiv
  60  convert hcomp using 1
  61  field_simp [hpos.ne']
  62  ring
  63
  64/-- Derivative of tetrahedral volume along a squared-edge path, assuming
  65the derivative of `cm3` along the path. -/
  66theorem hasDerivAt_volume3_along
  67    {γ : ℝ → SqEdges} {x cmDeriv : ℝ}
  68    (hcm : HasDerivAt (fun t : ℝ => cm3 (γ t)) cmDeriv x)
  69    (hpos : 0 < cm3 (γ x) / 288) :
  70    HasDerivAt (fun t : ℝ => volume3SqEdges (γ t))
  71      (cmDeriv / (576 * Real.sqrt (cm3 (γ x) / 288))) x :=
  72  hasDerivAt_volume3_of_hasDerivAt_cm3 hcm hpos
  73
  74/-- The local tetrahedral Schläfli derivative data at a nondegenerate
  75tetrahedron.  `dihedralDeriv e e'` means `∂θ_e/∂L_e'`; `volumeDeriv e'`
  76is retained as auxiliary volume derivative data for downstream Hessian
  77computations.  The Euclidean Schläfli identity itself is the vanishing of
  78`Σ_e L_e dθ_e`; it is not a volume-derivative formula. -/
  79structure TetraSchlaefliDerivativeData (T : NonDegenerateTet) where
  80  dihedralDeriv : Fin 6 → Fin 6 → ℝ
  81  volumeDeriv : Fin 6 → ℝ
  82  schlaefli :
  83    ∀ e' : Fin 6,
  84      (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralDeriv e e')
  85        = 0
  86
  87/-- The exact local statement we need to prove from the cofactor derivative
  88formulas. -/
  89def SchlaefliTetrahedronTheorem : Prop :=
  90  ∀ T : NonDegenerateTet, Nonempty (TetraSchlaefliDerivativeData T)
  91
  92/-- The explicit Schläfli equation for chosen derivative functions. -/
  93def TetraSchlaefliEquation (T : NonDegenerateTet)
  94    (dTheta_dL : Fin 6 → Fin 6 → ℝ) (_dVolume_dL : Fin 6 → ℝ) : Prop :=
  95  ∀ e' : Fin 6,
  96    (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dTheta_dL e e')
  97      = 0
  98
  99/-- If the explicit Schläfli equation has been proved for concrete
 100derivative functions, it constructs the local derivative-data package. -/
 101def tetraSchlaefliDerivativeData_of_equation
 102    (T : NonDegenerateTet)
 103    (dTheta_dL : Fin 6 → Fin 6 → ℝ) (dVolume_dL : Fin 6 → ℝ)
 104    (hS : TetraSchlaefliEquation T dTheta_dL dVolume_dL) :
 105    TetraSchlaefliDerivativeData T where
 106  dihedralDeriv := dTheta_dL
 107  volumeDeriv := dVolume_dL
 108  schlaefli := hS
 109
 110/-- The local data gives the Schläfli sum for its own derivative matrices. -/
 111theorem schlaefli_sum_of_tetraData
 112    {T : NonDegenerateTet} (D : TetraSchlaefliDerivativeData T) (e' : Fin 6) :
 113    (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * D.dihedralDeriv e e')
 114      = 0 :=
 115  D.schlaefli e'
 116
 117end
 118
 119end SchlaefliTetrahedron
 120end Geometry
 121end IndisputableMonolith
 122