IndisputableMonolith.Geometry.TetrahedronRealization

   1import Mathlib.Geometry.Euclidean.Basic
   2import Mathlib.Analysis.InnerProductSpace.PiL2
   3import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
   4import IndisputableMonolith.Geometry.CayleyMengerPolynomial
   5import IndisputableMonolith.Geometry.ReggeRigorousFoundation
   6
   7/-!
   8# Euclidean Realizations of Tetrahedra
   9
  10This module connects the abstract six squared-edge coordinates used by
  11the Cayley-Menger layer to actual points in Euclidean 3-space.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Geometry
  16namespace TetrahedronRealization
  17
  18open CayleyMengerPolynomial
  19open ReggeRigorousFoundation
  20
  21noncomputable section
  22
  23/-- A tetrahedron realized by four points in Euclidean 3-space.  The
  24`nondegenerate` field is kept as the affine-independence hypothesis that
  25will later feed the strict dihedral range and positive-volume proofs. -/
  26structure RealizedTet where
  27  p : Fin 4 → EuclideanSpace ℝ (Fin 3)
  28  nondegenerate : AffineIndependent ℝ p
  29
  30/-- Convert the local tetrahedral edge index to its endpoint vertices. -/
  31def edgeVertices3 : Fin 6 → Fin 4 × Fin 4 :=
  32  ReggeRigorousFoundation.edgeVertices
  33
  34/-- Edge vector from `i` to `j`. -/
  35def edgeVector (T : RealizedTet) (i j : Fin 4) : EuclideanSpace ℝ (Fin 3) :=
  36  T.p j - T.p i
  37
  38/-- Squared length of an edge between two vertices. -/
  39def vertexSqDist (T : RealizedTet) (i j : Fin 4) : ℝ :=
  40  ‖edgeVector T i j‖ ^ 2
  41
  42/-- Extract the six squared edge lengths in the same order as `SqEdges`. -/
  43def sqEdgeOfPoints (T : RealizedTet) : SqEdges :=
  44  fun e =>
  45    let v := edgeVertices3 e
  46    vertexSqDist T v.1 v.2
  47
  48/-- Squared edge lengths from points are nonnegative. -/
  49theorem sqEdgeOfPoints_nonneg (T : RealizedTet) (e : Fin 6) :
  50    0 ≤ sqEdgeOfPoints T e := by
  51  unfold sqEdgeOfPoints vertexSqDist
  52  exact sq_nonneg _
  53
  54/-- The three edge vectors from vertex `0` that span the tetrahedron. -/
  55def basisEdgeVector (T : RealizedTet) : Fin 3 → EuclideanSpace ℝ (Fin 3)
  56  | 0 => edgeVector T 0 1
  57  | 1 => edgeVector T 0 2
  58  | 2 => edgeVector T 0 3
  59
  60/-- Gram matrix of the three edge vectors based at vertex `0`. -/
  61def gram3 (T : RealizedTet) : Matrix (Fin 3) (Fin 3) ℝ :=
  62  fun i j => inner ℝ (basisEdgeVector T i) (basisEdgeVector T j)
  63
  64/-- The Gram matrix is symmetric. -/
  65theorem gram3_symm (T : RealizedTet) (i j : Fin 3) :
  66    gram3 T i j = gram3 T j i := by
  67  unfold gram3
  68  rw [real_inner_comm]
  69
  70/-- Euclidean oriented volume squared from the Gram determinant:
  71`V² = det(Gram) / 36`. -/
  72def volumeSqFromGram (T : RealizedTet) : ℝ :=
  73  Matrix.det (gram3 T) / 36
  74
  75/-- The defining Gram-volume identity. -/
  76theorem det_gram3_eq_36_volumeSq (T : RealizedTet) :
  77    Matrix.det (gram3 T) = 36 * volumeSqFromGram T := by
  78  unfold volumeSqFromGram
  79  ring
  80
  81/-- Cayley-Menger volume squared from the extracted edge data:
  82`V² = cm3 / 288`. -/
  83def volumeSqFromCM (T : RealizedTet) : ℝ :=
  84  cm3 (sqEdgeOfPoints T) / 288
  85
  86/-- The theorem target connecting the Euclidean Gram volume to the
  87Cayley-Menger volume for realized tetrahedra. -/
  88def GramCayleyMengerVolumeTheorem : Prop :=
  89  ∀ T : RealizedTet, volumeSqFromCM T = volumeSqFromGram T
  90
  91end
  92
  93end TetrahedronRealization
  94end Geometry
  95end IndisputableMonolith
  96