IndisputableMonolith.Geometry.DihedralCofactorFormula
IndisputableMonolith/Geometry/DihedralCofactorFormula.lean · 874 lines · 80 declarations
show as:
view math explainer →
1import Mathlib.LinearAlgebra.CrossProduct
2import Mathlib.LinearAlgebra.Matrix.DotProduct
3import IndisputableMonolith.Geometry.GramCayleyMenger
4import IndisputableMonolith.Geometry.DihedralCayleyMenger
5
6/-!
7# Berger Cofactor Formula Target
8
9This module defines the Euclidean geometric side of the tetrahedral
10dihedral cosine: face normals from cross products and the normalized
11inner product of the two adjacent face normals.
12
13The remaining theorem in this module is the Berger cofactor formula,
14which will identify this geometric cosine with the Cayley-Menger cofactor
15ratio in `DihedralCayleyMenger`.
16-/
17
18namespace IndisputableMonolith
19namespace Geometry
20namespace DihedralCofactorFormula
21
22open TetrahedronRealization
23open DihedralCayleyMenger
24open CayleyMengerPolynomial
25open CayleyMengerMatrix
26
27open scoped Matrix
28
29noncomputable section
30
31/-- The two faces adjacent to an edge, represented by the opposite vertices
32of those faces. For edge `(i,j)`, these are the two remaining vertices. -/
33def adjacentFaceOppositeVertices : Fin 6 → Fin 4 × Fin 4
34 | 0 => (2, 3)
35 | 1 => (1, 3)
36 | 2 => (1, 2)
37 | 3 => (0, 3)
38 | 4 => (0, 2)
39 | 5 => (0, 1)
40
41/-- Coordinate vector for the edge from `a` to `b`. -/
42def coordEdgeVector (T : RealizedTet) (a b : Fin 4) : Fin 3 → ℝ :=
43 (T.p b - T.p a).ofLp
44
45/-- Coordinate dot products agree with the real inner product of the
46corresponding Euclidean edge vectors. -/
47theorem coordEdgeVector_dot_eq_inner
48 (T : RealizedTet) (a b c d : Fin 4) :
49 coordEdgeVector T a b ⬝ᵥ coordEdgeVector T c d =
50 inner ℝ (edgeVector T a b) (edgeVector T c d) := by
51 unfold coordEdgeVector edgeVector
52 rw [EuclideanSpace.inner_eq_star_dotProduct]
53 simp [dotProduct_comm]
54
55/-- Rebase any coordinate edge vector at vertex `0`. -/
56theorem coordEdgeVector_eq_base_sub (T : RealizedTet) (a b : Fin 4) :
57 coordEdgeVector T a b = coordEdgeVector T 0 b - coordEdgeVector T 0 a := by
58 unfold coordEdgeVector
59 ext k
60 simp
61
62/-- Dot product of two coordinate edge vectors after rebasing at vertex `0`. -/
63theorem coordEdgeVector_dot_base_sub (T : RealizedTet) (a b c d : Fin 4) :
64 coordEdgeVector T a b ⬝ᵥ coordEdgeVector T c d =
65 (coordEdgeVector T 0 b - coordEdgeVector T 0 a) ⬝ᵥ
66 (coordEdgeVector T 0 d - coordEdgeVector T 0 c) := by
67 rw [coordEdgeVector_eq_base_sub T a b, coordEdgeVector_eq_base_sub T c d]
68
69/-- Face normal for the face through vertices `(a,b,c)`, as a coordinate
70vector in `ℝ^3`. -/
71def faceNormal (T : RealizedTet) (a b c : Fin 4) : Fin 3 → ℝ :=
72 coordEdgeVector T a b ⨯₃ coordEdgeVector T a c
73
74/-- Dot product of two face normals, reduced by the cross-dot-cross identity. -/
75theorem faceNormal_dot_faceNormal
76 (T : RealizedTet) (a b c d e f : Fin 4) :
77 faceNormal T a b c ⬝ᵥ faceNormal T d e f =
78 (coordEdgeVector T a b ⬝ᵥ coordEdgeVector T d e) *
79 (coordEdgeVector T a c ⬝ᵥ coordEdgeVector T d f)
80 - (coordEdgeVector T a b ⬝ᵥ coordEdgeVector T d f) *
81 (coordEdgeVector T a c ⬝ᵥ coordEdgeVector T d e) := by
82 unfold faceNormal
83 rw [cross_dot_cross]
84
85/-- Squared norm of a face normal, reduced to edge-vector dot products. -/
86theorem faceNormal_dot_self
87 (T : RealizedTet) (a b c : Fin 4) :
88 faceNormal T a b c ⬝ᵥ faceNormal T a b c =
89 (coordEdgeVector T a b ⬝ᵥ coordEdgeVector T a b) *
90 (coordEdgeVector T a c ⬝ᵥ coordEdgeVector T a c)
91 - (coordEdgeVector T a b ⬝ᵥ coordEdgeVector T a c) *
92 (coordEdgeVector T a c ⬝ᵥ coordEdgeVector T a b) := by
93 simpa using faceNormal_dot_faceNormal T a b c a b c
94
95/-- The numerator of the geometric dihedral cosine at an edge, before
96normalization. -/
97def geometricDihedralNumerator (T : RealizedTet) (e : Fin 6) : ℝ :=
98 let edge := edgeVertices3 e
99 let opp := adjacentFaceOppositeVertices e
100 faceNormal T edge.1 edge.2 opp.1 ⬝ᵥ faceNormal T edge.1 edge.2 opp.2
101
102/-- The denominator square of the geometric dihedral cosine at an edge. -/
103def geometricDihedralDenomSq (T : RealizedTet) (e : Fin 6) : ℝ :=
104 let edge := edgeVertices3 e
105 let opp := adjacentFaceOppositeVertices e
106 let n₁ := faceNormal T edge.1 edge.2 opp.1
107 let n₂ := faceNormal T edge.1 edge.2 opp.2
108 (n₁ ⬝ᵥ n₁) * (n₂ ⬝ᵥ n₂)
109
110/-- The internal geometric dihedral cosine at an edge, computed from the
111two face normals adjacent to the edge. The sign is chosen to match the
112internal Regge dihedral convention. -/
113def geometricDihedralCos (T : RealizedTet) (e : Fin 6) : ℝ :=
114 geometricDihedralNumerator T e / Real.sqrt (geometricDihedralDenomSq T e)
115
116/-- Expands the geometric cosine numerator using `cross_dot_cross`. -/
117theorem geometricDihedralNumerator_cross
118 (T : RealizedTet) (e : Fin 6) :
119 geometricDihedralNumerator T e =
120 let edge := edgeVertices3 e
121 let opp := adjacentFaceOppositeVertices e
122 (coordEdgeVector T edge.1 edge.2 ⬝ᵥ coordEdgeVector T edge.1 edge.2) *
123 (coordEdgeVector T edge.1 opp.1 ⬝ᵥ coordEdgeVector T edge.1 opp.2)
124 - (coordEdgeVector T edge.1 edge.2 ⬝ᵥ coordEdgeVector T edge.1 opp.2) *
125 (coordEdgeVector T edge.1 opp.1 ⬝ᵥ coordEdgeVector T edge.1 edge.2) := by
126 unfold geometricDihedralNumerator
127 dsimp
128 rw [faceNormal_dot_faceNormal]
129
130/-- Edge `0 = (0,1)`: the geometric numerator in Gram entries. -/
131theorem geometricDihedralNumerator_edge0_gram (T : RealizedTet) :
132 geometricDihedralNumerator T 0 =
133 gram3 T 0 0 * gram3 T 1 2 - gram3 T 0 2 * gram3 T 1 0 := by
134 rw [geometricDihedralNumerator_cross]
135 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices,
136 coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
137
138set_option maxHeartbeats 2000000
139/-- Edge `0`: the corresponding Cayley-Menger cofactor equals four times
140the geometric numerator. -/
141theorem cmCofactor3_edge0_eq_four_geometricNumerator (T : RealizedTet) :
142 cmCofactor3 (sqEdgeOfPoints T) 3 4 =
143 4 * geometricDihedralNumerator T 0 := by
144 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
145 rw [geometricDihedralNumerator_edge0_gram]
146 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
147 simp [show ¬ Even (7 : Nat) by decide, Matrix.det_succ_row_zero,
148 Fin.sum_univ_succ, Fin.succAbove]
149 rw [gram3_symm T 1 0]
150 ring
151
152/-- Edge `0`: the first adjacent face-normal square in Gram entries. -/
153theorem faceNormal_edge0_left_self_gram (T : RealizedTet) :
154 faceNormal T 0 1 2 ⬝ᵥ faceNormal T 0 1 2 =
155 gram3 T 0 0 * gram3 T 1 1 - gram3 T 0 1 * gram3 T 1 0 := by
156 rw [faceNormal_dot_self]
157 simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
158
159/-- Edge `0`: the second adjacent face-normal square in Gram entries. -/
160theorem faceNormal_edge0_right_self_gram (T : RealizedTet) :
161 faceNormal T 0 1 3 ⬝ᵥ faceNormal T 0 1 3 =
162 gram3 T 0 0 * gram3 T 2 2 - gram3 T 0 2 * gram3 T 2 0 := by
163 rw [faceNormal_dot_self]
164 simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
165
166set_option maxHeartbeats 2000000
167/-- Edge `0`: diagonal cofactor for the first adjacent face. -/
168theorem cmCofactor3_edge0_left_diag_eq_neg_four_normalSq (T : RealizedTet) :
169 cmCofactor3 (sqEdgeOfPoints T) 3 3 =
170 -4 * (faceNormal T 0 1 3 ⬝ᵥ faceNormal T 0 1 3) := by
171 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
172 rw [faceNormal_edge0_right_self_gram]
173 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
174 simp [show Even (6 : Nat) by decide, Matrix.det_succ_row_zero,
175 Fin.sum_univ_succ, Fin.succAbove]
176 rw [gram3_symm T 2 0]
177 ring_nf
178
179set_option maxHeartbeats 2000000
180/-- Edge `0`: diagonal cofactor for the second adjacent face. -/
181theorem cmCofactor3_edge0_right_diag_eq_neg_four_normalSq (T : RealizedTet) :
182 cmCofactor3 (sqEdgeOfPoints T) 4 4 =
183 -4 * (faceNormal T 0 1 2 ⬝ᵥ faceNormal T 0 1 2) := by
184 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
185 rw [faceNormal_edge0_left_self_gram]
186 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
187 simp [show Even (8 : Nat) by decide, Matrix.det_succ_row_zero,
188 Fin.sum_univ_succ, Fin.succAbove]
189 rw [gram3_symm T 1 0]
190 ring_nf
191
192/-- Edge `0`: product of the two diagonal cofactors equals `16` times the
193geometric denominator square. -/
194theorem cmCofactor3_edge0_diag_product_eq_sixteen_denomSq (T : RealizedTet) :
195 cmCofactor3 (sqEdgeOfPoints T) 3 3 *
196 cmCofactor3 (sqEdgeOfPoints T) 4 4 =
197 16 * geometricDihedralDenomSq T 0 := by
198 rw [cmCofactor3_edge0_left_diag_eq_neg_four_normalSq,
199 cmCofactor3_edge0_right_diag_eq_neg_four_normalSq]
200 unfold geometricDihedralDenomSq
201 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
202 ring
203
204/-- Dot product of a real vector with itself is nonnegative. -/
205theorem dotProduct_self_nonneg (v : Fin 3 → ℝ) : 0 ≤ v ⬝ᵥ v := by
206 unfold dotProduct
207 exact Finset.sum_nonneg (fun i _ => mul_self_nonneg (v i))
208
209/-- The geometric denominator square is nonnegative. -/
210theorem geometricDihedralDenomSq_nonneg (T : RealizedTet) (e : Fin 6) :
211 0 ≤ geometricDihedralDenomSq T e := by
212 unfold geometricDihedralDenomSq
213 dsimp
214 exact mul_nonneg (dotProduct_self_nonneg _) (dotProduct_self_nonneg _)
215
216/-- Normalized dot products of coordinate vectors lie in `[-1, 1]`. -/
217theorem abs_dot_div_sqrt_self_mul_self_le_one (u v : Fin 3 → ℝ) :
218 |(u ⬝ᵥ v) / Real.sqrt ((u ⬝ᵥ u) * (v ⬝ᵥ v))| ≤ 1 := by
219 let U : EuclideanSpace ℝ (Fin 3) := (EuclideanSpace.equiv (𝕜 := ℝ) (ι := Fin 3)).symm u
220 let V : EuclideanSpace ℝ (Fin 3) := (EuclideanSpace.equiv (𝕜 := ℝ) (ι := Fin 3)).symm v
221 have hinner : inner ℝ U V = u ⬝ᵥ v := by
222 subst U
223 subst V
224 rw [EuclideanSpace.inner_eq_star_dotProduct]
225 simp [dotProduct_comm]
226 have hUU : ‖U‖ ^ 2 = u ⬝ᵥ u := by
227 subst U
228 rw [← real_inner_self_eq_norm_sq]
229 rw [EuclideanSpace.inner_eq_star_dotProduct]
230 simp
231 have hVV : ‖V‖ ^ 2 = v ⬝ᵥ v := by
232 subst V
233 rw [← real_inner_self_eq_norm_sq]
234 rw [EuclideanSpace.inner_eq_star_dotProduct]
235 simp
236 have hsqrt : Real.sqrt ((u ⬝ᵥ u) * (v ⬝ᵥ v)) = ‖U‖ * ‖V‖ := by
237 rw [← hUU, ← hVV]
238 rw [show ‖U‖ ^ 2 * ‖V‖ ^ 2 = (‖U‖ * ‖V‖) ^ 2 by ring]
239 exact Real.sqrt_sq (mul_nonneg (norm_nonneg U) (norm_nonneg V))
240 rw [← hinner, hsqrt]
241 exact abs_real_inner_div_norm_mul_norm_le_one U V
242
243/-- Geometric dihedral cosines lie in `[-1, 1]`. -/
244theorem geometricDihedralCos_range (T : RealizedTet) (e : Fin 6) :
245 -1 ≤ geometricDihedralCos T e ∧ geometricDihedralCos T e ≤ 1 := by
246 unfold geometricDihedralCos geometricDihedralNumerator geometricDihedralDenomSq
247 dsimp
248 exact abs_le.mp (abs_dot_div_sqrt_self_mul_self_le_one _ _)
249
250/-- A geometric dihedral cosine is strictly interior once the two endpoint
251cases are excluded. The endpoint-exclusion proof from affine independence is
252the remaining geometric step. -/
253theorem geometricDihedralCos_interior_of_ne_endpoints
254 (T : RealizedTet) (e : Fin 6)
255 (hneg : geometricDihedralCos T e ≠ -1)
256 (hpos : geometricDihedralCos T e ≠ 1) :
257 -1 < geometricDihedralCos T e ∧ geometricDihedralCos T e < 1 := by
258 have hr := geometricDihedralCos_range T e
259 exact ⟨lt_of_le_of_ne hr.1 (Ne.symm hneg), lt_of_le_of_ne hr.2 hpos⟩
260
261/-- Edge `0`: the diagonal-cofactor square root scales to the geometric
262denominator. -/
263theorem cmCofactor3_edge0_sqrt_diag_product (T : RealizedTet) :
264 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 3 3 *
265 cmCofactor3 (sqEdgeOfPoints T) 4 4)
266 = 4 * Real.sqrt (geometricDihedralDenomSq T 0) := by
267 rw [cmCofactor3_edge0_diag_product_eq_sixteen_denomSq]
268 rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16)]
269 have hsqrt16 : Real.sqrt (16 : ℝ) = 4 := by
270 rw [show (16 : ℝ) = 4 ^ 2 by norm_num]
271 exact Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)
272 rw [hsqrt16]
273
274/-- Edge `0`: Berger's cofactor formula reduced to the remaining square-root
275scaling/positivity fact. -/
276theorem geometricDihedralCos_edge0_eq_cofactorRatio_of_sqrt
277 (T : RealizedTet)
278 (hsqrt :
279 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 3 3 *
280 cmCofactor3 (sqEdgeOfPoints T) 4 4)
281 = 4 * Real.sqrt (geometricDihedralDenomSq T 0)) :
282 geometricDihedralCos T 0 = dihedralCos3Sq (sqEdgeOfPoints T) 0 := by
283 unfold geometricDihedralCos dihedralCos3Sq dihedralDenom3
284 change geometricDihedralNumerator T 0 / Real.sqrt (geometricDihedralDenomSq T 0) =
285 cmCofactor3 (sqEdgeOfPoints T) 3 4 /
286 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 3 3 *
287 cmCofactor3 (sqEdgeOfPoints T) 4 4)
288 rw [cmCofactor3_edge0_eq_four_geometricNumerator, hsqrt]
289 field_simp
290
291/-- Edge `0`: Berger's cofactor formula is fully proved. -/
292theorem geometricDihedralCos_edge0_eq_cmCofactorRatio (T : RealizedTet) :
293 geometricDihedralCos T 0 = dihedralCos3Sq (sqEdgeOfPoints T) 0 :=
294 geometricDihedralCos_edge0_eq_cofactorRatio_of_sqrt T
295 (cmCofactor3_edge0_sqrt_diag_product T)
296
297/-! ## Edge 1: `(0,2)` -/
298
299theorem geometricDihedralNumerator_edge1_gram (T : RealizedTet) :
300 geometricDihedralNumerator T 1 =
301 gram3 T 1 1 * gram3 T 0 2 - gram3 T 1 2 * gram3 T 0 1 := by
302 rw [geometricDihedralNumerator_cross]
303 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices,
304 coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
305
306set_option maxHeartbeats 2000000
307theorem cmCofactor3_edge1_eq_four_geometricNumerator (T : RealizedTet) :
308 cmCofactor3 (sqEdgeOfPoints T) 2 4 =
309 4 * geometricDihedralNumerator T 1 := by
310 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
311 rw [geometricDihedralNumerator_edge1_gram]
312 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
313 simp [show Even (6 : Nat) by decide, Matrix.det_succ_row_zero,
314 Fin.sum_univ_succ, Fin.succAbove]
315 ring_nf
316
317theorem faceNormal_edge1_left_self_gram (T : RealizedTet) :
318 faceNormal T 0 2 1 ⬝ᵥ faceNormal T 0 2 1 =
319 gram3 T 1 1 * gram3 T 0 0 - gram3 T 1 0 * gram3 T 0 1 := by
320 rw [faceNormal_dot_self]
321 simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
322
323theorem faceNormal_edge1_right_self_gram (T : RealizedTet) :
324 faceNormal T 0 2 3 ⬝ᵥ faceNormal T 0 2 3 =
325 gram3 T 1 1 * gram3 T 2 2 - gram3 T 1 2 * gram3 T 2 1 := by
326 rw [faceNormal_dot_self]
327 simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
328
329set_option maxHeartbeats 2000000
330theorem cmCofactor3_edge1_left_diag_eq_neg_four_normalSq (T : RealizedTet) :
331 cmCofactor3 (sqEdgeOfPoints T) 2 2 =
332 -4 * (faceNormal T 0 2 3 ⬝ᵥ faceNormal T 0 2 3) := by
333 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
334 rw [faceNormal_edge1_right_self_gram]
335 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
336 simp [show Even (4 : Nat) by decide, Matrix.det_succ_row_zero,
337 Fin.sum_univ_succ, Fin.succAbove]
338 rw [gram3_symm T 2 1]
339 ring_nf
340
341set_option maxHeartbeats 2000000
342theorem cmCofactor3_edge1_right_diag_eq_neg_four_normalSq (T : RealizedTet) :
343 cmCofactor3 (sqEdgeOfPoints T) 4 4 =
344 -4 * (faceNormal T 0 2 1 ⬝ᵥ faceNormal T 0 2 1) := by
345 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
346 rw [faceNormal_edge1_left_self_gram]
347 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
348 simp [show Even (8 : Nat) by decide, Matrix.det_succ_row_zero,
349 Fin.sum_univ_succ, Fin.succAbove]
350 rw [gram3_symm T 1 0]
351 ring_nf
352
353theorem cmCofactor3_edge1_diag_product_eq_sixteen_denomSq (T : RealizedTet) :
354 cmCofactor3 (sqEdgeOfPoints T) 2 2 *
355 cmCofactor3 (sqEdgeOfPoints T) 4 4 =
356 16 * geometricDihedralDenomSq T 1 := by
357 rw [cmCofactor3_edge1_left_diag_eq_neg_four_normalSq,
358 cmCofactor3_edge1_right_diag_eq_neg_four_normalSq]
359 unfold geometricDihedralDenomSq
360 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
361 ring
362
363theorem cmCofactor3_edge1_sqrt_diag_product (T : RealizedTet) :
364 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 2 2 *
365 cmCofactor3 (sqEdgeOfPoints T) 4 4)
366 = 4 * Real.sqrt (geometricDihedralDenomSq T 1) := by
367 rw [cmCofactor3_edge1_diag_product_eq_sixteen_denomSq]
368 rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16)]
369 have hsqrt16 : Real.sqrt (16 : ℝ) = 4 := by
370 rw [show (16 : ℝ) = 4 ^ 2 by norm_num]
371 exact Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)
372 rw [hsqrt16]
373
374theorem geometricDihedralCos_edge1_eq_cmCofactorRatio (T : RealizedTet) :
375 geometricDihedralCos T 1 = dihedralCos3Sq (sqEdgeOfPoints T) 1 := by
376 unfold geometricDihedralCos dihedralCos3Sq dihedralDenom3
377 change geometricDihedralNumerator T 1 / Real.sqrt (geometricDihedralDenomSq T 1) =
378 cmCofactor3 (sqEdgeOfPoints T) 2 4 /
379 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 2 2 *
380 cmCofactor3 (sqEdgeOfPoints T) 4 4)
381 rw [cmCofactor3_edge1_eq_four_geometricNumerator, cmCofactor3_edge1_sqrt_diag_product]
382 field_simp
383
384/-! ## Edge 2: `(0,3)` -/
385
386theorem geometricDihedralNumerator_edge2_gram (T : RealizedTet) :
387 geometricDihedralNumerator T 2 =
388 gram3 T 2 2 * gram3 T 0 1 - gram3 T 2 1 * gram3 T 0 2 := by
389 rw [geometricDihedralNumerator_cross]
390 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices,
391 coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
392
393set_option maxHeartbeats 2000000
394theorem cmCofactor3_edge2_eq_four_geometricNumerator (T : RealizedTet) :
395 cmCofactor3 (sqEdgeOfPoints T) 2 3 =
396 4 * geometricDihedralNumerator T 2 := by
397 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
398 rw [geometricDihedralNumerator_edge2_gram]
399 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
400 simp [show ¬ Even (5 : Nat) by decide, Matrix.det_succ_row_zero,
401 Fin.sum_univ_succ, Fin.succAbove]
402 rw [gram3_symm T 2 1]
403 ring_nf
404
405theorem faceNormal_edge2_left_self_gram (T : RealizedTet) :
406 faceNormal T 0 3 1 ⬝ᵥ faceNormal T 0 3 1 =
407 gram3 T 2 2 * gram3 T 0 0 - gram3 T 2 0 * gram3 T 0 2 := by
408 rw [faceNormal_dot_self]
409 simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
410
411theorem faceNormal_edge2_right_self_gram (T : RealizedTet) :
412 faceNormal T 0 3 2 ⬝ᵥ faceNormal T 0 3 2 =
413 gram3 T 2 2 * gram3 T 1 1 - gram3 T 2 1 * gram3 T 1 2 := by
414 rw [faceNormal_dot_self]
415 simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]
416
417set_option maxHeartbeats 2000000
418theorem cmCofactor3_edge2_left_diag_eq_neg_four_normalSq (T : RealizedTet) :
419 cmCofactor3 (sqEdgeOfPoints T) 2 2 =
420 -4 * (faceNormal T 0 3 2 ⬝ᵥ faceNormal T 0 3 2) := by
421 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
422 rw [faceNormal_edge2_right_self_gram]
423 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
424 simp [show Even (4 : Nat) by decide, Matrix.det_succ_row_zero,
425 Fin.sum_univ_succ, Fin.succAbove]
426 rw [gram3_symm T 2 1]
427 ring_nf
428
429set_option maxHeartbeats 2000000
430theorem cmCofactor3_edge2_right_diag_eq_neg_four_normalSq (T : RealizedTet) :
431 cmCofactor3 (sqEdgeOfPoints T) 3 3 =
432 -4 * (faceNormal T 0 3 1 ⬝ᵥ faceNormal T 0 3 1) := by
433 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
434 rw [faceNormal_edge2_left_self_gram]
435 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
436 simp [show Even (6 : Nat) by decide, Matrix.det_succ_row_zero,
437 Fin.sum_univ_succ, Fin.succAbove]
438 rw [gram3_symm T 2 0]
439 ring_nf
440
441theorem cmCofactor3_edge2_diag_product_eq_sixteen_denomSq (T : RealizedTet) :
442 cmCofactor3 (sqEdgeOfPoints T) 2 2 *
443 cmCofactor3 (sqEdgeOfPoints T) 3 3 =
444 16 * geometricDihedralDenomSq T 2 := by
445 rw [cmCofactor3_edge2_left_diag_eq_neg_four_normalSq,
446 cmCofactor3_edge2_right_diag_eq_neg_four_normalSq]
447 unfold geometricDihedralDenomSq
448 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
449 ring
450
451theorem cmCofactor3_edge2_sqrt_diag_product (T : RealizedTet) :
452 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 2 2 *
453 cmCofactor3 (sqEdgeOfPoints T) 3 3)
454 = 4 * Real.sqrt (geometricDihedralDenomSq T 2) := by
455 rw [cmCofactor3_edge2_diag_product_eq_sixteen_denomSq]
456 rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16)]
457 have hsqrt16 : Real.sqrt (16 : ℝ) = 4 := by
458 rw [show (16 : ℝ) = 4 ^ 2 by norm_num]
459 exact Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)
460 rw [hsqrt16]
461
462theorem geometricDihedralCos_edge2_eq_cmCofactorRatio (T : RealizedTet) :
463 geometricDihedralCos T 2 = dihedralCos3Sq (sqEdgeOfPoints T) 2 := by
464 unfold geometricDihedralCos dihedralCos3Sq dihedralDenom3
465 change geometricDihedralNumerator T 2 / Real.sqrt (geometricDihedralDenomSq T 2) =
466 cmCofactor3 (sqEdgeOfPoints T) 2 3 /
467 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 2 2 *
468 cmCofactor3 (sqEdgeOfPoints T) 3 3)
469 rw [cmCofactor3_edge2_eq_four_geometricNumerator, cmCofactor3_edge2_sqrt_diag_product]
470 field_simp
471
472/-! ## Edge 3: `(1,2)` -/
473
474theorem geometricDihedralNumerator_edge3_gram (T : RealizedTet) :
475 geometricDihedralNumerator T 3 =
476 gram3 T 0 0 * gram3 T 1 1 - gram3 T 0 0 * gram3 T 1 2
477 - gram3 T 1 1 * gram3 T 0 2 - gram3 T 0 1 * gram3 T 0 1
478 + gram3 T 0 1 * gram3 T 0 2 + gram3 T 0 1 * gram3 T 1 2 := by
479 rw [geometricDihedralNumerator_cross]
480 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
481 rw [coordEdgeVector_eq_base_sub T 1 2, coordEdgeVector_eq_base_sub T 1 0,
482 coordEdgeVector_eq_base_sub T 1 3]
483 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
484 gram3, basisEdgeVector, edgeVector]
485 repeat rw [← real_inner_self_eq_norm_sq]
486 simp [inner_sub_left, inner_sub_right, real_inner_comm]
487 ring_nf
488
489set_option maxHeartbeats 2000000
490theorem cmCofactor3_edge3_eq_four_geometricNumerator (T : RealizedTet) :
491 cmCofactor3 (sqEdgeOfPoints T) 1 4 =
492 4 * geometricDihedralNumerator T 3 := by
493 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
494 rw [geometricDihedralNumerator_edge3_gram]
495 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
496 simp [show ¬ Even (5 : Nat) by decide, Matrix.det_succ_row_zero,
497 Fin.sum_univ_succ, Fin.succAbove]
498 ring_nf
499
500theorem faceNormal_edge3_left_self_gram (T : RealizedTet) :
501 faceNormal T 1 2 0 ⬝ᵥ faceNormal T 1 2 0 =
502 gram3 T 0 0 * gram3 T 1 1 - gram3 T 0 1 * gram3 T 1 0 := by
503 rw [faceNormal_dot_self]
504 rw [coordEdgeVector_eq_base_sub T 1 2, coordEdgeVector_eq_base_sub T 1 0]
505 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
506 gram3, basisEdgeVector, edgeVector]
507 repeat rw [← real_inner_self_eq_norm_sq]
508 simp [inner_sub_left, inner_sub_right, real_inner_comm]
509 ring_nf
510
511theorem faceNormal_edge3_right_self_gram (T : RealizedTet) :
512 faceNormal T 1 2 3 ⬝ᵥ faceNormal T 1 2 3 =
513 (gram3 T 0 0 * gram3 T 1 1 + gram3 T 0 0 * gram3 T 2 2
514 - 2 * gram3 T 0 0 * gram3 T 1 2 + gram3 T 1 1 * gram3 T 2 2
515 - 2 * gram3 T 1 1 * gram3 T 0 2 - 2 * gram3 T 2 2 * gram3 T 0 1
516 - gram3 T 0 1 * gram3 T 0 1 + 2 * gram3 T 0 1 * gram3 T 0 2
517 + 2 * gram3 T 0 1 * gram3 T 1 2 - gram3 T 0 2 * gram3 T 0 2
518 + 2 * gram3 T 0 2 * gram3 T 1 2 - gram3 T 1 2 * gram3 T 1 2) := by
519 rw [faceNormal_dot_self]
520 rw [coordEdgeVector_eq_base_sub T 1 2, coordEdgeVector_eq_base_sub T 1 3]
521 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
522 gram3, basisEdgeVector, edgeVector]
523 repeat rw [← real_inner_self_eq_norm_sq]
524 simp [inner_sub_left, inner_sub_right, real_inner_comm]
525 ring_nf
526
527set_option maxHeartbeats 2000000
528theorem cmCofactor3_edge3_left_diag_eq_neg_four_normalSq (T : RealizedTet) :
529 cmCofactor3 (sqEdgeOfPoints T) 1 1 =
530 -4 * (faceNormal T 1 2 3 ⬝ᵥ faceNormal T 1 2 3) := by
531 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
532 rw [faceNormal_edge3_right_self_gram]
533 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
534 simp [show Even (2 : Nat) by decide, Matrix.det_succ_row_zero,
535 Fin.sum_univ_succ, Fin.succAbove]
536 ring_nf
537
538set_option maxHeartbeats 2000000
539theorem cmCofactor3_edge3_right_diag_eq_neg_four_normalSq (T : RealizedTet) :
540 cmCofactor3 (sqEdgeOfPoints T) 4 4 =
541 -4 * (faceNormal T 1 2 0 ⬝ᵥ faceNormal T 1 2 0) := by
542 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
543 rw [faceNormal_edge3_left_self_gram]
544 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
545 simp [show Even (8 : Nat) by decide, Matrix.det_succ_row_zero,
546 Fin.sum_univ_succ, Fin.succAbove]
547 rw [gram3_symm T 1 0]
548 ring_nf
549
550theorem cmCofactor3_edge3_diag_product_eq_sixteen_denomSq (T : RealizedTet) :
551 cmCofactor3 (sqEdgeOfPoints T) 1 1 *
552 cmCofactor3 (sqEdgeOfPoints T) 4 4 =
553 16 * geometricDihedralDenomSq T 3 := by
554 rw [cmCofactor3_edge3_left_diag_eq_neg_four_normalSq,
555 cmCofactor3_edge3_right_diag_eq_neg_four_normalSq]
556 unfold geometricDihedralDenomSq
557 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
558 ring
559
560theorem cmCofactor3_edge3_sqrt_diag_product (T : RealizedTet) :
561 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 1 1 *
562 cmCofactor3 (sqEdgeOfPoints T) 4 4)
563 = 4 * Real.sqrt (geometricDihedralDenomSq T 3) := by
564 rw [cmCofactor3_edge3_diag_product_eq_sixteen_denomSq]
565 rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16)]
566 have hsqrt16 : Real.sqrt (16 : ℝ) = 4 := by
567 rw [show (16 : ℝ) = 4 ^ 2 by norm_num]
568 exact Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)
569 rw [hsqrt16]
570
571theorem geometricDihedralCos_edge3_eq_cmCofactorRatio (T : RealizedTet) :
572 geometricDihedralCos T 3 = dihedralCos3Sq (sqEdgeOfPoints T) 3 := by
573 unfold geometricDihedralCos dihedralCos3Sq dihedralDenom3
574 change geometricDihedralNumerator T 3 / Real.sqrt (geometricDihedralDenomSq T 3) =
575 cmCofactor3 (sqEdgeOfPoints T) 1 4 /
576 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 1 1 *
577 cmCofactor3 (sqEdgeOfPoints T) 4 4)
578 rw [cmCofactor3_edge3_eq_four_geometricNumerator, cmCofactor3_edge3_sqrt_diag_product]
579 field_simp
580
581/-! ## Edge 4: `(1,3)` -/
582
583theorem geometricDihedralNumerator_edge4_gram (T : RealizedTet) :
584 geometricDihedralNumerator T 4 =
585 gram3 T 0 0 * gram3 T 2 2 - gram3 T 0 0 * gram3 T 1 2
586 - gram3 T 2 2 * gram3 T 0 1 + gram3 T 0 1 * gram3 T 0 2
587 - gram3 T 0 2 * gram3 T 0 2 + gram3 T 0 2 * gram3 T 1 2 := by
588 rw [geometricDihedralNumerator_cross]
589 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
590 rw [coordEdgeVector_eq_base_sub T 1 3, coordEdgeVector_eq_base_sub T 1 0,
591 coordEdgeVector_eq_base_sub T 1 2]
592 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
593 gram3, basisEdgeVector, edgeVector]
594 repeat rw [← real_inner_self_eq_norm_sq]
595 simp [inner_sub_left, inner_sub_right, real_inner_comm]
596 ring_nf
597
598set_option maxHeartbeats 2000000
599theorem cmCofactor3_edge4_eq_four_geometricNumerator (T : RealizedTet) :
600 cmCofactor3 (sqEdgeOfPoints T) 1 3 =
601 4 * geometricDihedralNumerator T 4 := by
602 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
603 rw [geometricDihedralNumerator_edge4_gram]
604 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
605 simp [show Even (4 : Nat) by decide, Matrix.det_succ_row_zero,
606 Fin.sum_univ_succ, Fin.succAbove]
607 ring_nf
608
609theorem faceNormal_edge4_left_self_gram (T : RealizedTet) :
610 faceNormal T 1 3 0 ⬝ᵥ faceNormal T 1 3 0 =
611 gram3 T 0 0 * gram3 T 2 2 - gram3 T 0 2 * gram3 T 2 0 := by
612 rw [faceNormal_dot_self]
613 rw [coordEdgeVector_eq_base_sub T 1 3, coordEdgeVector_eq_base_sub T 1 0]
614 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
615 gram3, basisEdgeVector, edgeVector]
616 repeat rw [← real_inner_self_eq_norm_sq]
617 simp [inner_sub_left, inner_sub_right, real_inner_comm]
618 ring_nf
619
620theorem faceNormal_edge4_right_self_gram (T : RealizedTet) :
621 faceNormal T 1 3 2 ⬝ᵥ faceNormal T 1 3 2 =
622 (gram3 T 0 0 * gram3 T 1 1 + gram3 T 0 0 * gram3 T 2 2
623 - 2 * gram3 T 0 0 * gram3 T 1 2 + gram3 T 1 1 * gram3 T 2 2
624 - 2 * gram3 T 1 1 * gram3 T 0 2 - 2 * gram3 T 2 2 * gram3 T 0 1
625 - gram3 T 0 1 * gram3 T 0 1 + 2 * gram3 T 0 1 * gram3 T 0 2
626 + 2 * gram3 T 0 1 * gram3 T 1 2 - gram3 T 0 2 * gram3 T 0 2
627 + 2 * gram3 T 0 2 * gram3 T 1 2 - gram3 T 1 2 * gram3 T 1 2) := by
628 rw [faceNormal_dot_self]
629 rw [coordEdgeVector_eq_base_sub T 1 3, coordEdgeVector_eq_base_sub T 1 2]
630 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
631 gram3, basisEdgeVector, edgeVector]
632 repeat rw [← real_inner_self_eq_norm_sq]
633 simp [inner_sub_left, inner_sub_right, real_inner_comm]
634 ring_nf
635
636set_option maxHeartbeats 2000000
637theorem cmCofactor3_edge4_left_diag_eq_neg_four_normalSq (T : RealizedTet) :
638 cmCofactor3 (sqEdgeOfPoints T) 1 1 =
639 -4 * (faceNormal T 1 3 2 ⬝ᵥ faceNormal T 1 3 2) := by
640 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
641 rw [faceNormal_edge4_right_self_gram]
642 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
643 simp [show Even (2 : Nat) by decide, Matrix.det_succ_row_zero,
644 Fin.sum_univ_succ, Fin.succAbove]
645 ring_nf
646
647set_option maxHeartbeats 2000000
648theorem cmCofactor3_edge4_right_diag_eq_neg_four_normalSq (T : RealizedTet) :
649 cmCofactor3 (sqEdgeOfPoints T) 3 3 =
650 -4 * (faceNormal T 1 3 0 ⬝ᵥ faceNormal T 1 3 0) := by
651 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
652 rw [faceNormal_edge4_left_self_gram]
653 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
654 simp [show Even (6 : Nat) by decide, Matrix.det_succ_row_zero,
655 Fin.sum_univ_succ, Fin.succAbove]
656 rw [gram3_symm T 2 0]
657 ring_nf
658
659theorem cmCofactor3_edge4_diag_product_eq_sixteen_denomSq (T : RealizedTet) :
660 cmCofactor3 (sqEdgeOfPoints T) 1 1 *
661 cmCofactor3 (sqEdgeOfPoints T) 3 3 =
662 16 * geometricDihedralDenomSq T 4 := by
663 rw [cmCofactor3_edge4_left_diag_eq_neg_four_normalSq,
664 cmCofactor3_edge4_right_diag_eq_neg_four_normalSq]
665 unfold geometricDihedralDenomSq
666 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
667 ring
668
669theorem cmCofactor3_edge4_sqrt_diag_product (T : RealizedTet) :
670 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 1 1 *
671 cmCofactor3 (sqEdgeOfPoints T) 3 3)
672 = 4 * Real.sqrt (geometricDihedralDenomSq T 4) := by
673 rw [cmCofactor3_edge4_diag_product_eq_sixteen_denomSq]
674 rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16)]
675 have hsqrt16 : Real.sqrt (16 : ℝ) = 4 := by
676 rw [show (16 : ℝ) = 4 ^ 2 by norm_num]
677 exact Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)
678 rw [hsqrt16]
679
680theorem geometricDihedralCos_edge4_eq_cmCofactorRatio (T : RealizedTet) :
681 geometricDihedralCos T 4 = dihedralCos3Sq (sqEdgeOfPoints T) 4 := by
682 unfold geometricDihedralCos dihedralCos3Sq dihedralDenom3
683 change geometricDihedralNumerator T 4 / Real.sqrt (geometricDihedralDenomSq T 4) =
684 cmCofactor3 (sqEdgeOfPoints T) 1 3 /
685 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 1 1 *
686 cmCofactor3 (sqEdgeOfPoints T) 3 3)
687 rw [cmCofactor3_edge4_eq_four_geometricNumerator, cmCofactor3_edge4_sqrt_diag_product]
688 field_simp
689
690/-! ## Edge 5: `(2,3)` -/
691
692theorem geometricDihedralNumerator_edge5_gram (T : RealizedTet) :
693 geometricDihedralNumerator T 5 =
694 gram3 T 1 1 * gram3 T 2 2 - gram3 T 1 1 * gram3 T 0 2
695 - gram3 T 2 2 * gram3 T 0 1 + gram3 T 0 1 * gram3 T 1 2
696 + gram3 T 0 2 * gram3 T 1 2 - gram3 T 1 2 * gram3 T 1 2 := by
697 rw [geometricDihedralNumerator_cross]
698 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
699 rw [coordEdgeVector_eq_base_sub T 2 3, coordEdgeVector_eq_base_sub T 2 0,
700 coordEdgeVector_eq_base_sub T 2 1]
701 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
702 gram3, basisEdgeVector, edgeVector]
703 repeat rw [← real_inner_self_eq_norm_sq]
704 simp [inner_sub_left, inner_sub_right, real_inner_comm]
705 ring_nf
706
707set_option maxHeartbeats 2000000
708theorem cmCofactor3_edge5_eq_four_geometricNumerator (T : RealizedTet) :
709 cmCofactor3 (sqEdgeOfPoints T) 1 2 =
710 4 * geometricDihedralNumerator T 5 := by
711 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
712 rw [geometricDihedralNumerator_edge5_gram]
713 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
714 simp [show ¬ Even (3 : Nat) by decide, Matrix.det_succ_row_zero,
715 Fin.sum_univ_succ, Fin.succAbove]
716 ring_nf
717
718theorem faceNormal_edge5_left_self_gram (T : RealizedTet) :
719 faceNormal T 2 3 0 ⬝ᵥ faceNormal T 2 3 0 =
720 gram3 T 1 1 * gram3 T 2 2 - gram3 T 1 2 * gram3 T 2 1 := by
721 rw [faceNormal_dot_self]
722 rw [coordEdgeVector_eq_base_sub T 2 3, coordEdgeVector_eq_base_sub T 2 0]
723 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
724 gram3, basisEdgeVector, edgeVector]
725 repeat rw [← real_inner_self_eq_norm_sq]
726 simp [inner_sub_left, inner_sub_right, real_inner_comm]
727 ring_nf
728
729theorem faceNormal_edge5_right_self_gram (T : RealizedTet) :
730 faceNormal T 2 3 1 ⬝ᵥ faceNormal T 2 3 1 =
731 (gram3 T 0 0 * gram3 T 1 1 + gram3 T 0 0 * gram3 T 2 2
732 - 2 * gram3 T 0 0 * gram3 T 1 2 + gram3 T 1 1 * gram3 T 2 2
733 - 2 * gram3 T 1 1 * gram3 T 0 2 - 2 * gram3 T 2 2 * gram3 T 0 1
734 - gram3 T 0 1 * gram3 T 0 1 + 2 * gram3 T 0 1 * gram3 T 0 2
735 + 2 * gram3 T 0 1 * gram3 T 1 2 - gram3 T 0 2 * gram3 T 0 2
736 + 2 * gram3 T 0 2 * gram3 T 1 2 - gram3 T 1 2 * gram3 T 1 2) := by
737 rw [faceNormal_dot_self]
738 rw [coordEdgeVector_eq_base_sub T 2 3, coordEdgeVector_eq_base_sub T 2 1]
739 simp [sub_dotProduct, dotProduct_sub, coordEdgeVector_dot_eq_inner,
740 gram3, basisEdgeVector, edgeVector]
741 repeat rw [← real_inner_self_eq_norm_sq]
742 simp [inner_sub_left, inner_sub_right, real_inner_comm]
743 ring_nf
744
745set_option maxHeartbeats 2000000
746theorem cmCofactor3_edge5_left_diag_eq_neg_four_normalSq (T : RealizedTet) :
747 cmCofactor3 (sqEdgeOfPoints T) 1 1 =
748 -4 * (faceNormal T 2 3 1 ⬝ᵥ faceNormal T 2 3 1) := by
749 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
750 rw [faceNormal_edge5_right_self_gram]
751 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
752 simp [show Even (2 : Nat) by decide, Matrix.det_succ_row_zero,
753 Fin.sum_univ_succ, Fin.succAbove]
754 ring_nf
755
756set_option maxHeartbeats 2000000
757theorem cmCofactor3_edge5_right_diag_eq_neg_four_normalSq (T : RealizedTet) :
758 cmCofactor3 (sqEdgeOfPoints T) 2 2 =
759 -4 * (faceNormal T 2 3 0 ⬝ᵥ faceNormal T 2 3 0) := by
760 rw [GramCayleyMenger.sqEdgeOfPoints_eq_sqEdgesFromGram]
761 rw [faceNormal_edge5_left_self_gram]
762 unfold cmCofactor3 cmCofactorSign3 cmMinor3 cmMatrix3 GramCayleyMenger.sqEdgesFromGram
763 simp [show Even (4 : Nat) by decide, Matrix.det_succ_row_zero,
764 Fin.sum_univ_succ, Fin.succAbove]
765 rw [gram3_symm T 2 1]
766 ring_nf
767
768theorem cmCofactor3_edge5_diag_product_eq_sixteen_denomSq (T : RealizedTet) :
769 cmCofactor3 (sqEdgeOfPoints T) 1 1 *
770 cmCofactor3 (sqEdgeOfPoints T) 2 2 =
771 16 * geometricDihedralDenomSq T 5 := by
772 rw [cmCofactor3_edge5_left_diag_eq_neg_four_normalSq,
773 cmCofactor3_edge5_right_diag_eq_neg_four_normalSq]
774 unfold geometricDihedralDenomSq
775 simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
776 ring
777
778theorem cmCofactor3_edge5_sqrt_diag_product (T : RealizedTet) :
779 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 1 1 *
780 cmCofactor3 (sqEdgeOfPoints T) 2 2)
781 = 4 * Real.sqrt (geometricDihedralDenomSq T 5) := by
782 rw [cmCofactor3_edge5_diag_product_eq_sixteen_denomSq]
783 rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16)]
784 have hsqrt16 : Real.sqrt (16 : ℝ) = 4 := by
785 rw [show (16 : ℝ) = 4 ^ 2 by norm_num]
786 exact Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)
787 rw [hsqrt16]
788
789theorem geometricDihedralCos_edge5_eq_cmCofactorRatio (T : RealizedTet) :
790 geometricDihedralCos T 5 = dihedralCos3Sq (sqEdgeOfPoints T) 5 := by
791 unfold geometricDihedralCos dihedralCos3Sq dihedralDenom3
792 change geometricDihedralNumerator T 5 / Real.sqrt (geometricDihedralDenomSq T 5) =
793 cmCofactor3 (sqEdgeOfPoints T) 1 2 /
794 Real.sqrt (cmCofactor3 (sqEdgeOfPoints T) 1 1 *
795 cmCofactor3 (sqEdgeOfPoints T) 2 2)
796 rw [cmCofactor3_edge5_eq_four_geometricNumerator, cmCofactor3_edge5_sqrt_diag_product]
797 field_simp
798
799/-- Berger cofactor formula target for realized tetrahedra. -/
800def BergerCofactorFormula3 : Prop :=
801 ∀ T : RealizedTet, ∀ e : Fin 6,
802 geometricDihedralCos T e = dihedralCos3Sq (sqEdgeOfPoints T) e
803
804/-- Berger's cofactor formula for all six tetrahedral edges. -/
805theorem geometricDihedralCos_eq_cmCofactorRatio
806 (T : RealizedTet) (e : Fin 6) :
807 geometricDihedralCos T e = dihedralCos3Sq (sqEdgeOfPoints T) e := by
808 fin_cases e
809 · exact geometricDihedralCos_edge0_eq_cmCofactorRatio T
810 · exact geometricDihedralCos_edge1_eq_cmCofactorRatio T
811 · exact geometricDihedralCos_edge2_eq_cmCofactorRatio T
812 · exact geometricDihedralCos_edge3_eq_cmCofactorRatio T
813 · exact geometricDihedralCos_edge4_eq_cmCofactorRatio T
814 · exact geometricDihedralCos_edge5_eq_cmCofactorRatio T
815
816/-- The theorem target is discharged. -/
817theorem bergerCofactorFormula3 : BergerCofactorFormula3 :=
818 geometricDihedralCos_eq_cmCofactorRatio
819
820/-- Cofactor-defined dihedral cosines of realized tetrahedra lie in `[-1,1]`. -/
821theorem dihedralCos3Sq_sqEdgeOfPoints_range (T : RealizedTet) (e : Fin 6) :
822 -1 ≤ dihedralCos3Sq (sqEdgeOfPoints T) e ∧
823 dihedralCos3Sq (sqEdgeOfPoints T) e ≤ 1 := by
824 rw [← geometricDihedralCos_eq_cmCofactorRatio T e]
825 exact geometricDihedralCos_range T e
826
827/-- Cofactor dihedral cosines of realized tetrahedra are strictly interior
828once endpoint cases are excluded. -/
829theorem dihedralCos3Sq_sqEdgeOfPoints_interior_of_ne_endpoints
830 (T : RealizedTet) (e : Fin 6)
831 (hneg : dihedralCos3Sq (sqEdgeOfPoints T) e ≠ -1)
832 (hpos : dihedralCos3Sq (sqEdgeOfPoints T) e ≠ 1) :
833 -1 < dihedralCos3Sq (sqEdgeOfPoints T) e ∧
834 dihedralCos3Sq (sqEdgeOfPoints T) e < 1 := by
835 rw [← geometricDihedralCos_eq_cmCofactorRatio T e] at hneg hpos ⊢
836 exact geometricDihedralCos_interior_of_ne_endpoints T e hneg hpos
837
838/-- Any abstract nondegenerate tetrahedron that is realized by Euclidean
839points inherits the cofactor cosine range. -/
840theorem dihedralCos3_range_of_realization
841 (T : ReggeRigorousFoundation.NonDegenerateTet)
842 (R : RealizedTet) (hR : sqEdgeOfPoints R = T.sqEdge) (e : Fin 6) :
843 -1 ≤ dihedralCos3 T e ∧ dihedralCos3 T e ≤ 1 := by
844 unfold dihedralCos3
845 rw [← hR]
846 exact dihedralCos3Sq_sqEdgeOfPoints_range R e
847
848/-- Build `DihedralAngleData` for a realized abstract tetrahedron without
849caller-supplied range proofs. -/
850def dihedralAngleData3_of_realization
851 (T : ReggeRigorousFoundation.NonDegenerateTet)
852 (R : RealizedTet) (hR : sqEdgeOfPoints R = T.sqEdge) (e : Fin 6) :
853 DihedralAngle.DihedralAngleData :=
854 let hrange := dihedralCos3_range_of_realization T R hR e
855 dihedralAngleData3 T e hrange.1 hrange.2
856
857/-- Realized abstract tetrahedra inherit strict cofactor cosine interior
858from endpoint exclusion. -/
859theorem dihedralCos3_interior_of_realization_ne_endpoints
860 (T : ReggeRigorousFoundation.NonDegenerateTet)
861 (R : RealizedTet) (hR : sqEdgeOfPoints R = T.sqEdge) (e : Fin 6)
862 (hneg : dihedralCos3 T e ≠ -1)
863 (hpos : dihedralCos3 T e ≠ 1) :
864 -1 < dihedralCos3 T e ∧ dihedralCos3 T e < 1 := by
865 unfold dihedralCos3 at hneg hpos ⊢
866 rw [← hR] at hneg hpos ⊢
867 exact dihedralCos3Sq_sqEdgeOfPoints_interior_of_ne_endpoints R e hneg hpos
868
869end
870
871end DihedralCofactorFormula
872end Geometry
873end IndisputableMonolith
874