IndisputableMonolith.Geometry.SchlaefliTetrahedronProof
IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean · 850 lines · 45 declarations
show as:
view math explainer →
1import IndisputableMonolith.Geometry.SchlaefliTetrahedron
2import IndisputableMonolith.Geometry.DihedralDerivatives
3import IndisputableMonolith.Geometry.AffineIndepInterior
4
5/-!
6# Closed-Form Tetrahedral Schläfli Target
7
8This module connects the explicit Cayley-Menger and dihedral derivative
9values to the local tetrahedral Schläfli package. The hard remaining
10content is now a single closed-form identity, not an implicit external
11field.
12-/
13
14namespace IndisputableMonolith
15namespace Geometry
16namespace SchlaefliTetrahedronProof
17
18open CayleyMengerPolynomial
19open CayleyMengerDerivatives
20open DihedralDerivatives
21open SchlaefliTetrahedron
22open ReggeRigorousFoundation
23open AffineIndepInterior
24
25noncomputable section
26
27/-- Closed-form derivative value for `V = sqrt (cm3 / 288)` with respect
28to a squared-edge coordinate. -/
29def volume3ClosedDerivSq (a : SqEdges) (k : Fin 6) : ℝ :=
30 cm3_grad a k / (576 * Real.sqrt (cm3 a / 288))
31
32/-- The closed-form squared-edge derivative of tetrahedral volume is the
33actual derivative of `volume3SqEdges`. -/
34theorem hasDerivAt_volume3ClosedDerivSq
35 (T : NonDegenerateTet) (k : Fin 6) :
36 HasDerivAt
37 (fun t : ℝ => volume3SqEdges (Function.update T.sqEdge k t))
38 (volume3ClosedDerivSq T.sqEdge k) (T.sqEdge k) := by
39 unfold volume3ClosedDerivSq
40 have hbase : Function.update T.sqEdge k (T.sqEdge k) = T.sqEdge := by
41 funext i
42 by_cases hi : i = k <;> simp [Function.update, hi]
43 have h := hasDerivAt_volume3_along
44 (γ := fun t : ℝ => Function.update T.sqEdge k t)
45 (x := T.sqEdge k)
46 (cmDeriv := cm3_grad T.sqEdge k)
47 (hasDerivAt_cm3_grad T.sqEdge k)
48 (by
49 have h288 : (0 : ℝ) < 288 := by norm_num
50 simpa [hbase] using div_pos T.cm_pos h288)
51 simpa [hbase] using h
52
53/-- Closed-form derivative value for the dihedral angle at edge `e` with
54respect to squared-edge coordinate `k`. -/
55def dihedralClosedDerivSq (T : NonDegenerateTet) (e k : Fin 6) : ℝ :=
56 dihedralAngle3SqClosedFormDeriv T.sqEdge e k
57
58/-- Polynomial-cofactor version of the squared-edge dihedral derivative
59value. This is definitionally lighter than `dihedralClosedDerivSq` and is
60the preferred target for the six algebraic Schläfli identities. -/
61def dihedralClosedDerivSqPoly (T : NonDegenerateTet) (e k : Fin 6) : ℝ :=
62 -(1 / Real.sqrt (1 - (CofactorDerivatives.dihedralCos3SqPoly T.sqEdge e) ^ 2)) *
63 CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv T.sqEdge e k
64
65theorem dihedralClosedDerivSq_eq_poly
66 (T : NonDegenerateTet) (e k : Fin 6) :
67 dihedralClosedDerivSq T e k = dihedralClosedDerivSqPoly T e k := by
68 unfold dihedralClosedDerivSq dihedralClosedDerivSqPoly
69 unfold DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
70 rw [CofactorDerivatives.dihedralCos3Sq_eq_poly]
71 rw [CofactorDerivatives.dihedralCos3SqClosedFormDeriv_eq_poly]
72
73/-- The square map derivative at the positive edge length `sqrt (a k)`.
74This is the scalar chain-rule factor behind `d/dL = 2L d/da`. -/
75theorem hasDerivAt_sqEdgeCoordinate_from_edgeLength
76 (T : NonDegenerateTet) (k : Fin 6) :
77 HasDerivAt (fun L : ℝ => L ^ 2)
78 (2 * Real.sqrt (T.sqEdge k)) (Real.sqrt (T.sqEdge k)) := by
79 have h := (hasDerivAt_id (Real.sqrt (T.sqEdge k))).pow 2
80 simpa [pow_succ, two_mul, mul_comm, mul_left_comm, mul_assoc] using h
81
82/-- Convert a squared-edge derivative of volume to an edge-length derivative. -/
83def volume3ClosedDerivLength (T : NonDegenerateTet) (k : Fin 6) : ℝ :=
84 2 * Real.sqrt (T.sqEdge k) * volume3ClosedDerivSq T.sqEdge k
85
86/-- The closed-form edge-length derivative of volume is obtained from the
87squared-edge derivative by `d(a_k)/dL_k = 2 L_k`. -/
88theorem hasDerivAt_volume3ClosedDerivLength
89 (T : NonDegenerateTet) (k : Fin 6) :
90 HasDerivAt
91 (fun L : ℝ => volume3SqEdges (Function.update T.sqEdge k (L ^ 2)))
92 (volume3ClosedDerivLength T k) (Real.sqrt (T.sqEdge k)) := by
93 unfold volume3ClosedDerivLength
94 have hsq := hasDerivAt_sqEdgeCoordinate_from_edgeLength T k
95 have hsqsqrt : Real.sqrt (T.sqEdge k) ^ 2 = T.sqEdge k :=
96 Real.sq_sqrt (le_of_lt (T.sqEdge_pos k))
97 have hvol : HasDerivAt
98 (fun t : ℝ => volume3SqEdges (Function.update T.sqEdge k t))
99 (volume3ClosedDerivSq T.sqEdge k)
100 (Real.sqrt (T.sqEdge k) ^ 2) := by
101 simpa [hsqsqrt] using hasDerivAt_volume3ClosedDerivSq T k
102 have hcomp := HasDerivAt.comp_of_eq
103 (x := Real.sqrt (T.sqEdge k)) hvol hsq rfl
104 simpa [mul_comm, mul_left_comm, mul_assoc] using hcomp
105
106/-- Convert a squared-edge derivative of a dihedral angle to an edge-length
107derivative. -/
108def dihedralClosedDerivLength (T : NonDegenerateTet) (e k : Fin 6) : ℝ :=
109 2 * Real.sqrt (T.sqEdge k) * dihedralClosedDerivSq T e k
110
111/-- The closed-form edge-length derivative of a dihedral angle is obtained
112from the squared-edge derivative by `d(a_k)/dL_k = 2 L_k`, under the local
113smoothness hypotheses for the cofactor angle. -/
114theorem hasDerivAt_dihedralClosedDerivLength
115 (T : NonDegenerateTet) (e k : Fin 6)
116 (hprod_ne :
117 (let p := DihedralCayleyMenger.oppositeCMVertices e |>.1
118 let q := DihedralCayleyMenger.oppositeCMVertices e |>.2
119 CayleyMengerMatrix.cmCofactor3 T.sqEdge p p *
120 CayleyMengerMatrix.cmCofactor3 T.sqEdge q q) ≠ 0)
121 (hden_ne : DihedralCayleyMenger.dihedralDenom3 T.sqEdge e ≠ 0)
122 (hm : DihedralCayleyMenger.dihedralCos3Sq T.sqEdge e ≠ -1)
123 (hp : DihedralCayleyMenger.dihedralCos3Sq T.sqEdge e ≠ 1) :
124 HasDerivAt
125 (fun L : ℝ =>
126 dihedralAngle3Sq (Function.update T.sqEdge k (L ^ 2)) e)
127 (dihedralClosedDerivLength T e k) (Real.sqrt (T.sqEdge k)) := by
128 unfold dihedralClosedDerivLength dihedralClosedDerivSq
129 have hsq := hasDerivAt_sqEdgeCoordinate_from_edgeLength T k
130 have hsqsqrt : Real.sqrt (T.sqEdge k) ^ 2 = T.sqEdge k :=
131 Real.sq_sqrt (le_of_lt (T.sqEdge_pos k))
132 have hangle : HasDerivAt
133 (fun t : ℝ => dihedralAngle3Sq (Function.update T.sqEdge k t) e)
134 (dihedralAngle3SqClosedFormDeriv T.sqEdge e k)
135 (Real.sqrt (T.sqEdge k) ^ 2) := by
136 simpa [hsqsqrt] using
137 hasDerivAt_dihedralAngle3Sq_explicit T.sqEdge e k hprod_ne hden_ne hm hp
138 have hcomp := HasDerivAt.comp_of_eq
139 (x := Real.sqrt (T.sqEdge k)) hangle hsq rfl
140 simpa [mul_comm, mul_left_comm, mul_assoc] using hcomp
141
142/-- The local Schläfli equation with the old squared-edge derivative
143coordinates. This is kept only as an internal algebraic target; the actual
144Schläfli package below uses edge-length derivatives. -/
145def TetraSchlaefliClosedEquationSq (T : NonDegenerateTet) : Prop :=
146 TetraSchlaefliEquation T
147 (fun e k => dihedralClosedDerivSq T e k)
148 (fun k => volume3ClosedDerivSq T.sqEdge k)
149
150/-- The local Schläfli equation after converting closed-form squared-edge
151derivatives to edge-length derivatives. -/
152def TetraSchlaefliClosedEquation (T : NonDegenerateTet) : Prop :=
153 TetraSchlaefliEquation T
154 (fun e k => dihedralClosedDerivLength T e k)
155 (fun k => volume3ClosedDerivLength T k)
156
157/-- The corrected edge-length Schläfli equation follows from the squared-edge
158closed-form equation by multiplying the fixed-coordinate equation by
159`2 * sqrt (a_k)`. -/
160theorem TetraSchlaefliClosedEquation_of_sq
161 (T : NonDegenerateTet)
162 (hSq : TetraSchlaefliClosedEquationSq T) :
163 TetraSchlaefliClosedEquation T := by
164 intro k
165 unfold dihedralClosedDerivLength
166 unfold TetraSchlaefliClosedEquationSq TetraSchlaefliEquation at hSq
167 have h := hSq k
168 calc
169 (∑ e : Fin 6,
170 Real.sqrt (T.sqEdge e) *
171 (2 * Real.sqrt (T.sqEdge k) * dihedralClosedDerivSq T e k))
172 = 2 * Real.sqrt (T.sqEdge k) *
173 (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralClosedDerivSq T e k) := by
174 rw [Finset.mul_sum]
175 refine Finset.sum_congr rfl ?_
176 intro e _
177 ring
178 _ = 2 * Real.sqrt (T.sqEdge k) * 0 := by
179 rw [h]
180 _ = 0 := by
181 ring
182
183/-- The theorem target left by the closed-form reduction. -/
184def SchlaefliTetrahedronClosedFormTarget : Prop :=
185 ∀ T : NonDegenerateTet, TetraSchlaefliClosedEquation T
186
187/-- The six edge-coordinate closed-form Schläfli identities, stated after
188the squared-edge algebraic reduction. This is the finite algebraic core left
189to prove. -/
190def TetraSchlaefliSixEdgeClosedFormTarget : Prop :=
191 ∀ T : NonDegenerateTet, ∀ k : Fin 6,
192 (∑ e : Fin 6,
193 Real.sqrt (T.sqEdge e) * dihedralClosedDerivSq T e k)
194 = 0
195
196/-- Polynomial-cofactor form of the six algebraic Schläfli identities. -/
197def TetraSchlaefliSixEdgePolynomialTarget : Prop :=
198 ∀ T : NonDegenerateTet, ∀ k : Fin 6,
199 (∑ e : Fin 6,
200 Real.sqrt (T.sqEdge e) * dihedralClosedDerivSqPoly T e k)
201 = 0
202
203/-- Rationalized Schläfli summand after using the cofactor discriminant to
204remove the arccos radical. Up to the common nonzero factor
205`1 / sqrt (2 * cm3 a)`, the original polynomial-cofactor summand is this
206pure rational expression. -/
207def schlaefliPolySummandNorm (a : SqEdges) (e k : Fin 6) : ℝ :=
208 match e with
209 | 0 =>
210 let P := CofactorPolynomial.cmCofactor3Poly 3 3 a
211 let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
212 let N := CofactorPolynomial.cmCofactor3Poly 3 4 a
213 let Pp := CofactorPolynomial.cmCofactorPartial 3 3 k a
214 let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
215 let Np := CofactorPolynomial.cmCofactorPartial 3 4 k a
216 (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
217 | 1 =>
218 let P := CofactorPolynomial.cmCofactor3Poly 2 2 a
219 let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
220 let N := CofactorPolynomial.cmCofactor3Poly 2 4 a
221 let Pp := CofactorPolynomial.cmCofactorPartial 2 2 k a
222 let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
223 let Np := CofactorPolynomial.cmCofactorPartial 2 4 k a
224 (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
225 | 2 =>
226 let P := CofactorPolynomial.cmCofactor3Poly 2 2 a
227 let Q := CofactorPolynomial.cmCofactor3Poly 3 3 a
228 let N := CofactorPolynomial.cmCofactor3Poly 2 3 a
229 let Pp := CofactorPolynomial.cmCofactorPartial 2 2 k a
230 let Qp := CofactorPolynomial.cmCofactorPartial 3 3 k a
231 let Np := CofactorPolynomial.cmCofactorPartial 2 3 k a
232 (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
233 | 3 =>
234 let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
235 let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
236 let N := CofactorPolynomial.cmCofactor3Poly 1 4 a
237 let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
238 let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
239 let Np := CofactorPolynomial.cmCofactorPartial 1 4 k a
240 (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
241 | 4 =>
242 let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
243 let Q := CofactorPolynomial.cmCofactor3Poly 3 3 a
244 let N := CofactorPolynomial.cmCofactor3Poly 1 3 a
245 let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
246 let Qp := CofactorPolynomial.cmCofactorPartial 3 3 k a
247 let Np := CofactorPolynomial.cmCofactorPartial 1 3 k a
248 (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
249 | 5 =>
250 let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
251 let Q := CofactorPolynomial.cmCofactor3Poly 2 2 a
252 let N := CofactorPolynomial.cmCofactor3Poly 1 2 a
253 let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
254 let Qp := CofactorPolynomial.cmCofactorPartial 2 2 k a
255 let Np := CofactorPolynomial.cmCofactorPartial 1 2 k a
256 (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
257
258/-- Numerator of the rationalized Schläfli summand. -/
259def schlaefliPolySummandNum (a : SqEdges) (e k : Fin 6) : ℝ :=
260 let p := DihedralCayleyMenger.oppositeCMVertices e |>.1
261 let q := DihedralCayleyMenger.oppositeCMVertices e |>.2
262 let P := CofactorPolynomial.cmCofactor3Poly p p a
263 let Q := CofactorPolynomial.cmCofactor3Poly q q a
264 let N := CofactorPolynomial.cmCofactor3Poly p q a
265 let Pp := CofactorPolynomial.cmCofactorPartial p p k a
266 let Qp := CofactorPolynomial.cmCofactorPartial q q k a
267 let Np := CofactorPolynomial.cmCofactorPartial p q k a
268 (-(2 * Np * P * Q - N * (Pp * Q + P * Qp)))
269
270/-- Denominator of the rationalized Schläfli summand. -/
271def schlaefliPolySummandDen (a : SqEdges) (e : Fin 6) : ℝ :=
272 let p := DihedralCayleyMenger.oppositeCMVertices e |>.1
273 let q := DihedralCayleyMenger.oppositeCMVertices e |>.2
274 2 * CofactorPolynomial.cmCofactor3Poly p p a *
275 CofactorPolynomial.cmCofactor3Poly q q a
276
277/-- The normalized summand is numerator divided by denominator. -/
278theorem schlaefliPolySummandNorm_eq_num_div_den
279 (a : SqEdges) (e k : Fin 6) :
280 schlaefliPolySummandNorm a e k =
281 schlaefliPolySummandNum a e k / schlaefliPolySummandDen a e := by
282 fin_cases e <;>
283 simp [schlaefliPolySummandNorm, schlaefliPolySummandNum,
284 schlaefliPolySummandDen, DihedralCayleyMenger.oppositeCMVertices]
285
286/-- Product denominator for clearing the six rational Schläfli summands. -/
287def schlaefliCommonDenom (a : SqEdges) : ℝ :=
288 ∏ e : Fin 6, schlaefliPolySummandDen a e
289
290/-- Common numerator after clearing all six rational Schläfli summands. -/
291def schlaefliCommonNumerator (a : SqEdges) (k : Fin 6) : ℝ :=
292 ∑ e : Fin 6,
293 schlaefliPolySummandNum a e k *
294 ∏ j ∈ (Finset.univ.erase e), schlaefliPolySummandDen a j
295
296/-- Each rationalized Schläfli summand denominator is nonzero on a
297nondegenerate tetrahedron. -/
298theorem schlaefliPolySummandDen_ne_zero
299 (T : NonDegenerateTet) (e : Fin 6) :
300 schlaefliPolySummandDen T.sqEdge e ≠ 0 := by
301 unfold schlaefliPolySummandDen
302 have hprod := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T e
303 fin_cases e <;>
304 simpa [DihedralCayleyMenger.oppositeCMVertices,
305 CofactorDerivatives.dihedralCofactorProductPoly, mul_assoc] using
306 mul_ne_zero two_ne_zero hprod
307
308/-- The common denominator is nonzero on a nondegenerate tetrahedron. -/
309theorem schlaefliCommonDenom_ne_zero
310 (T : NonDegenerateTet) :
311 schlaefliCommonDenom T.sqEdge ≠ 0 := by
312 unfold schlaefliCommonDenom
313 exact Finset.prod_ne_zero_iff.mpr (by
314 intro e _
315 exact schlaefliPolySummandDen_ne_zero T e)
316
317/-- Remaining common-numerator closure target. The intended proof is six
318coordinate-specific numerator lemmas rather than one global unfold. -/
319def SchlaefliCommonNumeratorTarget : Prop :=
320 ∀ a : SqEdges, ∀ k : Fin 6, schlaefliCommonNumerator a k = 0
321
322/-- The rationalized six-edge Schläfli identities. This is the remaining
323post-radical-normalization target: prove these six rational sums by expanding
324`schlaefliPolySummandNorm`, clearing the cofactor-product denominators, and
325finishing with `ring_nf`. -/
326def SchlaefliPolySummandNormSumTarget : Prop :=
327 ∀ T : NonDegenerateTet, ∀ k : Fin 6,
328 (∑ e : Fin 6, schlaefliPolySummandNorm T.sqEdge e k) = 0
329
330/-- Explicit expansion of a six-term finite sum over `Fin 6`. -/
331theorem sum_fin6_real (f : Fin 6 → ℝ) :
332 (∑ e : Fin 6, f e) =
333 f 0 + f 1 + f 2 + f 3 + f 4 + f 5 := by
334 norm_num [Fin.sum_univ_succ]
335 change f 0 + (f 1 + (f 2 + (f 3 + (f 4 + f 5)))) =
336 f 0 + f 1 + f 2 + f 3 + f 4 + f 5
337 ring
338
339/- The next closure step is to prove the six coordinate instances of
340`SchlaefliPolySummandNormSumTarget`. Direct global unfolding still creates
341large inverse-normalized goals, so the intended implementation is one
342coordinate numerator lemma at a time. -/
343
344set_option maxHeartbeats 8000000
345set_option maxRecDepth 4096
346/-- The rationalized six-edge Schläfli sums vanish. -/
347theorem schlaefliPolySummandNorm_sum_eq_zero :
348 SchlaefliPolySummandNormSumTarget := by
349 intro T k
350 rw [sum_fin6_real]
351 have h0p := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 0
352 have h1p := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 1
353 have h5p := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 5
354 simp [CofactorDerivatives.dihedralCofactorProductPoly,
355 DihedralCayleyMenger.oppositeCMVertices] at h0p h1p h5p
356 have h33 : CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge ≠ 0 := h0p.1
357 have h44 : CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 := h0p.2
358 have h22 : CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge ≠ 0 := h1p.1
359 have h11 : CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge ≠ 0 := h5p.1
360 let D : ℝ :=
361 CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
362 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
363 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge *
364 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge
365 have hD : D ≠ 0 := by
366 unfold D
367 exact mul_ne_zero (mul_ne_zero (mul_ne_zero h11 h22) h33) h44
368 have hmul :
369 D * (schlaefliPolySummandNorm T.sqEdge 0 k +
370 schlaefliPolySummandNorm T.sqEdge 1 k +
371 schlaefliPolySummandNorm T.sqEdge 2 k +
372 schlaefliPolySummandNorm T.sqEdge 3 k +
373 schlaefliPolySummandNorm T.sqEdge 4 k +
374 schlaefliPolySummandNorm T.sqEdge 5 k) = 0 := by
375 fin_cases k <;>
376 unfold D schlaefliPolySummandNorm <;>
377 field_simp [h11, h22, h33, h44] <;>
378 simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial] <;>
379 ring_nf
380 exact (mul_eq_zero.mp hmul).resolve_left hD
381
382/-- Remaining bridge target: each polynomial-cofactor Schläfli summand should
383equal the rationalized summand times the common factor
384`1 / sqrt (2 * cm3)`. The normalized rational sum is already proved; this
385bridge is the last radical-cancellation step before
386`TetraSchlaefliSixEdgePolynomialTarget`. -/
387def SchlaefliSummandBridgeTarget : Prop :=
388 ∀ T : NonDegenerateTet, ∀ e k : Fin 6,
389 Real.sqrt (T.sqEdge e) * dihedralClosedDerivSqPoly T e k =
390 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
391 schlaefliPolySummandNorm T.sqEdge e k
392
393set_option maxHeartbeats 4000000
394/-- Radical bridge for edge `0`. -/
395theorem schlaefli_summand_bridge_edge0
396 (T : NonDegenerateTet) (k : Fin 6) :
397 Real.sqrt (T.sqEdge 0) * dihedralClosedDerivSqPoly T 0 k =
398 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
399 schlaefliPolySummandNorm T.sqEdge 0 k := by
400 unfold dihedralClosedDerivSqPoly
401 have hp_nonneg := CofactorDerivatives.dihedralCofactorProductPoly_nonneg_of_nonDegenerate T 0
402 have hp_exp : 0 ≤
403 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge *
404 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge := by
405 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
406 DihedralCayleyMenger.oppositeCMVertices] using hp_nonneg
407 have hp_ne := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 0
408 have hp_exp_ne :
409 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge *
410 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 := by
411 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
412 DihedralCayleyMenger.oppositeCMVertices] using hp_ne
413 have h33 : CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge ≠ 0 :=
414 (mul_ne_zero_iff.mp hp_exp_ne).1
415 have h44 : CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 :=
416 (mul_ne_zero_iff.mp hp_exp_ne).2
417 have hd_ne := CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T 0
418 have hnum_nonneg : 0 ≤ 2 * cm3 T.sqEdge * T.sqEdge 0 := by
419 nlinarith [T.cm_pos, T.sqEdge_pos 0]
420 rw [CofactorDerivatives.sqrt_one_sub_dihedralCos3SqPoly_sq_eq
421 T.sqEdge 0 hp_nonneg hp_ne hd_ne hnum_nonneg]
422 have hsqrt : Real.sqrt (2 * cm3 T.sqEdge * T.sqEdge 0) =
423 Real.sqrt (2 * cm3 T.sqEdge) * Real.sqrt (T.sqEdge 0) := by
424 have hleft : 0 ≤ 2 * cm3 T.sqEdge := by nlinarith [T.cm_pos]
425 rw [show 2 * cm3 T.sqEdge * T.sqEdge 0 =
426 (2 * cm3 T.sqEdge) * T.sqEdge 0 by ring]
427 rw [Real.sqrt_mul hleft]
428 rw [hsqrt]
429 simp [CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
430 CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
431 CofactorDerivatives.dihedralDenom3Poly,
432 DihedralCayleyMenger.oppositeCMVertices,
433 schlaefliPolySummandNorm]
434 have hcm : Real.sqrt (2 * cm3 T.sqEdge) ≠ 0 :=
435 Real.sqrt_ne_zero'.mpr (by nlinarith [T.cm_pos] : 0 < 2 * cm3 T.sqEdge)
436 have he : Real.sqrt (T.sqEdge 0) ≠ 0 :=
437 Real.sqrt_ne_zero'.mpr (T.sqEdge_pos 0)
438 have hd :
439 Real.sqrt (CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge *
440 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge) ≠ 0 := by
441 simpa [CofactorDerivatives.dihedralDenom3Poly,
442 DihedralCayleyMenger.oppositeCMVertices] using hd_ne
443 field_simp [hcm, he, hd]
444 rw [Real.sq_sqrt hp_exp]
445 field_simp [hcm, h33, h44]
446 fin_cases k <;>
447 simp [CofactorPolynomial.cmCofactor3Poly,
448 CofactorPolynomial.cmCofactorPartial] <;>
449 ring_nf
450
451
452/-- Radical bridge for edge `1`. -/
453theorem schlaefli_summand_bridge_edge1
454 (T : NonDegenerateTet) (k : Fin 6) :
455 Real.sqrt (T.sqEdge 1) * dihedralClosedDerivSqPoly T 1 k =
456 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
457 schlaefliPolySummandNorm T.sqEdge 1 k := by
458 unfold dihedralClosedDerivSqPoly
459 have hp_nonneg := CofactorDerivatives.dihedralCofactorProductPoly_nonneg_of_nonDegenerate T 1
460 have hp_exp : 0 ≤
461 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
462 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge := by
463 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
464 DihedralCayleyMenger.oppositeCMVertices] using hp_nonneg
465 have hp_ne := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 1
466 have hp_exp_ne :
467 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
468 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 := by
469 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
470 DihedralCayleyMenger.oppositeCMVertices] using hp_ne
471 have hp_left : CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge ≠ 0 :=
472 (mul_ne_zero_iff.mp hp_exp_ne).1
473 have hp_right : CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 :=
474 (mul_ne_zero_iff.mp hp_exp_ne).2
475 have hd_ne := CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T 1
476 have hnum_nonneg : 0 ≤ 2 * cm3 T.sqEdge * T.sqEdge 1 := by
477 nlinarith [T.cm_pos, T.sqEdge_pos 1]
478 rw [CofactorDerivatives.sqrt_one_sub_dihedralCos3SqPoly_sq_eq
479 T.sqEdge 1 hp_nonneg hp_ne hd_ne hnum_nonneg]
480 have hsqrt : Real.sqrt (2 * cm3 T.sqEdge * T.sqEdge 1) =
481 Real.sqrt (2 * cm3 T.sqEdge) * Real.sqrt (T.sqEdge 1) := by
482 have hleft : 0 ≤ 2 * cm3 T.sqEdge := by nlinarith [T.cm_pos]
483 rw [show 2 * cm3 T.sqEdge * T.sqEdge 1 =
484 (2 * cm3 T.sqEdge) * T.sqEdge 1 by ring]
485 rw [Real.sqrt_mul hleft]
486 rw [hsqrt]
487 simp [CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
488 CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
489 CofactorDerivatives.dihedralDenom3Poly,
490 DihedralCayleyMenger.oppositeCMVertices,
491 schlaefliPolySummandNorm]
492 have hcm : Real.sqrt (2 * cm3 T.sqEdge) ≠ 0 :=
493 Real.sqrt_ne_zero'.mpr (by nlinarith [T.cm_pos] : 0 < 2 * cm3 T.sqEdge)
494 have he : Real.sqrt (T.sqEdge 1) ≠ 0 :=
495 Real.sqrt_ne_zero'.mpr (T.sqEdge_pos 1)
496 have hd :
497 Real.sqrt (CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
498 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge) ≠ 0 := by
499 simpa [CofactorDerivatives.dihedralDenom3Poly,
500 DihedralCayleyMenger.oppositeCMVertices] using hd_ne
501 field_simp [hcm, he, hd]
502 rw [Real.sq_sqrt hp_exp]
503 field_simp [hcm, hp_left, hp_right]
504 fin_cases k <;>
505 simp [CofactorPolynomial.cmCofactor3Poly,
506 CofactorPolynomial.cmCofactorPartial] <;>
507 ring_nf
508
509/-- Radical bridge for edge `2`. -/
510theorem schlaefli_summand_bridge_edge2
511 (T : NonDegenerateTet) (k : Fin 6) :
512 Real.sqrt (T.sqEdge 2) * dihedralClosedDerivSqPoly T 2 k =
513 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
514 schlaefliPolySummandNorm T.sqEdge 2 k := by
515 unfold dihedralClosedDerivSqPoly
516 have hp_nonneg := CofactorDerivatives.dihedralCofactorProductPoly_nonneg_of_nonDegenerate T 2
517 have hp_exp : 0 ≤
518 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
519 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge := by
520 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
521 DihedralCayleyMenger.oppositeCMVertices] using hp_nonneg
522 have hp_ne := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 2
523 have hp_exp_ne :
524 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
525 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge ≠ 0 := by
526 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
527 DihedralCayleyMenger.oppositeCMVertices] using hp_ne
528 have hp_left : CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge ≠ 0 :=
529 (mul_ne_zero_iff.mp hp_exp_ne).1
530 have hp_right : CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge ≠ 0 :=
531 (mul_ne_zero_iff.mp hp_exp_ne).2
532 have hd_ne := CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T 2
533 have hnum_nonneg : 0 ≤ 2 * cm3 T.sqEdge * T.sqEdge 2 := by
534 nlinarith [T.cm_pos, T.sqEdge_pos 2]
535 rw [CofactorDerivatives.sqrt_one_sub_dihedralCos3SqPoly_sq_eq
536 T.sqEdge 2 hp_nonneg hp_ne hd_ne hnum_nonneg]
537 have hsqrt : Real.sqrt (2 * cm3 T.sqEdge * T.sqEdge 2) =
538 Real.sqrt (2 * cm3 T.sqEdge) * Real.sqrt (T.sqEdge 2) := by
539 have hleft : 0 ≤ 2 * cm3 T.sqEdge := by nlinarith [T.cm_pos]
540 rw [show 2 * cm3 T.sqEdge * T.sqEdge 2 =
541 (2 * cm3 T.sqEdge) * T.sqEdge 2 by ring]
542 rw [Real.sqrt_mul hleft]
543 rw [hsqrt]
544 simp [CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
545 CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
546 CofactorDerivatives.dihedralDenom3Poly,
547 DihedralCayleyMenger.oppositeCMVertices,
548 schlaefliPolySummandNorm]
549 have hcm : Real.sqrt (2 * cm3 T.sqEdge) ≠ 0 :=
550 Real.sqrt_ne_zero'.mpr (by nlinarith [T.cm_pos] : 0 < 2 * cm3 T.sqEdge)
551 have he : Real.sqrt (T.sqEdge 2) ≠ 0 :=
552 Real.sqrt_ne_zero'.mpr (T.sqEdge_pos 2)
553 have hd :
554 Real.sqrt (CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
555 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge) ≠ 0 := by
556 simpa [CofactorDerivatives.dihedralDenom3Poly,
557 DihedralCayleyMenger.oppositeCMVertices] using hd_ne
558 field_simp [hcm, he, hd]
559 rw [Real.sq_sqrt hp_exp]
560 field_simp [hcm, hp_left, hp_right]
561 fin_cases k <;>
562 simp [CofactorPolynomial.cmCofactor3Poly,
563 CofactorPolynomial.cmCofactorPartial] <;>
564 ring_nf
565
566/-- Radical bridge for edge `3`. -/
567theorem schlaefli_summand_bridge_edge3
568 (T : NonDegenerateTet) (k : Fin 6) :
569 Real.sqrt (T.sqEdge 3) * dihedralClosedDerivSqPoly T 3 k =
570 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
571 schlaefliPolySummandNorm T.sqEdge 3 k := by
572 unfold dihedralClosedDerivSqPoly
573 have hp_nonneg := CofactorDerivatives.dihedralCofactorProductPoly_nonneg_of_nonDegenerate T 3
574 have hp_exp : 0 ≤
575 CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
576 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge := by
577 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
578 DihedralCayleyMenger.oppositeCMVertices] using hp_nonneg
579 have hp_ne := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 3
580 have hp_exp_ne :
581 CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
582 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 := by
583 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
584 DihedralCayleyMenger.oppositeCMVertices] using hp_ne
585 have hp_left : CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge ≠ 0 :=
586 (mul_ne_zero_iff.mp hp_exp_ne).1
587 have hp_right : CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 :=
588 (mul_ne_zero_iff.mp hp_exp_ne).2
589 have hd_ne := CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T 3
590 have hnum_nonneg : 0 ≤ 2 * cm3 T.sqEdge * T.sqEdge 3 := by
591 nlinarith [T.cm_pos, T.sqEdge_pos 3]
592 rw [CofactorDerivatives.sqrt_one_sub_dihedralCos3SqPoly_sq_eq
593 T.sqEdge 3 hp_nonneg hp_ne hd_ne hnum_nonneg]
594 have hsqrt : Real.sqrt (2 * cm3 T.sqEdge * T.sqEdge 3) =
595 Real.sqrt (2 * cm3 T.sqEdge) * Real.sqrt (T.sqEdge 3) := by
596 have hleft : 0 ≤ 2 * cm3 T.sqEdge := by nlinarith [T.cm_pos]
597 rw [show 2 * cm3 T.sqEdge * T.sqEdge 3 =
598 (2 * cm3 T.sqEdge) * T.sqEdge 3 by ring]
599 rw [Real.sqrt_mul hleft]
600 rw [hsqrt]
601 simp [CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
602 CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
603 CofactorDerivatives.dihedralDenom3Poly,
604 DihedralCayleyMenger.oppositeCMVertices,
605 schlaefliPolySummandNorm]
606 have hcm : Real.sqrt (2 * cm3 T.sqEdge) ≠ 0 :=
607 Real.sqrt_ne_zero'.mpr (by nlinarith [T.cm_pos] : 0 < 2 * cm3 T.sqEdge)
608 have he : Real.sqrt (T.sqEdge 3) ≠ 0 :=
609 Real.sqrt_ne_zero'.mpr (T.sqEdge_pos 3)
610 have hd :
611 Real.sqrt (CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
612 CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge) ≠ 0 := by
613 simpa [CofactorDerivatives.dihedralDenom3Poly,
614 DihedralCayleyMenger.oppositeCMVertices] using hd_ne
615 field_simp [hcm, he, hd]
616 rw [Real.sq_sqrt hp_exp]
617 field_simp [hcm, hp_left, hp_right]
618 fin_cases k <;>
619 simp [CofactorPolynomial.cmCofactor3Poly,
620 CofactorPolynomial.cmCofactorPartial] <;>
621 ring_nf
622
623/-- Radical bridge for edge `4`. -/
624theorem schlaefli_summand_bridge_edge4
625 (T : NonDegenerateTet) (k : Fin 6) :
626 Real.sqrt (T.sqEdge 4) * dihedralClosedDerivSqPoly T 4 k =
627 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
628 schlaefliPolySummandNorm T.sqEdge 4 k := by
629 unfold dihedralClosedDerivSqPoly
630 have hp_nonneg := CofactorDerivatives.dihedralCofactorProductPoly_nonneg_of_nonDegenerate T 4
631 have hp_exp : 0 ≤
632 CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
633 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge := by
634 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
635 DihedralCayleyMenger.oppositeCMVertices] using hp_nonneg
636 have hp_ne := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 4
637 have hp_exp_ne :
638 CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
639 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge ≠ 0 := by
640 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
641 DihedralCayleyMenger.oppositeCMVertices] using hp_ne
642 have hp_left : CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge ≠ 0 :=
643 (mul_ne_zero_iff.mp hp_exp_ne).1
644 have hp_right : CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge ≠ 0 :=
645 (mul_ne_zero_iff.mp hp_exp_ne).2
646 have hd_ne := CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T 4
647 have hnum_nonneg : 0 ≤ 2 * cm3 T.sqEdge * T.sqEdge 4 := by
648 nlinarith [T.cm_pos, T.sqEdge_pos 4]
649 rw [CofactorDerivatives.sqrt_one_sub_dihedralCos3SqPoly_sq_eq
650 T.sqEdge 4 hp_nonneg hp_ne hd_ne hnum_nonneg]
651 have hsqrt : Real.sqrt (2 * cm3 T.sqEdge * T.sqEdge 4) =
652 Real.sqrt (2 * cm3 T.sqEdge) * Real.sqrt (T.sqEdge 4) := by
653 have hleft : 0 ≤ 2 * cm3 T.sqEdge := by nlinarith [T.cm_pos]
654 rw [show 2 * cm3 T.sqEdge * T.sqEdge 4 =
655 (2 * cm3 T.sqEdge) * T.sqEdge 4 by ring]
656 rw [Real.sqrt_mul hleft]
657 rw [hsqrt]
658 simp [CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
659 CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
660 CofactorDerivatives.dihedralDenom3Poly,
661 DihedralCayleyMenger.oppositeCMVertices,
662 schlaefliPolySummandNorm]
663 have hcm : Real.sqrt (2 * cm3 T.sqEdge) ≠ 0 :=
664 Real.sqrt_ne_zero'.mpr (by nlinarith [T.cm_pos] : 0 < 2 * cm3 T.sqEdge)
665 have he : Real.sqrt (T.sqEdge 4) ≠ 0 :=
666 Real.sqrt_ne_zero'.mpr (T.sqEdge_pos 4)
667 have hd :
668 Real.sqrt (CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
669 CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge) ≠ 0 := by
670 simpa [CofactorDerivatives.dihedralDenom3Poly,
671 DihedralCayleyMenger.oppositeCMVertices] using hd_ne
672 field_simp [hcm, he, hd]
673 rw [Real.sq_sqrt hp_exp]
674 field_simp [hcm, hp_left, hp_right]
675 fin_cases k <;>
676 simp [CofactorPolynomial.cmCofactor3Poly,
677 CofactorPolynomial.cmCofactorPartial] <;>
678 ring_nf
679
680/-- Radical bridge for edge `5`. -/
681theorem schlaefli_summand_bridge_edge5
682 (T : NonDegenerateTet) (k : Fin 6) :
683 Real.sqrt (T.sqEdge 5) * dihedralClosedDerivSqPoly T 5 k =
684 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
685 schlaefliPolySummandNorm T.sqEdge 5 k := by
686 unfold dihedralClosedDerivSqPoly
687 have hp_nonneg := CofactorDerivatives.dihedralCofactorProductPoly_nonneg_of_nonDegenerate T 5
688 have hp_exp : 0 ≤
689 CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
690 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge := by
691 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
692 DihedralCayleyMenger.oppositeCMVertices] using hp_nonneg
693 have hp_ne := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 5
694 have hp_exp_ne :
695 CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
696 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge ≠ 0 := by
697 simpa [CofactorDerivatives.dihedralCofactorProductPoly,
698 DihedralCayleyMenger.oppositeCMVertices] using hp_ne
699 have hp_left : CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge ≠ 0 :=
700 (mul_ne_zero_iff.mp hp_exp_ne).1
701 have hp_right : CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge ≠ 0 :=
702 (mul_ne_zero_iff.mp hp_exp_ne).2
703 have hd_ne := CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T 5
704 have hnum_nonneg : 0 ≤ 2 * cm3 T.sqEdge * T.sqEdge 5 := by
705 nlinarith [T.cm_pos, T.sqEdge_pos 5]
706 rw [CofactorDerivatives.sqrt_one_sub_dihedralCos3SqPoly_sq_eq
707 T.sqEdge 5 hp_nonneg hp_ne hd_ne hnum_nonneg]
708 have hsqrt : Real.sqrt (2 * cm3 T.sqEdge * T.sqEdge 5) =
709 Real.sqrt (2 * cm3 T.sqEdge) * Real.sqrt (T.sqEdge 5) := by
710 have hleft : 0 ≤ 2 * cm3 T.sqEdge := by nlinarith [T.cm_pos]
711 rw [show 2 * cm3 T.sqEdge * T.sqEdge 5 =
712 (2 * cm3 T.sqEdge) * T.sqEdge 5 by ring]
713 rw [Real.sqrt_mul hleft]
714 rw [hsqrt]
715 simp [CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
716 CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
717 CofactorDerivatives.dihedralDenom3Poly,
718 DihedralCayleyMenger.oppositeCMVertices,
719 schlaefliPolySummandNorm]
720 have hcm : Real.sqrt (2 * cm3 T.sqEdge) ≠ 0 :=
721 Real.sqrt_ne_zero'.mpr (by nlinarith [T.cm_pos] : 0 < 2 * cm3 T.sqEdge)
722 have he : Real.sqrt (T.sqEdge 5) ≠ 0 :=
723 Real.sqrt_ne_zero'.mpr (T.sqEdge_pos 5)
724 have hd :
725 Real.sqrt (CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
726 CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge) ≠ 0 := by
727 simpa [CofactorDerivatives.dihedralDenom3Poly,
728 DihedralCayleyMenger.oppositeCMVertices] using hd_ne
729 field_simp [hcm, he, hd]
730 rw [Real.sq_sqrt hp_exp]
731 field_simp [hcm, hp_left, hp_right]
732 fin_cases k <;>
733 simp [CofactorPolynomial.cmCofactor3Poly,
734 CofactorPolynomial.cmCofactorPartial] <;>
735 ring_nf
736
737/-- The radical bridge from the original polynomial-cofactor summand to the
738rationalized summand. -/
739theorem schlaefliSummandBridge :
740 SchlaefliSummandBridgeTarget := by
741 intro T e k
742 fin_cases e
743 · exact schlaefli_summand_bridge_edge0 T k
744 · exact schlaefli_summand_bridge_edge1 T k
745 · exact schlaefli_summand_bridge_edge2 T k
746 · exact schlaefli_summand_bridge_edge3 T k
747 · exact schlaefli_summand_bridge_edge4 T k
748 · exact schlaefli_summand_bridge_edge5 T k
749
750/-- The corrected six-edge polynomial-cofactor Schläfli identity. -/
751theorem tetraSchlaefliSixEdgePolynomial :
752 TetraSchlaefliSixEdgePolynomialTarget := by
753 intro T k
754 calc
755 (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralClosedDerivSqPoly T e k)
756 = ∑ e : Fin 6,
757 (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
758 schlaefliPolySummandNorm T.sqEdge e k := by
759 refine Finset.sum_congr rfl ?_
760 intro e _
761 exact schlaefliSummandBridge T e k
762 _ = (1 / Real.sqrt (2 * cm3 T.sqEdge)) *
763 (∑ e : Fin 6, schlaefliPolySummandNorm T.sqEdge e k) := by
764 exact (Finset.mul_sum _ _ _).symm
765 _ = 0 := by
766 rw [schlaefliPolySummandNorm_sum_eq_zero T k]
767 ring
768
769/-- The polynomial-cofactor target implies the determinant-cofactor target. -/
770theorem sixEdgeClosedForm_of_polynomial
771 (hPoly : TetraSchlaefliSixEdgePolynomialTarget) :
772 TetraSchlaefliSixEdgeClosedFormTarget := by
773 intro T k
774 calc
775 (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralClosedDerivSq T e k)
776 = ∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralClosedDerivSqPoly T e k := by
777 refine Finset.sum_congr rfl ?_
778 intro e _
779 rw [dihedralClosedDerivSq_eq_poly]
780 _ = 0 := hPoly T k
781
782/-- The six explicit squared-edge identities imply the full corrected
783edge-length closed-form Schläfli theorem. -/
784theorem schlaefliClosedForm_of_sixEdgeSq
785 (hSix : TetraSchlaefliSixEdgeClosedFormTarget) :
786 SchlaefliTetrahedronClosedFormTarget := by
787 intro T
788 apply TetraSchlaefliClosedEquation_of_sq
789 intro k
790 exact hSix T k
791
792/-- The six explicit algebraic edge identities discharge the local
793tetrahedral Schläfli data package. -/
794theorem schlaefliTetrahedronTheorem_of_sixEdgeSq
795 (hSix : TetraSchlaefliSixEdgeClosedFormTarget) :
796 SchlaefliTetrahedronTheorem := by
797 intro T
798 exact ⟨tetraSchlaefliDerivativeData_of_equation T
799 (fun e k => dihedralClosedDerivLength T e k)
800 (fun k => volume3ClosedDerivLength T k)
801 ((schlaefliClosedForm_of_sixEdgeSq hSix) T)⟩
802
803/-- Once the closed-form equation is proved, it constructs the local
804Schläfli derivative package with no caller-supplied data. -/
805def tetraSchlaefliDerivativeData_closedForm
806 (T : NonDegenerateTet) (hT : TetraSchlaefliClosedEquation T) :
807 TetraSchlaefliDerivativeData T :=
808 tetraSchlaefliDerivativeData_of_equation T
809 (fun e k => dihedralClosedDerivLength T e k)
810 (fun k => volume3ClosedDerivLength T k)
811 hT
812
813/-- A closed-form Schläfli proof discharges the existing tetrahedral
814Schläfli theorem target. -/
815theorem schlaefliTetrahedronTheorem_of_closedForm
816 (h : SchlaefliTetrahedronClosedFormTarget) :
817 SchlaefliTetrahedronTheorem := by
818 intro T
819 exact ⟨tetraSchlaefliDerivativeData_closedForm T (h T)⟩
820
821/-- Determinant-cofactor six-edge Schläfli identity. -/
822theorem tetraSchlaefliSixEdgeClosedForm :
823 TetraSchlaefliSixEdgeClosedFormTarget :=
824 sixEdgeClosedForm_of_polynomial tetraSchlaefliSixEdgePolynomial
825
826/-- Closed-form tetrahedral Schläfli theorem. -/
827theorem schlaefliTetrahedronClosedForm :
828 SchlaefliTetrahedronClosedFormTarget :=
829 schlaefliClosedForm_of_sixEdgeSq tetraSchlaefliSixEdgeClosedForm
830
831/-- The local tetrahedral Schläfli derivative-data package is now constructed
832from the explicit cofactor formulas. -/
833theorem schlaefliTetrahedronTheorem :
834 SchlaefliTetrahedronTheorem :=
835 schlaefliTetrahedronTheorem_of_closedForm schlaefliTetrahedronClosedForm
836
837/-- Realized tetrahedra with strict face-normal independence inherit the
838same closed-form Schläfli package once the polynomial identity is proved. -/
839def RealizedNonDegenerateTet.schlaefliData_of_closedForm
840 (T : RealizedNonDegenerateTet)
841 (h : TetraSchlaefliClosedEquation T.tet) :
842 TetraSchlaefliDerivativeData T.tet :=
843 tetraSchlaefliDerivativeData_closedForm T.tet h
844
845end
846
847end SchlaefliTetrahedronProof
848end Geometry
849end IndisputableMonolith
850