IndisputableMonolith.Geometry.CayleyMengerMatrix

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Data.Fin.SuccPred
   3import Mathlib.Data.Matrix.Basic
   4import Mathlib.Algebra.BigOperators.Fin
   5import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
   6import Mathlib.LinearAlgebra.Matrix.Notation
   7import Mathlib.Topology.Instances.Matrix
   8import IndisputableMonolith.Geometry.CayleyMengerPolynomial
   9
  10/-!
  11# Cayley-Menger Matrix, Minors, and Cofactors for a Tetrahedron
  12
  13This module connects the explicit tetrahedral Cayley-Menger polynomial
  14`cm3` to the actual `5 × 5` Cayley-Menger determinant.  It is the
  15determinant/cofactor layer needed by the dihedral cosine formula.
  16
  17The row/column convention is:
  18
  19```
  20    0  1  2  3  4
  210 [ 0, 1, 1, 1, 1 ]
  221 [ 1, 0, a0,a1,a2]
  232 [ 1, a0,0, a3,a4]
  243 [ 1, a1,a3,0, a5]
  254 [ 1, a2,a4,a5,0 ]
  26```
  27
  28where `a0..a5` are the squared edge lengths
  29`(01),(02),(03),(12),(13),(23)`.
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Geometry
  34namespace CayleyMengerMatrix
  35
  36open CayleyMengerPolynomial
  37
  38noncomputable section
  39
  40/-- The `5 × 5` Cayley-Menger matrix of a tetrahedron, as a function of
  41the six squared edge lengths. -/
  42def cmMatrix3 (a : SqEdges) (i j : Fin 5) : ℝ :=
  43  match i.val, j.val with
  44  | 0, 0 => 0
  45  | 0, _ => 1
  46  | _, 0 => 1
  47  | 1, 1 => 0
  48  | 1, 2 => a 0
  49  | 2, 1 => a 0
  50  | 1, 3 => a 1
  51  | 3, 1 => a 1
  52  | 1, 4 => a 2
  53  | 4, 1 => a 2
  54  | 2, 2 => 0
  55  | 2, 3 => a 3
  56  | 3, 2 => a 3
  57  | 2, 4 => a 4
  58  | 4, 2 => a 4
  59  | 3, 3 => 0
  60  | 3, 4 => a 5
  61  | 4, 3 => a 5
  62  | 4, 4 => 0
  63  | _, _ => 0
  64
  65/-- The Cayley-Menger determinant, computed by Mathlib's matrix determinant. -/
  66def cmDet3 (a : SqEdges) : ℝ :=
  67  Matrix.det (cmMatrix3 a)
  68
  69/-- Delete row `r` and column `c` from the Cayley-Menger matrix and take
  70the determinant. -/
  71def cmMinor3 (a : SqEdges) (r c : Fin 5) : ℝ :=
  72  Matrix.det (Matrix.submatrix (cmMatrix3 a) (Fin.succAbove r) (Fin.succAbove c))
  73
  74/-- Cofactor sign `(-1)^(r+c)` as a real number. -/
  75def cmCofactorSign3 (r c : Fin 5) : ℝ :=
  76  if Even (r.val + c.val) then 1 else -1
  77
  78/-- Cayley-Menger cofactor `C_{r,c}`. -/
  79def cmCofactor3 (a : SqEdges) (r c : Fin 5) : ℝ :=
  80  cmCofactorSign3 r c * cmMinor3 a r c
  81
  82/-- The Cayley-Menger matrix is symmetric. -/
  83theorem cmMatrix3_symm (a : SqEdges) (i j : Fin 5) :
  84    cmMatrix3 a i j = cmMatrix3 a j i := by
  85  fin_cases i <;> fin_cases j <;> rfl
  86
  87set_option maxHeartbeats 2000000
  88/-- Mathlib's determinant of the Cayley-Menger matrix equals the explicit
  89polynomial `cm3`. -/
  90theorem cmDet3_eq_cm3 (a : SqEdges) : cmDet3 a = cm3 a := by
  91  unfold cmDet3 cmMatrix3 cm3
  92  simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
  93  ring_nf
  94
  95/-- Regular unit tetrahedron determinant check. -/
  96theorem cmDet3_regular_unit : cmDet3 regularUnitSqEdges = 4 := by
  97  rw [cmDet3_eq_cm3, cm3_regular_unit]
  98
  99/-- Right-angle unit tetrahedron determinant check. -/
 100theorem cmDet3_rightAngle_unit : cmDet3 rightAngleUnitSqEdges = 8 := by
 101  rw [cmDet3_eq_cm3, cm3_rightAngle_unit]
 102
 103/-- The determinant inherits the smoothness of the explicit polynomial. -/
 104theorem cmDet3_contDiff (n : ℕ∞) : ContDiff ℝ n cmDet3 := by
 105  have h : cmDet3 = cm3 := by
 106    funext a
 107    exact cmDet3_eq_cm3 a
 108  rw [h]
 109  exact cm3_contDiff n
 110
 111/-- Every entry of the Cayley-Menger matrix is a smooth function of the
 112six squared edge lengths. -/
 113theorem cmMatrix3_entry_contDiff (n : ℕ∞) (i j : Fin 5) :
 114    ContDiff ℝ n (fun a : SqEdges => cmMatrix3 a i j) := by
 115  fin_cases i <;> fin_cases j <;>
 116    simp [cmMatrix3] <;> fun_prop
 117
 118set_option maxHeartbeats 2000000
 119/-- Every Cayley-Menger minor is a smooth function of the six squared edge
 120lengths. -/
 121theorem cmMinor3_contDiff (n : ℕ∞) (r c : Fin 5) :
 122    ContDiff ℝ n (fun a : SqEdges => cmMinor3 a r c) := by
 123  unfold cmMinor3 cmMatrix3
 124  fin_cases r <;> fin_cases c <;>
 125    simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove] <;>
 126    fun_prop
 127
 128/-- Every Cayley-Menger cofactor is smooth. -/
 129theorem cmCofactor3_contDiff (n : ℕ∞) (r c : Fin 5) :
 130    ContDiff ℝ n (fun a : SqEdges => cmCofactor3 a r c) := by
 131  unfold cmCofactor3
 132  exact ContDiff.mul contDiff_const (cmMinor3_contDiff n r c)
 133
 134/-! ## Regular-unit cofactor normalization
 135
 136Directly normalizing `Matrix.submatrix` in downstream files produces huge
 137`Fin.succAbove` goals.  The following explicit determinant lemmas are the
 138normal forms needed by the regular-tetrahedron cofactor check. -/
 139
 140/-- The diagonal vertex minor of the regular unit Cayley-Menger matrix. -/
 141def regularUnitDiagMinorMatrix : Matrix (Fin 4) (Fin 4) ℝ :=
 142  !![(0 : ℝ), 1, 1, 1;
 143     1, 0, 1, 1;
 144     1, 1, 0, 1;
 145     1, 1, 1, 0]
 146
 147/-- The off-diagonal vertex minor of the regular unit Cayley-Menger matrix. -/
 148def regularUnitOffDiagMinorMatrix : Matrix (Fin 4) (Fin 4) ℝ :=
 149  !![(0 : ℝ), 1, 1, 1;
 150     1, 0, 1, 1;
 151     1, 1, 0, 1;
 152     1, 1, 1, 1]
 153
 154def regularUnitOffDiagMinorMatrix24 : Matrix (Fin 4) (Fin 4) ℝ :=
 155  !![(0 : ℝ), 1, 1, 1;
 156     1, 0, 1, 1;
 157     1, 1, 1, 0;
 158     1, 1, 1, 1]
 159
 160def regularUnitOffDiagMinorMatrix23 : Matrix (Fin 4) (Fin 4) ℝ :=
 161  !![(0 : ℝ), 1, 1, 1;
 162     1, 0, 1, 1;
 163     1, 1, 1, 1;
 164     1, 1, 1, 0]
 165
 166def regularUnitOffDiagMinorMatrix14 : Matrix (Fin 4) (Fin 4) ℝ :=
 167  !![(0 : ℝ), 1, 1, 1;
 168     1, 1, 0, 1;
 169     1, 1, 1, 0;
 170     1, 1, 1, 1]
 171
 172def regularUnitOffDiagMinorMatrix13 : Matrix (Fin 4) (Fin 4) ℝ :=
 173  !![(0 : ℝ), 1, 1, 1;
 174     1, 1, 0, 1;
 175     1, 1, 1, 1;
 176     1, 1, 1, 0]
 177
 178def regularUnitOffDiagMinorMatrix12 : Matrix (Fin 4) (Fin 4) ℝ :=
 179  !![(0 : ℝ), 1, 1, 1;
 180     1, 1, 1, 1;
 181     1, 1, 0, 1;
 182     1, 1, 1, 0]
 183
 184theorem det_regularUnitDiagMinorMatrix :
 185    Matrix.det regularUnitDiagMinorMatrix = -3 := by
 186  unfold regularUnitDiagMinorMatrix
 187  rw [Matrix.det_succ_row_zero]
 188  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 189  norm_num
 190
 191theorem det_regularUnitOffDiagMinorMatrix :
 192    Matrix.det regularUnitOffDiagMinorMatrix = -1 := by
 193  unfold regularUnitOffDiagMinorMatrix
 194  rw [Matrix.det_succ_row_zero]
 195  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 196  norm_num
 197
 198theorem det_regularUnitOffDiagMinorMatrix24 :
 199    Matrix.det regularUnitOffDiagMinorMatrix24 = 1 := by
 200  unfold regularUnitOffDiagMinorMatrix24
 201  rw [Matrix.det_succ_row_zero]
 202  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 203
 204theorem det_regularUnitOffDiagMinorMatrix23 :
 205    Matrix.det regularUnitOffDiagMinorMatrix23 = -1 := by
 206  unfold regularUnitOffDiagMinorMatrix23
 207  rw [Matrix.det_succ_row_zero]
 208  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 209
 210theorem det_regularUnitOffDiagMinorMatrix14 :
 211    Matrix.det regularUnitOffDiagMinorMatrix14 = -1 := by
 212  unfold regularUnitOffDiagMinorMatrix14
 213  rw [Matrix.det_succ_row_zero]
 214  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 215
 216theorem det_regularUnitOffDiagMinorMatrix13 :
 217    Matrix.det regularUnitOffDiagMinorMatrix13 = 1 := by
 218  unfold regularUnitOffDiagMinorMatrix13
 219  rw [Matrix.det_succ_row_zero]
 220  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 221
 222theorem det_regularUnitOffDiagMinorMatrix12 :
 223    Matrix.det regularUnitOffDiagMinorMatrix12 = -1 := by
 224  unfold regularUnitOffDiagMinorMatrix12
 225  rw [Matrix.det_succ_row_zero]
 226  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 227
 228/-- The `(3,4)` regular unit minor reduces to the explicit off-diagonal
 229normal-form matrix. -/
 230theorem regularUnit_minor_34_eq_offDiag :
 231    Matrix.submatrix (cmMatrix3 regularUnitSqEdges) (Fin.succAbove (3 : Fin 5))
 232      (Fin.succAbove (4 : Fin 5)) = regularUnitOffDiagMinorMatrix := by
 233  ext i j
 234  fin_cases i <;> fin_cases j <;>
 235    simp [regularUnitOffDiagMinorMatrix, cmMatrix3, regularUnitSqEdges, Fin.succAbove]
 236
 237/-- First off-diagonal regular unit cofactor. -/
 238theorem regularUnit_cofactor_34 :
 239    cmCofactor3 regularUnitSqEdges 3 4 = 1 := by
 240  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 241  simp [show ¬ Even (7 : Nat) by decide]
 242  rw [regularUnit_minor_34_eq_offDiag, det_regularUnitOffDiagMinorMatrix]
 243  norm_num
 244
 245theorem regularUnit_minor_24_eq_offDiag :
 246    Matrix.submatrix (cmMatrix3 regularUnitSqEdges) (Fin.succAbove (2 : Fin 5))
 247      (Fin.succAbove (4 : Fin 5)) = regularUnitOffDiagMinorMatrix24 := by
 248  ext i j
 249  fin_cases i <;> fin_cases j <;>
 250    simp [regularUnitOffDiagMinorMatrix24, cmMatrix3, regularUnitSqEdges, Fin.succAbove]
 251
 252theorem regularUnit_cofactor_24 :
 253    cmCofactor3 regularUnitSqEdges 2 4 = 1 := by
 254  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 255  simp [show Even (6 : Nat) by decide]
 256  rw [regularUnit_minor_24_eq_offDiag, det_regularUnitOffDiagMinorMatrix24]
 257
 258theorem regularUnit_minor_23_eq_offDiag :
 259    Matrix.submatrix (cmMatrix3 regularUnitSqEdges) (Fin.succAbove (2 : Fin 5))
 260      (Fin.succAbove (3 : Fin 5)) = regularUnitOffDiagMinorMatrix23 := by
 261  ext i j
 262  fin_cases i <;> fin_cases j <;>
 263    simp [regularUnitOffDiagMinorMatrix23, cmMatrix3, regularUnitSqEdges, Fin.succAbove]
 264
 265theorem regularUnit_cofactor_23 :
 266    cmCofactor3 regularUnitSqEdges 2 3 = 1 := by
 267  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 268  simp [show ¬ Even (5 : Nat) by decide]
 269  rw [regularUnit_minor_23_eq_offDiag, det_regularUnitOffDiagMinorMatrix23]
 270  norm_num
 271
 272theorem regularUnit_minor_14_eq_offDiag :
 273    Matrix.submatrix (cmMatrix3 regularUnitSqEdges) (Fin.succAbove (1 : Fin 5))
 274      (Fin.succAbove (4 : Fin 5)) = regularUnitOffDiagMinorMatrix14 := by
 275  ext i j
 276  fin_cases i <;> fin_cases j <;>
 277    simp [regularUnitOffDiagMinorMatrix14, cmMatrix3, regularUnitSqEdges, Fin.succAbove]
 278
 279theorem regularUnit_cofactor_14 :
 280    cmCofactor3 regularUnitSqEdges 1 4 = 1 := by
 281  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 282  simp [show ¬ Even (5 : Nat) by decide]
 283  rw [regularUnit_minor_14_eq_offDiag, det_regularUnitOffDiagMinorMatrix14]
 284  norm_num
 285
 286theorem regularUnit_minor_13_eq_offDiag :
 287    Matrix.submatrix (cmMatrix3 regularUnitSqEdges) (Fin.succAbove (1 : Fin 5))
 288      (Fin.succAbove (3 : Fin 5)) = regularUnitOffDiagMinorMatrix13 := by
 289  ext i j
 290  fin_cases i <;> fin_cases j <;>
 291    simp [regularUnitOffDiagMinorMatrix13, cmMatrix3, regularUnitSqEdges, Fin.succAbove]
 292
 293theorem regularUnit_cofactor_13 :
 294    cmCofactor3 regularUnitSqEdges 1 3 = 1 := by
 295  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 296  simp [show Even (4 : Nat) by decide]
 297  rw [regularUnit_minor_13_eq_offDiag, det_regularUnitOffDiagMinorMatrix13]
 298
 299theorem regularUnit_minor_12_eq_offDiag :
 300    Matrix.submatrix (cmMatrix3 regularUnitSqEdges) (Fin.succAbove (1 : Fin 5))
 301      (Fin.succAbove (2 : Fin 5)) = regularUnitOffDiagMinorMatrix12 := by
 302  ext i j
 303  fin_cases i <;> fin_cases j <;>
 304    simp [regularUnitOffDiagMinorMatrix12, cmMatrix3, regularUnitSqEdges, Fin.succAbove]
 305
 306theorem regularUnit_cofactor_12 :
 307    cmCofactor3 regularUnitSqEdges 1 2 = 1 := by
 308  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 309  simp [show ¬ Even (3 : Nat) by decide]
 310  rw [regularUnit_minor_12_eq_offDiag, det_regularUnitOffDiagMinorMatrix12]
 311  norm_num
 312
 313/-- Any nonzero diagonal vertex minor of the regular unit Cayley-Menger
 314matrix reduces to the diagonal normal form. -/
 315theorem regularUnit_diag_minor_eq_normalForm (p : Fin 5) (hp : p ≠ 0) :
 316    Matrix.submatrix (cmMatrix3 regularUnitSqEdges) (Fin.succAbove p) (Fin.succAbove p)
 317      = regularUnitDiagMinorMatrix := by
 318  fin_cases p
 319  · contradiction
 320  all_goals
 321    ext i j
 322    fin_cases i <;> fin_cases j <;>
 323      simp [regularUnitDiagMinorMatrix, cmMatrix3, regularUnitSqEdges, Fin.succAbove]
 324
 325/-- Diagonal vertex cofactors of the regular unit tetrahedron. -/
 326theorem regularUnit_vertex_diag_cofactor (p : Fin 5) (hp : p ≠ 0) :
 327    cmCofactor3 regularUnitSqEdges p p = -3 := by
 328  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 329  have heven : Even (p.val + p.val) := by
 330    use p.val
 331  simp [heven]
 332  rw [regularUnit_diag_minor_eq_normalForm p hp, det_regularUnitDiagMinorMatrix]
 333
 334/-- The determinant inherits the cubic scaling law from `cm3`. -/
 335theorem cmDet3_scaling (a : SqEdges) (s : ℝ) :
 336    cmDet3 (fun e => s * a e) = s ^ 3 * cmDet3 a := by
 337  rw [cmDet3_eq_cm3, cm3_scaling, cmDet3_eq_cm3]
 338
 339end
 340
 341end CayleyMengerMatrix
 342end Geometry
 343end IndisputableMonolith
 344