IndisputableMonolith.Geometry.DihedralCayleyMenger

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.SpecialFunctions.Sqrt
   3import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
   4import IndisputableMonolith.Geometry.CayleyMengerMatrix
   5import IndisputableMonolith.Geometry.ReggeRigorousFoundation
   6import IndisputableMonolith.Geometry.DihedralAngle
   7
   8/-!
   9# Dihedral Cosines from Cayley-Menger Cofactors
  10
  11This module replaces the prose reference in `DihedralAngle.lean` with an
  12actual Lean definition of the tetrahedral dihedral cosine from
  13Cayley-Menger cofactors.
  14
  15For an edge `e = (i,j)`, let `(p,q)` be the two vertices opposite that
  16edge.  In the Cayley-Menger matrix the vertex rows/columns are shifted by
  17one, so vertex `v : Fin 4` corresponds to CM index `v.val + 1 : Fin 5`.
  18The classical cofactor formula is:
  19
  20```
  21cos θ_e = C_{p,q} / sqrt (C_{p,p} * C_{q,q})
  22```
  23
  24where `C` is the cofactor matrix of the `5 × 5` Cayley-Menger matrix.
  25This sign convention gives `cos θ = 1/3` for the regular tetrahedron,
  26matching the standard internal dihedral angle.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Geometry
  31namespace DihedralCayleyMenger
  32
  33open CayleyMengerPolynomial CayleyMengerMatrix ReggeRigorousFoundation
  34open DihedralAngle
  35
  36noncomputable section
  37
  38/-- Convert a tetrahedron vertex index `0..3` to the corresponding
  39Cayley-Menger matrix index `1..4`. -/
  40def cmVertexIndex : Fin 4 → Fin 5
  41  | 0 => 1
  42  | 1 => 2
  43  | 2 => 3
  44  | 3 => 4
  45
  46/-- For each tetrahedral edge, return the two Cayley-Menger vertex indices
  47opposite that edge. -/
  48def oppositeCMVertices : Fin 6 → Fin 5 × Fin 5
  49  | 0 => (3, 4) -- edge (0,1), opposite vertices 2,3
  50  | 1 => (2, 4) -- edge (0,2), opposite vertices 1,3
  51  | 2 => (2, 3) -- edge (0,3), opposite vertices 1,2
  52  | 3 => (1, 4) -- edge (1,2), opposite vertices 0,3
  53  | 4 => (1, 3) -- edge (1,3), opposite vertices 0,2
  54  | 5 => (1, 2) -- edge (2,3), opposite vertices 0,1
  55
  56/-- The Cayley-Menger cofactor denominator for the dihedral cosine at an
  57edge. -/
  58def dihedralDenom3 (a : SqEdges) (e : Fin 6) : ℝ :=
  59  let p := (oppositeCMVertices e).1
  60  let q := (oppositeCMVertices e).2
  61  Real.sqrt (cmCofactor3 a p p * cmCofactor3 a q q)
  62
  63/-- The tetrahedral dihedral cosine from Cayley-Menger cofactors. -/
  64def dihedralCos3Sq (a : SqEdges) (e : Fin 6) : ℝ :=
  65  let p := (oppositeCMVertices e).1
  66  let q := (oppositeCMVertices e).2
  67  cmCofactor3 a p q / dihedralDenom3 a e
  68
  69/-- The same cosine on a `NonDegenerateTet`. -/
  70def dihedralCos3 (T : NonDegenerateTet) (e : Fin 6) : ℝ :=
  71  dihedralCos3Sq T.sqEdge e
  72
  73/-- The dihedral angle obtained from the cofactor cosine formula. -/
  74def dihedralAngle3 (T : NonDegenerateTet) (e : Fin 6) : ℝ :=
  75  Real.arccos (dihedralCos3 T e)
  76
  77/-- Package the cofactor-defined angle in the existing `DihedralAngleData`
  78API, assuming the usual range bound for the cofactor cosine. -/
  79def dihedralAngleData3 (T : NonDegenerateTet) (e : Fin 6)
  80    (hlo : -1 ≤ dihedralCos3 T e) (hhi : dihedralCos3 T e ≤ 1) :
  81    DihedralAngleData where
  82  cosine := dihedralCos3 T e
  83  cosine_lb := hlo
  84  cosine_ub := hhi
  85
  86/-- The regular-tetrahedron cofactor check required to reduce the cofactor
  87formula to `cos θ = 1 / 3`.  This is isolated so the expensive determinant
  88minor expansion is not repeated by downstream modules. -/
  89def RegularUnitCofactorCheck : Prop :=
  90  ∀ e : Fin 6,
  91    let p := (oppositeCMVertices e).1
  92    let q := (oppositeCMVertices e).2
  93    cmCofactor3 regularUnitSqEdges p q = 1 ∧
  94      cmCofactor3 regularUnitSqEdges p p = -3 ∧
  95      cmCofactor3 regularUnitSqEdges q q = -3
  96
  97/-- The regular-unit cofactor check is now a theorem, not an assumption. -/
  98theorem regularUnitCofactorCheck : RegularUnitCofactorCheck := by
  99  intro e
 100  fin_cases e <;>
 101    simp [oppositeCMVertices,
 102      regularUnit_cofactor_34, regularUnit_cofactor_24, regularUnit_cofactor_23,
 103      regularUnit_cofactor_14, regularUnit_cofactor_13, regularUnit_cofactor_12,
 104      regularUnit_vertex_diag_cofactor]
 105
 106/-- If the regular-tetrahedron cofactor check holds, the cofactor formula
 107gives the standard value `cos θ = 1 / 3`. -/
 108theorem dihedralCos3_regularUnit_of_cofactorCheck
 109    (hC : RegularUnitCofactorCheck) (e : Fin 6) :
 110    dihedralCos3 regularUnitTet e = (1 / 3 : ℝ) := by
 111  unfold dihedralCos3 dihedralCos3Sq dihedralDenom3
 112  simp [regularUnitTet]
 113  rcases hC e with ⟨hnum, hpp, hqq⟩
 114  rw [hnum, hpp, hqq]
 115  have hsqrt9 : Real.sqrt 9 = (3 : ℝ) := by
 116    rw [show (9 : ℝ) = 3 ^ 2 by norm_num]
 117    exact Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 3)
 118  norm_num
 119  rw [hsqrt9]
 120  norm_num
 121
 122/-- Hence, under the regular cofactor check, the cofactor angle agrees with
 123the existing regular-tetrahedron dihedral API. -/
 124theorem dihedralAngle3_regularUnit_of_cofactorCheck
 125    (hC : RegularUnitCofactorCheck) (e : Fin 6) :
 126    dihedralAngle3 regularUnitTet e = regular_tet_dihedral.theta := by
 127  unfold dihedralAngle3 DihedralAngleData.theta regular_tet_dihedral
 128  rw [dihedralCos3_regularUnit_of_cofactorCheck hC e]
 129
 130/-- The cofactor formula gives the standard regular tetrahedron value
 131`cos θ = 1 / 3` without external assumptions. -/
 132theorem dihedralCos3_regularUnit (e : Fin 6) :
 133    dihedralCos3 regularUnitTet e = (1 / 3 : ℝ) :=
 134  dihedralCos3_regularUnit_of_cofactorCheck regularUnitCofactorCheck e
 135
 136/-- The cofactor angle agrees with the existing regular-tetrahedron
 137dihedral API without external assumptions. -/
 138theorem dihedralAngle3_regularUnit (e : Fin 6) :
 139    dihedralAngle3 regularUnitTet e = regular_tet_dihedral.theta :=
 140  dihedralAngle3_regularUnit_of_cofactorCheck regularUnitCofactorCheck e
 141
 142end
 143
 144end DihedralCayleyMenger
 145end Geometry
 146end IndisputableMonolith
 147