IndisputableMonolith.Geometry.AffineIndepInterior
IndisputableMonolith/Geometry/AffineIndepInterior.lean · 500 lines · 28 declarations
show as:
view math explainer →
1import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
2import IndisputableMonolith.Geometry.DihedralCofactorFormula
3
4/-!
5# Strict Dihedral Interior from Face-Normal Independence
6
7This module supplies the strict interior step needed by the Regge closure
8program. The analytic core is independent of tetrahedral bookkeeping:
9two linearly independent adjacent face normals have normalized dot product
10strictly between `-1` and `1`.
11
12The remaining geometric reduction is to prove the adjacent face-normal
13independence from the `AffineIndependent` field of `RealizedTet`; this file
14keeps that target explicit while removing the previous arccos endpoint
15inputs from downstream calculus once normal independence is available.
16-/
17
18namespace IndisputableMonolith
19namespace Geometry
20namespace AffineIndepInterior
21
22open DihedralCofactorFormula
23open TetrahedronRealization
24open DihedralCayleyMenger
25
26open scoped Matrix
27
28noncomputable section
29
30/-- View a coordinate vector as the Euclidean `ℓ²` vector used by Mathlib's
31inner-product API. -/
32def toEuclidean3 (u : Fin 3 → ℝ) : EuclideanSpace ℝ (Fin 3) :=
33 (EuclideanSpace.equiv (𝕜 := ℝ) (ι := Fin 3)).symm u
34
35theorem inner_toEuclidean3 (u v : Fin 3 → ℝ) :
36 inner ℝ (toEuclidean3 u) (toEuclidean3 v) = u ⬝ᵥ v := by
37 unfold toEuclidean3
38 rw [EuclideanSpace.inner_eq_star_dotProduct]
39 simp [dotProduct_comm]
40
41theorem norm_toEuclidean3_sq (u : Fin 3 → ℝ) :
42 ‖toEuclidean3 u‖ ^ 2 = u ⬝ᵥ u := by
43 unfold toEuclidean3
44 rw [← real_inner_self_eq_norm_sq]
45 rw [EuclideanSpace.inner_eq_star_dotProduct]
46 simp
47
48theorem sqrt_dot_self_mul_self_eq_norm_mul_norm (u v : Fin 3 → ℝ) :
49 Real.sqrt ((u ⬝ᵥ u) * (v ⬝ᵥ v)) =
50 ‖toEuclidean3 u‖ * ‖toEuclidean3 v‖ := by
51 rw [← norm_toEuclidean3_sq u, ← norm_toEuclidean3_sq v]
52 rw [show ‖toEuclidean3 u‖ ^ 2 * ‖toEuclidean3 v‖ ^ 2 =
53 (‖toEuclidean3 u‖ * ‖toEuclidean3 v‖) ^ 2 by ring]
54 exact Real.sqrt_sq
55 (mul_nonneg (norm_nonneg (toEuclidean3 u)) (norm_nonneg (toEuclidean3 v)))
56
57theorem toEuclidean3_smul (r : ℝ) (u : Fin 3 → ℝ) :
58 toEuclidean3 (r • u) = r • toEuclidean3 u := by
59 unfold toEuclidean3
60 simp
61
62theorem smul_of_toEuclidean3_smul {r : ℝ} {u v : Fin 3 → ℝ}
63 (h : toEuclidean3 v = r • toEuclidean3 u) : v = r • u := by
64 have h' := congrArg (EuclideanSpace.equiv (𝕜 := ℝ) (ι := Fin 3)) h
65 simpa [toEuclidean3] using h'
66
67/-- The normalized dot product of two coordinate vectors is not `1` when
68the vectors are linearly independent. -/
69theorem dot_div_sqrt_ne_one_of_linearIndependent
70 {u v : Fin 3 → ℝ} (hlin : LinearIndependent ℝ ![u, v]) :
71 (u ⬝ᵥ v) / Real.sqrt ((u ⬝ᵥ u) * (v ⬝ᵥ v)) ≠ 1 := by
72 intro h
73 have hE :
74 inner ℝ (toEuclidean3 u) (toEuclidean3 v) /
75 (‖toEuclidean3 u‖ * ‖toEuclidean3 v‖) = 1 := by
76 simpa [inner_toEuclidean3, sqrt_dot_self_mul_self_eq_norm_mul_norm] using h
77 rcases (real_inner_div_norm_mul_norm_eq_one_iff
78 (toEuclidean3 u) (toEuclidean3 v)).1 hE with ⟨huE, r, hr, hvE⟩
79 have hu : u ≠ 0 := by
80 intro hu0
81 apply huE
82 unfold toEuclidean3
83 simp [hu0]
84 have hv : v = r • u := smul_of_toEuclidean3_smul hvE
85 exact ((LinearIndependent.pair_iff' hu).1 hlin r) hv.symm
86
87/-- The normalized dot product of two coordinate vectors is not `-1` when
88the vectors are linearly independent. -/
89theorem dot_div_sqrt_ne_neg_one_of_linearIndependent
90 {u v : Fin 3 → ℝ} (hlin : LinearIndependent ℝ ![u, v]) :
91 (u ⬝ᵥ v) / Real.sqrt ((u ⬝ᵥ u) * (v ⬝ᵥ v)) ≠ -1 := by
92 intro h
93 have hE :
94 inner ℝ (toEuclidean3 u) (toEuclidean3 v) /
95 (‖toEuclidean3 u‖ * ‖toEuclidean3 v‖) = -1 := by
96 simpa [inner_toEuclidean3, sqrt_dot_self_mul_self_eq_norm_mul_norm] using h
97 rcases (real_inner_div_norm_mul_norm_eq_neg_one_iff
98 (toEuclidean3 u) (toEuclidean3 v)).1 hE with ⟨huE, r, hr, hvE⟩
99 have hu : u ≠ 0 := by
100 intro hu0
101 apply huE
102 unfold toEuclidean3
103 simp [hu0]
104 have hv : v = r • u := smul_of_toEuclidean3_smul hvE
105 exact ((LinearIndependent.pair_iff' hu).1 hlin r) hv.symm
106
107/-- The two adjacent face normals for a tetrahedral edge. -/
108def adjacentFaceNormals (T : RealizedTet) (e : Fin 6) :
109 (Fin 3 → ℝ) × (Fin 3 → ℝ) :=
110 let edge := edgeVertices3 e
111 let opp := adjacentFaceOppositeVertices e
112 (faceNormal T edge.1 edge.2 opp.1, faceNormal T edge.1 edge.2 opp.2)
113
114/-- Face-normal linear independence is the exact local geometric condition
115that excludes the `arccos` endpoint cases. -/
116def AdjacentFaceNormalsIndependent (T : RealizedTet) (e : Fin 6) : Prop :=
117 LinearIndependent ℝ ![(adjacentFaceNormals T e).1, (adjacentFaceNormals T e).2]
118
119/-- A face normal is nonzero whenever the two edge vectors spanning the face
120are linearly independent. -/
121theorem faceNormal_ne_zero_of_edgeVectors_linearIndependent
122 (T : RealizedTet) (a b c : Fin 4)
123 (hlin : LinearIndependent ℝ ![coordEdgeVector T a b, coordEdgeVector T a c]) :
124 faceNormal T a b c ≠ 0 := by
125 unfold faceNormal
126 exact (crossProduct_ne_zero_iff_linearIndependent).2 hlin
127
128/-- Adjacent face-normal independence is equivalent to the cross product of
129the two adjacent face normals being nonzero. -/
130theorem adjacentFaceNormalsIndependent_iff_cross_ne_zero
131 (T : RealizedTet) (e : Fin 6) :
132 AdjacentFaceNormalsIndependent T e ↔
133 (adjacentFaceNormals T e).1 ⨯₃ (adjacentFaceNormals T e).2 ≠ 0 := by
134 unfold AdjacentFaceNormalsIndependent
135 exact (crossProduct_ne_zero_iff_linearIndependent).symm
136
137/-- A nonzero cross product of adjacent face normals supplies the strict
138interior hypothesis used by the dihedral cosine proof. -/
139theorem adjacentFaceNormalsIndependent_of_cross_ne_zero
140 (T : RealizedTet) (e : Fin 6)
141 (h : (adjacentFaceNormals T e).1 ⨯₃ (adjacentFaceNormals T e).2 ≠ 0) :
142 AdjacentFaceNormalsIndependent T e :=
143 (adjacentFaceNormalsIndependent_iff_cross_ne_zero T e).2 h
144
145/-- If two face normals share the same edge vector `u`, their cross product
146is the scalar triple product times `u`. This is the algebraic core of the
147affine-independence-to-normal-independence step. -/
148theorem shared_edge_face_normals_cross
149 (u v w : Fin 3 → ℝ) :
150 (u ⨯₃ v) ⨯₃ (u ⨯₃ w) = (u ⬝ᵥ v ⨯₃ w) • u := by
151 rw [cross_cross_eq_smul_sub_smul']
152 have hdot : u ⬝ᵥ (u ⨯₃ v) = 0 := dot_self_cross u v
153 rw [hdot, zero_smul, sub_zero]
154 rw [show (u ⨯₃ v) ⬝ᵥ w = u ⬝ᵥ v ⨯₃ w by
155 rw [dotProduct_comm, triple_product_permutation]]
156
157/-- Adjacent tetrahedral face normals have the shared-edge cross-product
158normal form edge-by-edge. -/
159theorem adjacentFaceNormals_cross_eq_triple_smul_edge
160 (T : RealizedTet) (e : Fin 6) :
161 (adjacentFaceNormals T e).1 ⨯₃ (adjacentFaceNormals T e).2 =
162 let edge := edgeVertices3 e
163 let opp := adjacentFaceOppositeVertices e
164 (coordEdgeVector T edge.1 edge.2 ⬝ᵥ
165 coordEdgeVector T edge.1 opp.1 ⨯₃ coordEdgeVector T edge.1 opp.2) •
166 coordEdgeVector T edge.1 edge.2 := by
167 unfold adjacentFaceNormals faceNormal
168 dsimp
169 exact shared_edge_face_normals_cross _ _ _
170
171/-- Nonzero scalar triple product implies the two face normals adjacent to
172the shared edge are linearly independent. -/
173theorem faceNormals_independent_of_triple_ne_zero
174 {u v w : Fin 3 → ℝ}
175 (htriple : u ⬝ᵥ v ⨯₃ w ≠ 0) :
176 LinearIndependent ℝ ![u ⨯₃ v, u ⨯₃ w] := by
177 have hu : u ≠ 0 := by
178 intro hu0
179 apply htriple
180 simp [hu0]
181 have hcross : (u ⨯₃ v) ⨯₃ (u ⨯₃ w) ≠ 0 := by
182 rw [shared_edge_face_normals_cross]
183 exact smul_ne_zero htriple hu
184 exact (crossProduct_ne_zero_iff_linearIndependent).1 hcross
185
186/-- Linear independence of three coordinate vectors forces their scalar
187triple product to be nonzero. -/
188theorem scalar_triple_ne_zero_of_linearIndependent
189 {u v w : Fin 3 → ℝ}
190 (hlin : LinearIndependent ℝ ![u, v, w]) :
191 u ⬝ᵥ v ⨯₃ w ≠ 0 := by
192 have hunit : IsUnit (Matrix.of ![u, v, w]).det := by
193 have hrows : LinearIndependent ℝ (Matrix.of ![u, v, w]).row := by
194 simpa [Matrix.row] using hlin
195 exact (Matrix.isUnit_iff_isUnit_det _).1
196 ((Matrix.linearIndependent_rows_iff_isUnit).1 hrows)
197 have hdet_ne : Matrix.det ![u, v, w] ≠ 0 := hunit.ne_zero
198 simpa [triple_product_eq_det] using hdet_ne
199
200/-- Coordinate extraction through `EuclideanSpace.equiv` preserves linear
201independence. -/
202theorem coord_linearIndependent_of_euclidean
203 {v : Fin 3 → EuclideanSpace ℝ (Fin 3)}
204 (hlin : LinearIndependent ℝ v) :
205 LinearIndependent ℝ (fun i => (v i).ofLp) := by
206 let L := (EuclideanSpace.equiv (𝕜 := ℝ) (ι := Fin 3)).toLinearMap
207 have hmap : LinearIndependent ℝ (L ∘ v) := by
208 exact hlin.map' L (EuclideanSpace.equiv (𝕜 := ℝ) (ι := Fin 3)).toLinearEquiv.ker
209 simpa [L, Function.comp_def] using hmap
210
211/-- Edge-local scalar triple product nonvanishing implies adjacent face-normal
212independence. -/
213theorem adjacentFaceNormalsIndependent_of_triple_ne_zero
214 (T : RealizedTet) (e : Fin 6)
215 (htriple :
216 let edge := edgeVertices3 e
217 let opp := adjacentFaceOppositeVertices e
218 coordEdgeVector T edge.1 edge.2 ⬝ᵥ
219 coordEdgeVector T edge.1 opp.1 ⨯₃ coordEdgeVector T edge.1 opp.2 ≠ 0) :
220 AdjacentFaceNormalsIndependent T e := by
221 unfold AdjacentFaceNormalsIndependent adjacentFaceNormals faceNormal
222 dsimp at htriple ⊢
223 exact faceNormals_independent_of_triple_ne_zero htriple
224
225/-- The three base edge vectors of a realized tetrahedron are linearly
226independent. -/
227theorem basisEdgeVector_linearIndependent (T : RealizedTet) :
228 LinearIndependent ℝ (basisEdgeVector T) := by
229 have h := T.nondegenerate
230 rw [affineIndependent_iff_linearIndependent_vsub ℝ T.p (0 : Fin 4)] at h
231 let e : Fin 3 ≃ { j : Fin 4 // j ≠ 0 } := {
232 toFun := fun i =>
233 match i with
234 | 0 => ⟨1, by decide⟩
235 | 1 => ⟨2, by decide⟩
236 | 2 => ⟨3, by decide⟩
237 invFun := fun j =>
238 match j with
239 | ⟨1, _⟩ => 0
240 | ⟨2, _⟩ => 1
241 | ⟨3, _⟩ => 2
242 | ⟨0, h0⟩ => False.elim (h0 rfl)
243 left_inv := by
244 intro i
245 fin_cases i <;> rfl
246 right_inv := by
247 intro j
248 rcases j with ⟨j, hj⟩
249 fin_cases j <;> simp at hj ⊢
250 }
251 have h' := LinearIndependent.comp h e e.injective
252 convert h' using 1
253 ext i
254 fin_cases i <;> rfl
255
256/-- Coordinate edge vectors from any fixed base vertex to the other three
257vertices are linearly independent, for any ordering of those three vertices. -/
258theorem coordEdgeVector_from_base_linearIndependent
259 (T : RealizedTet) (base : Fin 4)
260 (e : Fin 3 ≃ { j : Fin 4 // j ≠ base }) :
261 LinearIndependent ℝ (fun i : Fin 3 => coordEdgeVector T base (e i).1) := by
262 have h := T.nondegenerate
263 rw [affineIndependent_iff_linearIndependent_vsub ℝ T.p base] at h
264 have h' := LinearIndependent.comp h e e.injective
265 have hcoord := coord_linearIndependent_of_euclidean h'
266 exact hcoord
267
268/-- For each tetrahedral edge, the shared edge and the two vectors to the
269opposite vertices form a linearly independent coordinate triple. -/
270theorem edge_opposite_coord_triple_linearIndependent
271 (T : RealizedTet) (e : Fin 6) :
272 let edge := edgeVertices3 e
273 let opp := adjacentFaceOppositeVertices e
274 LinearIndependent ℝ ![
275 coordEdgeVector T edge.1 edge.2,
276 coordEdgeVector T edge.1 opp.1,
277 coordEdgeVector T edge.1 opp.2] := by
278 fin_cases e
279 · let E : Fin 3 ≃ { j : Fin 4 // j ≠ 0 } := {
280 toFun := fun i =>
281 match i with
282 | 0 => ⟨1, by decide⟩
283 | 1 => ⟨2, by decide⟩
284 | 2 => ⟨3, by decide⟩
285 invFun := fun j =>
286 match j with
287 | ⟨1, _⟩ => 0
288 | ⟨2, _⟩ => 1
289 | ⟨3, _⟩ => 2
290 | ⟨0, h0⟩ => False.elim (h0 rfl)
291 left_inv := by intro i; fin_cases i <;> rfl
292 right_inv := by
293 intro j
294 rcases j with ⟨j, hj⟩
295 fin_cases j <;> simp at hj ⊢
296 }
297 simp [edgeVertices3, adjacentFaceOppositeVertices,
298 ReggeRigorousFoundation.edgeVertices]
299 convert coordEdgeVector_from_base_linearIndependent T 0 E using 1
300 ext i
301 fin_cases i <;> rfl
302 · let E : Fin 3 ≃ { j : Fin 4 // j ≠ 0 } := {
303 toFun := fun i =>
304 match i with
305 | 0 => ⟨2, by decide⟩
306 | 1 => ⟨1, by decide⟩
307 | 2 => ⟨3, by decide⟩
308 invFun := fun j =>
309 match j with
310 | ⟨2, _⟩ => 0
311 | ⟨1, _⟩ => 1
312 | ⟨3, _⟩ => 2
313 | ⟨0, h0⟩ => False.elim (h0 rfl)
314 left_inv := by intro i; fin_cases i <;> rfl
315 right_inv := by
316 intro j
317 rcases j with ⟨j, hj⟩
318 fin_cases j <;> simp at hj ⊢
319 }
320 simp [edgeVertices3, adjacentFaceOppositeVertices,
321 ReggeRigorousFoundation.edgeVertices]
322 convert coordEdgeVector_from_base_linearIndependent T 0 E using 1
323 ext i
324 fin_cases i <;> rfl
325 · let E : Fin 3 ≃ { j : Fin 4 // j ≠ 0 } := {
326 toFun := fun i =>
327 match i with
328 | 0 => ⟨3, by decide⟩
329 | 1 => ⟨1, by decide⟩
330 | 2 => ⟨2, by decide⟩
331 invFun := fun j =>
332 match j with
333 | ⟨3, _⟩ => 0
334 | ⟨1, _⟩ => 1
335 | ⟨2, _⟩ => 2
336 | ⟨0, h0⟩ => False.elim (h0 rfl)
337 left_inv := by intro i; fin_cases i <;> rfl
338 right_inv := by
339 intro j
340 rcases j with ⟨j, hj⟩
341 fin_cases j <;> simp at hj ⊢
342 }
343 simp [edgeVertices3, adjacentFaceOppositeVertices,
344 ReggeRigorousFoundation.edgeVertices]
345 convert coordEdgeVector_from_base_linearIndependent T 0 E using 1
346 ext i
347 fin_cases i <;> rfl
348 · let E : Fin 3 ≃ { j : Fin 4 // j ≠ 1 } := {
349 toFun := fun i =>
350 match i with
351 | 0 => ⟨2, by decide⟩
352 | 1 => ⟨0, by decide⟩
353 | 2 => ⟨3, by decide⟩
354 invFun := fun j =>
355 match j with
356 | ⟨2, _⟩ => 0
357 | ⟨0, _⟩ => 1
358 | ⟨3, _⟩ => 2
359 | ⟨1, h1⟩ => False.elim (h1 rfl)
360 left_inv := by intro i; fin_cases i <;> rfl
361 right_inv := by
362 intro j
363 rcases j with ⟨j, hj⟩
364 fin_cases j <;> simp at hj ⊢
365 }
366 simp [edgeVertices3, adjacentFaceOppositeVertices,
367 ReggeRigorousFoundation.edgeVertices]
368 convert coordEdgeVector_from_base_linearIndependent T 1 E using 1
369 ext i
370 fin_cases i <;> rfl
371 · let E : Fin 3 ≃ { j : Fin 4 // j ≠ 1 } := {
372 toFun := fun i =>
373 match i with
374 | 0 => ⟨3, by decide⟩
375 | 1 => ⟨0, by decide⟩
376 | 2 => ⟨2, by decide⟩
377 invFun := fun j =>
378 match j with
379 | ⟨3, _⟩ => 0
380 | ⟨0, _⟩ => 1
381 | ⟨2, _⟩ => 2
382 | ⟨1, h1⟩ => False.elim (h1 rfl)
383 left_inv := by intro i; fin_cases i <;> rfl
384 right_inv := by
385 intro j
386 rcases j with ⟨j, hj⟩
387 fin_cases j <;> simp at hj ⊢
388 }
389 simp [edgeVertices3, adjacentFaceOppositeVertices,
390 ReggeRigorousFoundation.edgeVertices]
391 convert coordEdgeVector_from_base_linearIndependent T 1 E using 1
392 ext i
393 fin_cases i <;> rfl
394 · let E : Fin 3 ≃ { j : Fin 4 // j ≠ 2 } := {
395 toFun := fun i =>
396 match i with
397 | 0 => ⟨3, by decide⟩
398 | 1 => ⟨0, by decide⟩
399 | 2 => ⟨1, by decide⟩
400 invFun := fun j =>
401 match j with
402 | ⟨3, _⟩ => 0
403 | ⟨0, _⟩ => 1
404 | ⟨1, _⟩ => 2
405 | ⟨2, h2⟩ => False.elim (h2 rfl)
406 left_inv := by intro i; fin_cases i <;> rfl
407 right_inv := by
408 intro j
409 rcases j with ⟨j, hj⟩
410 fin_cases j <;> simp at hj ⊢
411 }
412 simp [edgeVertices3, adjacentFaceOppositeVertices,
413 ReggeRigorousFoundation.edgeVertices]
414 convert coordEdgeVector_from_base_linearIndependent T 2 E using 1
415 ext i
416 fin_cases i <;> rfl
417
418/-- Affine independence of the tetrahedron implies adjacent face-normal
419independence for every edge. -/
420theorem adjacentFaceNormalsIndependent_of_affineIndependent
421 (T : RealizedTet) (e : Fin 6) :
422 AdjacentFaceNormalsIndependent T e := by
423 have hlin := edge_opposite_coord_triple_linearIndependent T e
424 have htriple := scalar_triple_ne_zero_of_linearIndependent hlin
425 exact adjacentFaceNormalsIndependent_of_triple_ne_zero T e htriple
426
427/-- Strict interior for the geometric dihedral cosine, given linear
428independence of the two adjacent face normals. -/
429theorem geometricDihedralCos_strict_interior_of_faceNormals_independent
430 (T : RealizedTet) (e : Fin 6)
431 (hlin : AdjacentFaceNormalsIndependent T e) :
432 -1 < geometricDihedralCos T e ∧ geometricDihedralCos T e < 1 := by
433 refine geometricDihedralCos_interior_of_ne_endpoints T e ?_ ?_
434 · unfold geometricDihedralCos geometricDihedralNumerator geometricDihedralDenomSq
435 unfold AdjacentFaceNormalsIndependent adjacentFaceNormals at hlin
436 dsimp at hlin ⊢
437 exact dot_div_sqrt_ne_neg_one_of_linearIndependent hlin
438 · unfold geometricDihedralCos geometricDihedralNumerator geometricDihedralDenomSq
439 unfold AdjacentFaceNormalsIndependent adjacentFaceNormals at hlin
440 dsimp at hlin ⊢
441 exact dot_div_sqrt_ne_one_of_linearIndependent hlin
442
443/-- Strict interior transferred to the Cayley-Menger cofactor cosine for a
444realized tetrahedron. -/
445theorem dihedralCos3Sq_strict_interior_of_faceNormals_independent
446 (T : RealizedTet) (e : Fin 6)
447 (hlin : AdjacentFaceNormalsIndependent T e) :
448 -1 < dihedralCos3Sq (sqEdgeOfPoints T) e ∧
449 dihedralCos3Sq (sqEdgeOfPoints T) e < 1 := by
450 rw [← geometricDihedralCos_eq_cmCofactorRatio T e]
451 exact geometricDihedralCos_strict_interior_of_faceNormals_independent T e hlin
452
453/-- Affine independence of the realized tetrahedron gives strict interior for
454the geometric dihedral cosine at every edge. -/
455theorem geometricDihedralCos_strict_interior_of_affineIndependent
456 (T : RealizedTet) (e : Fin 6) :
457 -1 < geometricDihedralCos T e ∧ geometricDihedralCos T e < 1 :=
458 geometricDihedralCos_strict_interior_of_faceNormals_independent T e
459 (adjacentFaceNormalsIndependent_of_affineIndependent T e)
460
461/-- Affine independence of the realized tetrahedron gives strict interior for
462the Cayley-Menger cofactor cosine at every edge. -/
463theorem dihedralCos3Sq_strict_interior_of_affineIndependent
464 (T : RealizedTet) (e : Fin 6) :
465 -1 < dihedralCos3Sq (sqEdgeOfPoints T) e ∧
466 dihedralCos3Sq (sqEdgeOfPoints T) e < 1 :=
467 dihedralCos3Sq_strict_interior_of_faceNormals_independent T e
468 (adjacentFaceNormalsIndependent_of_affineIndependent T e)
469
470/-- A realized nondegenerate tetrahedron packages an abstract
471`NonDegenerateTet` with a Euclidean realization and the face-normal
472independence needed for strict dihedral interior. The final affine
473independence closure target is to build the last field from
474`RealizedTet.nondegenerate` alone. -/
475structure RealizedNonDegenerateTet where
476 tet : ReggeRigorousFoundation.NonDegenerateTet
477 realization : RealizedTet
478 realizes : sqEdgeOfPoints realization = tet.sqEdge
479
480theorem RealizedNonDegenerateTet.dihedralCos3_strict_interior
481 (T : RealizedNonDegenerateTet) (e : Fin 6) :
482 -1 < dihedralCos3 T.tet e ∧ dihedralCos3 T.tet e < 1 := by
483 unfold dihedralCos3
484 rw [← T.realizes]
485 exact dihedralCos3Sq_strict_interior_of_affineIndependent T.realization e
486
487/-- Construct angle data from a realized tetrahedron with proved strict
488interior, without caller-supplied endpoint or range hypotheses. -/
489def RealizedNonDegenerateTet.dihedralAngleData3
490 (T : RealizedNonDegenerateTet) (e : Fin 6) :
491 DihedralAngle.DihedralAngleData :=
492 let h := T.dihedralCos3_strict_interior e
493 DihedralCayleyMenger.dihedralAngleData3 T.tet e (le_of_lt h.1) (le_of_lt h.2)
494
495end
496
497end AffineIndepInterior
498end Geometry
499end IndisputableMonolith
500