IndisputableMonolith.Geometry.CayleyMengerPolynomial

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.Calculus.ContDiff.Basic
   3import Mathlib.Analysis.Calculus.ContDiff.Operations
   4import Mathlib.Analysis.Calculus.Deriv.Basic
   5import Mathlib.Analysis.Calculus.Deriv.Mul
   6import Mathlib.Topology.Algebra.Module.Basic
   7
   8/-!
   9# Explicit Cayley-Menger Polynomial for a Tetrahedron (n = 3)
  10
  11This module begins the rigorous program to close Philip's deeper concern:
  12the genuine Regge second-variation coefficient matrix `M_ij` computed from
  13Cayley-Menger / dihedral-angle derivatives must be compared component by
  14component to `area(f_ij)`.
  15
  16## Strategy
  17
  18The classical Cayley-Menger determinant for a tetrahedron is a fixed
  19polynomial of degree 3 in the six squared edge lengths.  We define it
  20directly as that polynomial and verify it matches the classical 5x5
  21determinant on the regular and standard right-angle tetrahedron test
  22points.  Smoothness in the squared edge lengths then follows by direct
  23construction from `ContDiff` combinators.
  24
  25## Edge convention
  26
  27We index the six edges of a tetrahedron with vertices `0, 1, 2, 3` by
  28`Fin 6`:
  29
  30  edge 0 = (0,1),  squared length `α := a 0`
  31  edge 1 = (0,2),  squared length `β := a 1`
  32  edge 2 = (0,3),  squared length `γ := a 2`
  33  edge 3 = (1,2),  squared length `λ := a 3`
  34  edge 4 = (1,3),  squared length `μ := a 4`
  35  edge 5 = (2,3),  squared length `ν := a 5`
  36
  37Opposite-edge pairs are `(0,5)`, `(1,4)`, `(2,3)`.
  38
  39## Verified polynomial form
  40
  41```
  42CM_3(a) = 2 · [ α·ν·(β+γ+λ+μ−α−ν)
  43              + β·μ·(α+γ+λ+ν−β−μ)
  44              + γ·λ·(α+β+μ+ν−γ−λ)
  45              − α·β·λ − α·γ·μ − β·γ·ν − λ·μ·ν ]
  46```
  47
  48The classical Cayley relation is `288 · V² = CM_3(a)` for genuine
  49Euclidean tetrahedra, verified below on two test points.
  50
  51This polynomial is the workhorse for all later derivative and
  52component-comparison theorems.
  53-/
  54
  55namespace IndisputableMonolith
  56namespace Geometry
  57namespace CayleyMengerPolynomial
  58
  59noncomputable section
  60
  61/-- Squared edge lengths of a tetrahedron, indexed by `Fin 6`. -/
  62abbrev SqEdges : Type := Fin 6 → ℝ
  63
  64/-- The explicit Cayley-Menger polynomial in the six squared edge lengths. -/
  65def cm3 (a : SqEdges) : ℝ :=
  66  2 * ( a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)
  67      + a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)
  68      + a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)
  69      - a 0 * a 1 * a 3
  70      - a 0 * a 2 * a 4
  71      - a 1 * a 2 * a 5
  72      - a 3 * a 4 * a 5 )
  73
  74/-! ## §1. Test points: numerical verification of `288 V² = cm3` -/
  75
  76/-- Edge data for the unit regular tetrahedron (all squared lengths = 1). -/
  77def regularUnitSqEdges : SqEdges := fun _ => 1
  78
  79/-- The Cayley-Menger value of the unit regular tetrahedron is 4.
  80Classical: `V_unit_regular = √2 / 12`, so `288 V² = 288 / 72 = 4`. -/
  81theorem cm3_regular_unit : cm3 regularUnitSqEdges = 4 := by
  82  unfold cm3 regularUnitSqEdges
  83  norm_num
  84
  85/-- Edge data for the right-angle unit tetrahedron with three orthogonal
  86unit edges from a single vertex. -/
  87def rightAngleUnitSqEdges : SqEdges :=
  88  fun e =>
  89    match e with
  90    | ⟨0, _⟩ => 1
  91    | ⟨1, _⟩ => 1
  92    | ⟨2, _⟩ => 1
  93    | ⟨3, _⟩ => 2
  94    | ⟨4, _⟩ => 2
  95    | ⟨5, _⟩ => 2
  96    | ⟨n+6, h⟩ => absurd h (by omega)
  97
  98/-- The Cayley-Menger value of the right-angle unit tetrahedron is 8.
  99Classical: `V = 1/6`, so `288 V² = 288/36 = 8`. -/
 100theorem cm3_rightAngle_unit : cm3 rightAngleUnitSqEdges = 8 := by
 101  unfold cm3 rightAngleUnitSqEdges
 102  norm_num
 103
 104/-! ## §2. Smoothness of the Cayley-Menger polynomial
 105
 106We prove `ContDiff ℝ n cm3` for any natural smoothness order `n`.  This
 107covers all derivative needs (Hessian, Schläfli, etc.).
 108-/
 109
 110/-- Each coordinate projection `a ↦ a i` from `(Fin 6 → ℝ)` to `ℝ` is
 111smooth at any natural order `n`. -/
 112private theorem contDiff_eval (n : ℕ∞) (i : Fin 6) :
 113    ContDiff ℝ n (fun a : SqEdges => a i) :=
 114  (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin 6 => ℝ) i).contDiff
 115
 116/-- The Cayley-Menger polynomial is `Cⁿ` for any natural order `n`.
 117Built explicitly from `ContDiff.add`, `ContDiff.sub`, `ContDiff.mul`. -/
 118theorem cm3_contDiff (n : ℕ∞) : ContDiff ℝ n cm3 := by
 119  have h0 := contDiff_eval n 0
 120  have h1 := contDiff_eval n 1
 121  have h2 := contDiff_eval n 2
 122  have h3 := contDiff_eval n 3
 123  have h4 := contDiff_eval n 4
 124  have h5 := contDiff_eval n 5
 125  have hconst : ContDiff ℝ n (fun _ : SqEdges => (2 : ℝ)) := contDiff_const
 126  -- Build linear combinations.
 127  have s1 : ContDiff ℝ n (fun a : SqEdges => a 1 + a 2 + a 3 + a 4 - a 0 - a 5) :=
 128    ContDiff.sub (ContDiff.sub
 129      (ContDiff.add (ContDiff.add (ContDiff.add h1 h2) h3) h4) h0) h5
 130  have s2 : ContDiff ℝ n (fun a : SqEdges => a 0 + a 2 + a 3 + a 5 - a 1 - a 4) :=
 131    ContDiff.sub (ContDiff.sub
 132      (ContDiff.add (ContDiff.add (ContDiff.add h0 h2) h3) h5) h1) h4
 133  have s3 : ContDiff ℝ n (fun a : SqEdges => a 0 + a 1 + a 4 + a 5 - a 2 - a 3) :=
 134    ContDiff.sub (ContDiff.sub
 135      (ContDiff.add (ContDiff.add (ContDiff.add h0 h1) h4) h5) h2) h3
 136  -- Three "balanced" cubic terms.
 137  have c1 : ContDiff ℝ n (fun a : SqEdges =>
 138      a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)) :=
 139    ContDiff.mul (ContDiff.mul h0 h5) s1
 140  have c2 : ContDiff ℝ n (fun a : SqEdges =>
 141      a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)) :=
 142    ContDiff.mul (ContDiff.mul h1 h4) s2
 143  have c3 : ContDiff ℝ n (fun a : SqEdges =>
 144      a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)) :=
 145    ContDiff.mul (ContDiff.mul h2 h3) s3
 146  -- Four monomial cubic terms.
 147  have nA : ContDiff ℝ n (fun a : SqEdges => a 0 * a 1 * a 3) :=
 148    ContDiff.mul (ContDiff.mul h0 h1) h3
 149  have nB : ContDiff ℝ n (fun a : SqEdges => a 0 * a 2 * a 4) :=
 150    ContDiff.mul (ContDiff.mul h0 h2) h4
 151  have nC : ContDiff ℝ n (fun a : SqEdges => a 1 * a 2 * a 5) :=
 152    ContDiff.mul (ContDiff.mul h1 h2) h5
 153  have nD : ContDiff ℝ n (fun a : SqEdges => a 3 * a 4 * a 5) :=
 154    ContDiff.mul (ContDiff.mul h3 h4) h5
 155  have inner : ContDiff ℝ n (fun a : SqEdges =>
 156        a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)
 157      + a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)
 158      + a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)
 159      - a 0 * a 1 * a 3
 160      - a 0 * a 2 * a 4
 161      - a 1 * a 2 * a 5
 162      - a 3 * a 4 * a 5 ) :=
 163    ContDiff.sub (ContDiff.sub (ContDiff.sub (ContDiff.sub
 164      (ContDiff.add (ContDiff.add c1 c2) c3) nA) nB) nC) nD
 165  show ContDiff ℝ n cm3
 166  unfold cm3
 167  exact ContDiff.mul hconst inner
 168
 169/-- An immediate corollary: `cm3` is continuous. -/
 170theorem cm3_continuous : Continuous cm3 :=
 171  (cm3_contDiff 0).continuous
 172
 173/-! ## §3. Polynomial behavior under uniform scaling
 174
 175If all squared edge lengths are scaled by `s`, the CM polynomial scales by
 176`s³`.  Classical: `V → s^{3/2} V`, hence `V² → s³ V²`, hence
 177`CM = 288 V² → s³ · CM`.  This is a useful structural sanity check. -/
 178
 179theorem cm3_scaling (a : SqEdges) (s : ℝ) :
 180    cm3 (fun e => s * a e) = s ^ 3 * cm3 a := by
 181  unfold cm3
 182  ring
 183
 184/-- A trivial but useful corollary: the regular CM value at common
 185squared-length `s` equals `s³ · 4`. -/
 186theorem cm3_constSq (s : ℝ) : cm3 (fun _ => s) = 4 * s ^ 3 := by
 187  have h := cm3_scaling regularUnitSqEdges s
 188  have h1 : cm3 regularUnitSqEdges = 4 := cm3_regular_unit
 189  have h2 : (fun e : Fin 6 => s * regularUnitSqEdges e) = (fun _ : Fin 6 => s) := by
 190    funext e
 191    unfold regularUnitSqEdges
 192    ring
 193  have h3 : cm3 (fun _ : Fin 6 => s) = s ^ 3 * cm3 regularUnitSqEdges := by
 194    rw [← h2]; exact h
 195  rw [h3, h1]
 196  ring
 197
 198end
 199
 200end CayleyMengerPolynomial
 201end Geometry
 202end IndisputableMonolith
 203