IndisputableMonolith.Geometry.GramCayleyMenger

   1import IndisputableMonolith.Geometry.TetrahedronRealization
   2import IndisputableMonolith.Geometry.CayleyMengerMatrix
   3
   4/-!
   5# Gram and Cayley-Menger Bridge
   6
   7This module isolates the theorem connecting the Euclidean Gram determinant
   8of a realized tetrahedron to its Cayley-Menger determinant.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Geometry
  13namespace GramCayleyMenger
  14
  15open TetrahedronRealization
  16open CayleyMengerPolynomial
  17open CayleyMengerMatrix
  18
  19noncomputable section
  20
  21/-- Squared-edge data generated by a symmetric `3×3` Gram matrix for the
  22edge vectors `(u, v, w)` from vertex `0`. -/
  23def sqEdgesFromGram (G : Matrix (Fin 3) (Fin 3) ℝ) : SqEdges :=
  24  fun e =>
  25    match e with
  26    | 0 => G 0 0
  27    | 1 => G 1 1
  28    | 2 => G 2 2
  29    | 3 => G 0 0 + G 1 1 - 2 * G 0 1
  30    | 4 => G 0 0 + G 2 2 - 2 * G 0 2
  31    | 5 => G 1 1 + G 2 2 - 2 * G 1 2
  32
  33/-- Pure algebra: the tetrahedral Cayley-Menger polynomial generated by a
  34symmetric Gram matrix equals `8 * det G`. -/
  35theorem cm3_sqEdgesFromGram_eq_8_det (G : Matrix (Fin 3) (Fin 3) ℝ)
  36    (hsymm : ∀ i j, G i j = G j i) :
  37    cm3 (sqEdgesFromGram G) = 8 * Matrix.det G := by
  38  unfold sqEdgesFromGram cm3
  39  rw [Matrix.det_fin_three]
  40  have h10 : G 1 0 = G 0 1 := hsymm 1 0
  41  have h20 : G 2 0 = G 0 2 := hsymm 2 0
  42  have h21 : G 2 1 = G 1 2 := hsymm 2 1
  43  rw [h10, h20, h21]
  44  ring
  45
  46/-- The Gram determinant version of Cayley-Menger volume equivalence. -/
  47def GramCayleyMengerTheorem : Prop :=
  48  ∀ T : RealizedTet,
  49    cm3 (sqEdgeOfPoints T) / 288 = Matrix.det (gram3 T) / 36
  50
  51/-- Squared-distance identity induced by a basepoint Gram matrix. -/
  52private theorem sqDist_eq_baseGram
  53    (x y z : EuclideanSpace ℝ (Fin 3)) :
  54    ‖z - y‖ ^ 2 =
  55      ‖y - x‖ ^ 2 + ‖z - x‖ ^ 2 - 2 * inner ℝ (y - x) (z - x) := by
  56  rw [norm_sub_sq_real z y, norm_sub_sq_real y x, norm_sub_sq_real z x]
  57  simp [inner_sub_left, inner_sub_right, real_inner_comm]
  58  ring_nf
  59
  60/-- The squared edges extracted from points agree with the squared edges
  61generated from the Gram matrix of the three basepoint edge vectors. -/
  62theorem sqEdgeOfPoints_eq_sqEdgesFromGram (T : RealizedTet) :
  63    sqEdgeOfPoints T = sqEdgesFromGram (gram3 T) := by
  64  funext e
  65  fin_cases e
  66  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
  67      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  68  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
  69      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  70  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
  71      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  72  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
  73      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  74    exact sqDist_eq_baseGram (T.p 0) (T.p 1) (T.p 2)
  75  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
  76      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  77    exact sqDist_eq_baseGram (T.p 0) (T.p 1) (T.p 3)
  78  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
  79      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  80    exact sqDist_eq_baseGram (T.p 0) (T.p 2) (T.p 3)
  81
  82/-- For a realized tetrahedron, `cm3` of the extracted squared-edge data
  83equals `8 * det(Gram)`. -/
  84theorem cm3_sqEdgeOfPoints_eq_8_det_gram (T : RealizedTet) :
  85    cm3 (sqEdgeOfPoints T) = 8 * Matrix.det (gram3 T) := by
  86  rw [sqEdgeOfPoints_eq_sqEdgesFromGram]
  87  exact cm3_sqEdgesFromGram_eq_8_det (gram3 T) (gram3_symm T)
  88
  89/-- The realized tetrahedron satisfies the Gram/Cayley-Menger volume theorem. -/
  90theorem gram_cayley_menger_realized (T : RealizedTet) :
  91    volumeSqFromCM T = volumeSqFromGram T := by
  92  unfold volumeSqFromCM volumeSqFromGram
  93  rw [cm3_sqEdgeOfPoints_eq_8_det_gram]
  94  ring
  95
  96theorem gramCayleyMengerTheorem : GramCayleyMengerTheorem :=
  97  gram_cayley_menger_realized
  98
  99/-- The same target expressed through the named volume-squared definitions. -/
 100theorem gram_cayley_menger_target_equiv :
 101    GramCayleyMengerTheorem ↔
 102      ∀ T : RealizedTet, volumeSqFromCM T = volumeSqFromGram T := by
 103  unfold GramCayleyMengerTheorem volumeSqFromCM volumeSqFromGram
 104  rfl
 105
 106/-- The determinant-level target using `cmDet3`. -/
 107def GramCayleyMengerDetTheorem : Prop :=
 108  ∀ T : RealizedTet,
 109    cmDet3 (sqEdgeOfPoints T) / 288 = Matrix.det (gram3 T) / 36
 110
 111/-- The determinant-level and polynomial-level targets are equivalent
 112because `cmDet3 = cm3`. -/
 113theorem gram_cayley_menger_det_target_equiv :
 114    GramCayleyMengerDetTheorem ↔ GramCayleyMengerTheorem := by
 115  constructor
 116  · intro h T
 117    have hT := h T
 118    rw [cmDet3_eq_cm3] at hT
 119    exact hT
 120  · intro h T
 121    have hT := h T
 122    rw [cmDet3_eq_cm3]
 123    exact hT
 124
 125end
 126
 127end GramCayleyMenger
 128end Geometry
 129end IndisputableMonolith
 130