IndisputableMonolith.Geometry.CofactorPolynomial
IndisputableMonolith/Geometry/CofactorPolynomial.lean · 1078 lines · 116 declarations
show as:
view math explainer →
1import Mathlib.Analysis.Calculus.Deriv.Basic
2import Mathlib.Analysis.Calculus.Deriv.Add
3import Mathlib.Analysis.Calculus.Deriv.Mul
4import Mathlib.Analysis.Calculus.Deriv.Pow
5import IndisputableMonolith.Geometry.CayleyMengerMatrix
6import IndisputableMonolith.Geometry.DihedralCayleyMenger
7
8/-!
9# Explicit Cayley-Menger Cofactor Polynomials
10
11This generated module expands every tetrahedral Cayley-Menger cofactor into
12an explicit polynomial in the six squared edge coordinates. It is the
13cofactor analogue of `CayleyMengerDerivatives`: downstream dihedral-angle
14calculus can refer to named polynomial partials instead of opaque `fderiv`
15terms.
16-/
17
18namespace IndisputableMonolith
19namespace Geometry
20namespace CofactorPolynomial
21
22open CayleyMengerPolynomial CayleyMengerMatrix
23
24noncomputable section
25
26/-- Explicit polynomial normal form for every Cayley-Menger cofactor. -/
27def cmCofactor3Poly (r c : Fin 5) (a : SqEdges) : ℝ :=
28 match r.val, c.val with
29 | 0, 0 => (a 2) ^ 2 * (a 3) ^ 2 - 2 * (a 1) * (a 2) * (a 3) * (a 4) + (a 1) ^ 2 * (a 4) ^ 2 - 2 * (a 0) * (a 2) * (a 3) * (a 5) - 2 * (a 0) * (a 1) * (a 4) * (a 5) + (a 0) ^ 2 * (a 5) ^ 2
30 | 0, 1 => -2 * (a 3) * (a 4) * (a 5) + (a 2) * (a 3) * (a 5) + (a 2) * (a 3) * (a 4) - (a 2) * (a 3) ^ 2 + (a 1) * (a 4) * (a 5) - (a 1) * (a 4) ^ 2 + (a 1) * (a 3) * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 4) * (a 5) + (a 0) * (a 3) * (a 5)
31 | 0, 2 => (a 2) * (a 3) * (a 5) - (a 2) ^ 2 * (a 3) + (a 1) * (a 4) * (a 5) - 2 * (a 1) * (a 2) * (a 5) + (a 1) * (a 2) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 2) * (a 5) + (a 0) * (a 1) * (a 5)
32 | 0, 3 => (a 2) * (a 3) * (a 4) - (a 2) ^ 2 * (a 3) - (a 1) * (a 4) ^ 2 + (a 1) * (a 2) * (a 4) + (a 0) * (a 4) * (a 5) + (a 0) * (a 2) * (a 5) - 2 * (a 0) * (a 2) * (a 4) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 4) - (a 0) ^ 2 * (a 5)
33 | 0, 4 => -(a 2) * (a 3) ^ 2 + (a 1) * (a 3) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) + (a 0) * (a 3) * (a 5) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 5) + (a 0) * (a 1) * (a 4) - 2 * (a 0) * (a 1) * (a 3) - (a 0) ^ 2 * (a 5)
34 | 1, 0 => -2 * (a 3) * (a 4) * (a 5) + (a 2) * (a 3) * (a 5) + (a 2) * (a 3) * (a 4) - (a 2) * (a 3) ^ 2 + (a 1) * (a 4) * (a 5) - (a 1) * (a 4) ^ 2 + (a 1) * (a 3) * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 4) * (a 5) + (a 0) * (a 3) * (a 5)
35 | 1, 1 => (a 5) ^ 2 - 2 * (a 4) * (a 5) + (a 4) ^ 2 - 2 * (a 3) * (a 5) - 2 * (a 3) * (a 4) + (a 3) ^ 2
36 | 1, 2 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5) + (a 2) * (a 5) - (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - (a 1) * (a 3) - 2 * (a 0) * (a 5)
37 | 1, 3 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4) - (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - (a 0) * (a 3)
38 | 1, 4 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2 - 2 * (a 2) * (a 3) - (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5) - (a 0) * (a 4) + (a 0) * (a 3)
39 | 2, 0 => (a 2) * (a 3) * (a 5) - (a 2) ^ 2 * (a 3) + (a 1) * (a 4) * (a 5) - 2 * (a 1) * (a 2) * (a 5) + (a 1) * (a 2) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 2) * (a 5) + (a 0) * (a 1) * (a 5)
40 | 2, 1 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5) + (a 2) * (a 5) - (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - (a 1) * (a 3) - 2 * (a 0) * (a 5)
41 | 2, 2 => (a 5) ^ 2 - 2 * (a 2) * (a 5) + (a 2) ^ 2 - 2 * (a 1) * (a 5) - 2 * (a 1) * (a 2) + (a 1) ^ 2
42 | 2, 3 => -(a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) - (a 2) ^ 2 + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - (a 0) * (a 1)
43 | 2, 4 => -(a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 1) * (a 2) - (a 1) ^ 2 + (a 0) * (a 5) - (a 0) * (a 2) + (a 0) * (a 1)
44 | 3, 0 => (a 2) * (a 3) * (a 4) - (a 2) ^ 2 * (a 3) - (a 1) * (a 4) ^ 2 + (a 1) * (a 2) * (a 4) + (a 0) * (a 4) * (a 5) + (a 0) * (a 2) * (a 5) - 2 * (a 0) * (a 2) * (a 4) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 4) - (a 0) ^ 2 * (a 5)
45 | 3, 1 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4) - (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - (a 0) * (a 3)
46 | 3, 2 => -(a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) - (a 2) ^ 2 + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - (a 0) * (a 1)
47 | 3, 3 => (a 4) ^ 2 - 2 * (a 2) * (a 4) + (a 2) ^ 2 - 2 * (a 0) * (a 4) - 2 * (a 0) * (a 2) + (a 0) ^ 2
48 | 3, 4 => -(a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3) + (a 0) * (a 2) + (a 0) * (a 1) - (a 0) ^ 2
49 | 4, 0 => -(a 2) * (a 3) ^ 2 + (a 1) * (a 3) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) + (a 0) * (a 3) * (a 5) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 5) + (a 0) * (a 1) * (a 4) - 2 * (a 0) * (a 1) * (a 3) - (a 0) ^ 2 * (a 5)
50 | 4, 1 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2 - 2 * (a 2) * (a 3) - (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5) - (a 0) * (a 4) + (a 0) * (a 3)
51 | 4, 2 => -(a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 1) * (a 2) - (a 1) ^ 2 + (a 0) * (a 5) - (a 0) * (a 2) + (a 0) * (a 1)
52 | 4, 3 => -(a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3) + (a 0) * (a 2) + (a 0) * (a 1) - (a 0) ^ 2
53 | 4, 4 => (a 3) ^ 2 - 2 * (a 1) * (a 3) + (a 1) ^ 2 - 2 * (a 0) * (a 3) - 2 * (a 0) * (a 1) + (a 0) ^ 2
54 | _, _ => 0
55
56/-- Explicit partial derivative of a cofactor polynomial with respect to one
57squared-edge coordinate. -/
58def cmCofactorPartial (r c : Fin 5) (k : Fin 6) (a : SqEdges) : ℝ :=
59 match r.val, c.val, k.val with
60 | 0, 0, 0 => -2 * (a 2) * (a 3) * (a 5) - 2 * (a 1) * (a 4) * (a 5) + 2 * (a 0) * (a 5) ^ 2
61 | 0, 0, 1 => -2 * (a 2) * (a 3) * (a 4) + 2 * (a 1) * (a 4) ^ 2 - 2 * (a 0) * (a 4) * (a 5)
62 | 0, 0, 2 => 2 * (a 2) * (a 3) ^ 2 - 2 * (a 1) * (a 3) * (a 4) - 2 * (a 0) * (a 3) * (a 5)
63 | 0, 0, 3 => 2 * (a 2) ^ 2 * (a 3) - 2 * (a 1) * (a 2) * (a 4) - 2 * (a 0) * (a 2) * (a 5)
64 | 0, 0, 4 => -2 * (a 1) * (a 2) * (a 3) + 2 * (a 1) ^ 2 * (a 4) - 2 * (a 0) * (a 1) * (a 5)
65 | 0, 0, 5 => -2 * (a 0) * (a 2) * (a 3) - 2 * (a 0) * (a 1) * (a 4) + 2 * (a 0) ^ 2 * (a 5)
66 | 0, 1, 0 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5)
67 | 0, 1, 1 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4)
68 | 0, 1, 2 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2
69 | 0, 1, 3 => -2 * (a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5)
70 | 0, 1, 4 => -2 * (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
71 | 0, 1, 5 => -2 * (a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3)
72 | 0, 2, 0 => -(a 5) ^ 2 + (a 2) * (a 5) + (a 1) * (a 5)
73 | 0, 2, 1 => (a 4) * (a 5) - 2 * (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5)
74 | 0, 2, 2 => (a 3) * (a 5) - 2 * (a 2) * (a 3) - 2 * (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
75 | 0, 2, 3 => (a 2) * (a 5) - (a 2) ^ 2 + (a 1) * (a 2)
76 | 0, 2, 4 => (a 1) * (a 5) + (a 1) * (a 2) - (a 1) ^ 2
77 | 0, 2, 5 => (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 2) + (a 0) * (a 1)
78 | 0, 3, 0 => (a 4) * (a 5) + (a 2) * (a 5) - 2 * (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5)
79 | 0, 3, 1 => -(a 4) ^ 2 + (a 2) * (a 4) + (a 0) * (a 4)
80 | 0, 3, 2 => (a 3) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5) - 2 * (a 0) * (a 4) + (a 0) * (a 3)
81 | 0, 3, 3 => (a 2) * (a 4) - (a 2) ^ 2 + (a 0) * (a 2)
82 | 0, 3, 4 => (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) - 2 * (a 0) * (a 2) + (a 0) * (a 1)
83 | 0, 3, 5 => (a 0) * (a 4) + (a 0) * (a 2) - (a 0) ^ 2
84 | 0, 4, 0 => (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - 2 * (a 1) * (a 3) - 2 * (a 0) * (a 5)
85 | 0, 4, 1 => (a 3) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - 2 * (a 0) * (a 3)
86 | 0, 4, 2 => -(a 3) ^ 2 + (a 1) * (a 3) + (a 0) * (a 3)
87 | 0, 4, 3 => -2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - 2 * (a 0) * (a 1)
88 | 0, 4, 4 => (a 1) * (a 3) - (a 1) ^ 2 + (a 0) * (a 1)
89 | 0, 4, 5 => (a 0) * (a 3) + (a 0) * (a 1) - (a 0) ^ 2
90 | 1, 0, 0 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5)
91 | 1, 0, 1 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4)
92 | 1, 0, 2 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2
93 | 1, 0, 3 => -2 * (a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5)
94 | 1, 0, 4 => -2 * (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
95 | 1, 0, 5 => -2 * (a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3)
96 | 1, 1, 3 => -2 * (a 5) - 2 * (a 4) + 2 * (a 3)
97 | 1, 1, 4 => -2 * (a 5) + 2 * (a 4) - 2 * (a 3)
98 | 1, 1, 5 => 2 * (a 5) - 2 * (a 4) - 2 * (a 3)
99 | 1, 2, 0 => -2 * (a 5)
100 | 1, 2, 1 => (a 5) + (a 4) - (a 3)
101 | 1, 2, 2 => (a 5) - (a 4) + (a 3)
102 | 1, 2, 3 => (a 5) + (a 2) - (a 1)
103 | 1, 2, 4 => (a 5) - (a 2) + (a 1)
104 | 1, 2, 5 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
105 | 1, 3, 0 => (a 5) + (a 4) - (a 3)
106 | 1, 3, 1 => -2 * (a 4)
107 | 1, 3, 2 => -(a 5) + (a 4) + (a 3)
108 | 1, 3, 3 => (a 4) + (a 2) - (a 0)
109 | 1, 3, 4 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
110 | 1, 3, 5 => (a 4) - (a 2) + (a 0)
111 | 1, 4, 0 => (a 5) - (a 4) + (a 3)
112 | 1, 4, 1 => -(a 5) + (a 4) + (a 3)
113 | 1, 4, 2 => -2 * (a 3)
114 | 1, 4, 3 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
115 | 1, 4, 4 => (a 3) + (a 1) - (a 0)
116 | 1, 4, 5 => (a 3) - (a 1) + (a 0)
117 | 2, 0, 0 => -(a 5) ^ 2 + (a 2) * (a 5) + (a 1) * (a 5)
118 | 2, 0, 1 => (a 4) * (a 5) - 2 * (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5)
119 | 2, 0, 2 => (a 3) * (a 5) - 2 * (a 2) * (a 3) - 2 * (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
120 | 2, 0, 3 => (a 2) * (a 5) - (a 2) ^ 2 + (a 1) * (a 2)
121 | 2, 0, 4 => (a 1) * (a 5) + (a 1) * (a 2) - (a 1) ^ 2
122 | 2, 0, 5 => (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 2) + (a 0) * (a 1)
123 | 2, 1, 0 => -2 * (a 5)
124 | 2, 1, 1 => (a 5) + (a 4) - (a 3)
125 | 2, 1, 2 => (a 5) - (a 4) + (a 3)
126 | 2, 1, 3 => (a 5) + (a 2) - (a 1)
127 | 2, 1, 4 => (a 5) - (a 2) + (a 1)
128 | 2, 1, 5 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
129 | 2, 2, 1 => -2 * (a 5) - 2 * (a 2) + 2 * (a 1)
130 | 2, 2, 2 => -2 * (a 5) + 2 * (a 2) - 2 * (a 1)
131 | 2, 2, 5 => 2 * (a 5) - 2 * (a 2) - 2 * (a 1)
132 | 2, 3, 0 => (a 5) + (a 2) - (a 1)
133 | 2, 3, 1 => (a 4) + (a 2) - (a 0)
134 | 2, 3, 2 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
135 | 2, 3, 3 => -2 * (a 2)
136 | 2, 3, 4 => -(a 5) + (a 2) + (a 1)
137 | 2, 3, 5 => -(a 4) + (a 2) + (a 0)
138 | 2, 4, 0 => (a 5) - (a 2) + (a 1)
139 | 2, 4, 1 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
140 | 2, 4, 2 => (a 3) + (a 1) - (a 0)
141 | 2, 4, 3 => -(a 5) + (a 2) + (a 1)
142 | 2, 4, 4 => -2 * (a 1)
143 | 2, 4, 5 => -(a 3) + (a 1) + (a 0)
144 | 3, 0, 0 => (a 4) * (a 5) + (a 2) * (a 5) - 2 * (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5)
145 | 3, 0, 1 => -(a 4) ^ 2 + (a 2) * (a 4) + (a 0) * (a 4)
146 | 3, 0, 2 => (a 3) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5) - 2 * (a 0) * (a 4) + (a 0) * (a 3)
147 | 3, 0, 3 => (a 2) * (a 4) - (a 2) ^ 2 + (a 0) * (a 2)
148 | 3, 0, 4 => (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) - 2 * (a 0) * (a 2) + (a 0) * (a 1)
149 | 3, 0, 5 => (a 0) * (a 4) + (a 0) * (a 2) - (a 0) ^ 2
150 | 3, 1, 0 => (a 5) + (a 4) - (a 3)
151 | 3, 1, 1 => -2 * (a 4)
152 | 3, 1, 2 => -(a 5) + (a 4) + (a 3)
153 | 3, 1, 3 => (a 4) + (a 2) - (a 0)
154 | 3, 1, 4 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
155 | 3, 1, 5 => (a 4) - (a 2) + (a 0)
156 | 3, 2, 0 => (a 5) + (a 2) - (a 1)
157 | 3, 2, 1 => (a 4) + (a 2) - (a 0)
158 | 3, 2, 2 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
159 | 3, 2, 3 => -2 * (a 2)
160 | 3, 2, 4 => -(a 5) + (a 2) + (a 1)
161 | 3, 2, 5 => -(a 4) + (a 2) + (a 0)
162 | 3, 3, 0 => -2 * (a 4) - 2 * (a 2) + 2 * (a 0)
163 | 3, 3, 2 => -2 * (a 4) + 2 * (a 2) - 2 * (a 0)
164 | 3, 3, 4 => 2 * (a 4) - 2 * (a 2) - 2 * (a 0)
165 | 3, 4, 0 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
166 | 3, 4, 1 => (a 4) - (a 2) + (a 0)
167 | 3, 4, 2 => (a 3) - (a 1) + (a 0)
168 | 3, 4, 3 => -(a 4) + (a 2) + (a 0)
169 | 3, 4, 4 => -(a 3) + (a 1) + (a 0)
170 | 3, 4, 5 => -2 * (a 0)
171 | 4, 0, 0 => (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - 2 * (a 1) * (a 3) - 2 * (a 0) * (a 5)
172 | 4, 0, 1 => (a 3) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - 2 * (a 0) * (a 3)
173 | 4, 0, 2 => -(a 3) ^ 2 + (a 1) * (a 3) + (a 0) * (a 3)
174 | 4, 0, 3 => -2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - 2 * (a 0) * (a 1)
175 | 4, 0, 4 => (a 1) * (a 3) - (a 1) ^ 2 + (a 0) * (a 1)
176 | 4, 0, 5 => (a 0) * (a 3) + (a 0) * (a 1) - (a 0) ^ 2
177 | 4, 1, 0 => (a 5) - (a 4) + (a 3)
178 | 4, 1, 1 => -(a 5) + (a 4) + (a 3)
179 | 4, 1, 2 => -2 * (a 3)
180 | 4, 1, 3 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
181 | 4, 1, 4 => (a 3) + (a 1) - (a 0)
182 | 4, 1, 5 => (a 3) - (a 1) + (a 0)
183 | 4, 2, 0 => (a 5) - (a 2) + (a 1)
184 | 4, 2, 1 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
185 | 4, 2, 2 => (a 3) + (a 1) - (a 0)
186 | 4, 2, 3 => -(a 5) + (a 2) + (a 1)
187 | 4, 2, 4 => -2 * (a 1)
188 | 4, 2, 5 => -(a 3) + (a 1) + (a 0)
189 | 4, 3, 0 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
190 | 4, 3, 1 => (a 4) - (a 2) + (a 0)
191 | 4, 3, 2 => (a 3) - (a 1) + (a 0)
192 | 4, 3, 3 => -(a 4) + (a 2) + (a 0)
193 | 4, 3, 4 => -(a 3) + (a 1) + (a 0)
194 | 4, 3, 5 => -2 * (a 0)
195 | 4, 4, 0 => -2 * (a 3) - 2 * (a 1) + 2 * (a 0)
196 | 4, 4, 1 => -2 * (a 3) + 2 * (a 1) - 2 * (a 0)
197 | 4, 4, 3 => 2 * (a 3) - 2 * (a 1) - 2 * (a 0)
198 | _, _, _ => 0
199
200/-- Audit target: the explicit polynomial normal form should agree with the
201determinant cofactor. The formulas above are intentionally separated from
202the determinant proof because normalizing all `Fin.succAbove` minor cases in
203one theorem is too slow for interactive builds. -/
204def CofactorPolynomialAgreement : Prop :=
205 ∀ a : SqEdges, ∀ r c : Fin 5, cmCofactor3 a r c = cmCofactor3Poly r c a
206
207set_option maxHeartbeats 2000000
208/-- Normal form for the minor used by cofactor `(3,4)`, deleting row `3`
209and column `4` from the Cayley-Menger matrix. -/
210def cmMinor34Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
211 !![(0 : ℝ), 1, 1, 1;
212 1, 0, a 0, a 1;
213 1, a 0, 0, a 3;
214 1, a 2, a 4, a 5]
215
216/-- The raw `Fin.succAbove` submatrix for cofactor `(3,4)` has the explicit
217normal form `cmMinor34Matrix`. -/
218theorem cmMinor34_submatrix_eq (a : SqEdges) :
219 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (3 : Fin 5)) (Fin.succAbove (4 : Fin 5)) =
220 cmMinor34Matrix a := by
221 ext i j
222 fin_cases i <;> fin_cases j <;> rfl
223
224/-- Determinant of the explicit `(3,4)` minor normal form. -/
225theorem det_cmMinor34Matrix (a : SqEdges) :
226 Matrix.det (cmMinor34Matrix a) = - cmCofactor3Poly 3 4 a := by
227 unfold cmMinor34Matrix cmCofactor3Poly
228 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
229 ring_nf
230
231/-- Cofactor polynomial agreement for the numerator of edge `0`. -/
232theorem cmCofactor3_34_eq_poly (a : SqEdges) :
233 cmCofactor3 a 3 4 = cmCofactor3Poly 3 4 a := by
234 unfold cmCofactor3 cmMinor3
235 rw [cmMinor34_submatrix_eq]
236 rw [det_cmMinor34Matrix]
237 simp [cmCofactorSign3, show ¬ Even (7 : Nat) by decide]
238
239/-- Normal form for the minor used by cofactor `(2,4)`. -/
240def cmMinor24Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
241 !![(0 : ℝ), 1, 1, 1;
242 1, 0, a 0, a 1;
243 1, a 1, a 3, 0;
244 1, a 2, a 4, a 5]
245
246theorem cmMinor24_submatrix_eq (a : SqEdges) :
247 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (2 : Fin 5)) (Fin.succAbove (4 : Fin 5)) =
248 cmMinor24Matrix a := by
249 ext i j
250 fin_cases i <;> fin_cases j <;> rfl
251
252theorem det_cmMinor24Matrix (a : SqEdges) :
253 Matrix.det (cmMinor24Matrix a) = cmCofactor3Poly 2 4 a := by
254 unfold cmMinor24Matrix cmCofactor3Poly
255 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
256 ring_nf
257
258theorem cmCofactor3_24_eq_poly (a : SqEdges) :
259 cmCofactor3 a 2 4 = cmCofactor3Poly 2 4 a := by
260 unfold cmCofactor3 cmMinor3
261 rw [cmMinor24_submatrix_eq, det_cmMinor24Matrix]
262 simp [cmCofactorSign3, show Even (6 : Nat) by decide]
263
264/-- Normal form for the minor used by cofactor `(2,3)`. -/
265def cmMinor23Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
266 !![(0 : ℝ), 1, 1, 1;
267 1, 0, a 0, a 2;
268 1, a 1, a 3, a 5;
269 1, a 2, a 4, 0]
270
271theorem cmMinor23_submatrix_eq (a : SqEdges) :
272 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (2 : Fin 5)) (Fin.succAbove (3 : Fin 5)) =
273 cmMinor23Matrix a := by
274 ext i j
275 fin_cases i <;> fin_cases j <;> rfl
276
277theorem det_cmMinor23Matrix (a : SqEdges) :
278 Matrix.det (cmMinor23Matrix a) = - cmCofactor3Poly 2 3 a := by
279 unfold cmMinor23Matrix cmCofactor3Poly
280 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
281 ring_nf
282
283theorem cmCofactor3_23_eq_poly (a : SqEdges) :
284 cmCofactor3 a 2 3 = cmCofactor3Poly 2 3 a := by
285 unfold cmCofactor3 cmMinor3
286 rw [cmMinor23_submatrix_eq, det_cmMinor23Matrix]
287 simp [cmCofactorSign3, show ¬ Even (5 : Nat) by decide]
288
289/-- Normal form for the minor used by cofactor `(1,4)`. -/
290def cmMinor14Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
291 !![(0 : ℝ), 1, 1, 1;
292 1, a 0, 0, a 3;
293 1, a 1, a 3, 0;
294 1, a 2, a 4, a 5]
295
296theorem cmMinor14_submatrix_eq (a : SqEdges) :
297 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (1 : Fin 5)) (Fin.succAbove (4 : Fin 5)) =
298 cmMinor14Matrix a := by
299 ext i j
300 fin_cases i <;> fin_cases j <;> rfl
301
302theorem det_cmMinor14Matrix (a : SqEdges) :
303 Matrix.det (cmMinor14Matrix a) = - cmCofactor3Poly 1 4 a := by
304 unfold cmMinor14Matrix cmCofactor3Poly
305 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
306 ring_nf
307
308theorem cmCofactor3_14_eq_poly (a : SqEdges) :
309 cmCofactor3 a 1 4 = cmCofactor3Poly 1 4 a := by
310 unfold cmCofactor3 cmMinor3
311 rw [cmMinor14_submatrix_eq, det_cmMinor14Matrix]
312 simp [cmCofactorSign3, show ¬ Even (5 : Nat) by decide]
313
314/-- Normal form for the minor used by cofactor `(1,3)`. -/
315def cmMinor13Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
316 !![(0 : ℝ), 1, 1, 1;
317 1, a 0, 0, a 4;
318 1, a 1, a 3, a 5;
319 1, a 2, a 4, 0]
320
321theorem cmMinor13_submatrix_eq (a : SqEdges) :
322 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (1 : Fin 5)) (Fin.succAbove (3 : Fin 5)) =
323 cmMinor13Matrix a := by
324 ext i j
325 fin_cases i <;> fin_cases j <;> rfl
326
327theorem det_cmMinor13Matrix (a : SqEdges) :
328 Matrix.det (cmMinor13Matrix a) = cmCofactor3Poly 1 3 a := by
329 unfold cmMinor13Matrix cmCofactor3Poly
330 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
331 ring_nf
332
333theorem cmCofactor3_13_eq_poly (a : SqEdges) :
334 cmCofactor3 a 1 3 = cmCofactor3Poly 1 3 a := by
335 unfold cmCofactor3 cmMinor3
336 rw [cmMinor13_submatrix_eq, det_cmMinor13Matrix]
337 simp [cmCofactorSign3, show Even (4 : Nat) by decide]
338
339/-- Normal form for the minor used by cofactor `(1,2)`. -/
340def cmMinor12Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
341 !![(0 : ℝ), 1, 1, 1;
342 1, a 0, a 3, a 4;
343 1, a 1, 0, a 5;
344 1, a 2, a 5, 0]
345
346theorem cmMinor12_submatrix_eq (a : SqEdges) :
347 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (1 : Fin 5)) (Fin.succAbove (2 : Fin 5)) =
348 cmMinor12Matrix a := by
349 ext i j
350 fin_cases i <;> fin_cases j <;> rfl
351
352theorem det_cmMinor12Matrix (a : SqEdges) :
353 Matrix.det (cmMinor12Matrix a) = - cmCofactor3Poly 1 2 a := by
354 unfold cmMinor12Matrix cmCofactor3Poly
355 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
356 ring_nf
357
358theorem cmCofactor3_12_eq_poly (a : SqEdges) :
359 cmCofactor3 a 1 2 = cmCofactor3Poly 1 2 a := by
360 unfold cmCofactor3 cmMinor3
361 rw [cmMinor12_submatrix_eq, det_cmMinor12Matrix]
362 simp [cmCofactorSign3, show ¬ Even (3 : Nat) by decide]
363
364/-- Normal form for the diagonal minor used by cofactor `(1,1)`. -/
365def cmMinor11Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
366 !![(0 : ℝ), 1, 1, 1;
367 1, 0, a 3, a 4;
368 1, a 3, 0, a 5;
369 1, a 4, a 5, 0]
370
371theorem cmMinor11_submatrix_eq (a : SqEdges) :
372 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (1 : Fin 5)) (Fin.succAbove (1 : Fin 5)) =
373 cmMinor11Matrix a := by
374 ext i j
375 fin_cases i <;> fin_cases j <;> rfl
376
377theorem det_cmMinor11Matrix (a : SqEdges) :
378 Matrix.det (cmMinor11Matrix a) = cmCofactor3Poly 1 1 a := by
379 unfold cmMinor11Matrix cmCofactor3Poly
380 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
381 ring_nf
382
383theorem cmCofactor3_11_eq_poly (a : SqEdges) :
384 cmCofactor3 a 1 1 = cmCofactor3Poly 1 1 a := by
385 unfold cmCofactor3 cmMinor3
386 rw [cmMinor11_submatrix_eq, det_cmMinor11Matrix]
387 simp [cmCofactorSign3, show Even (2 : Nat) by decide]
388
389/-- Normal form for the diagonal minor used by cofactor `(2,2)`. -/
390def cmMinor22Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
391 !![(0 : ℝ), 1, 1, 1;
392 1, 0, a 1, a 2;
393 1, a 1, 0, a 5;
394 1, a 2, a 5, 0]
395
396theorem cmMinor22_submatrix_eq (a : SqEdges) :
397 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (2 : Fin 5)) (Fin.succAbove (2 : Fin 5)) =
398 cmMinor22Matrix a := by
399 ext i j
400 fin_cases i <;> fin_cases j <;> rfl
401
402theorem det_cmMinor22Matrix (a : SqEdges) :
403 Matrix.det (cmMinor22Matrix a) = cmCofactor3Poly 2 2 a := by
404 unfold cmMinor22Matrix cmCofactor3Poly
405 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
406 ring_nf
407
408theorem cmCofactor3_22_eq_poly (a : SqEdges) :
409 cmCofactor3 a 2 2 = cmCofactor3Poly 2 2 a := by
410 unfold cmCofactor3 cmMinor3
411 rw [cmMinor22_submatrix_eq, det_cmMinor22Matrix]
412 simp [cmCofactorSign3, show Even (4 : Nat) by decide]
413
414/-- Normal form for the diagonal minor used by cofactor `(3,3)`. -/
415def cmMinor33Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
416 !![(0 : ℝ), 1, 1, 1;
417 1, 0, a 0, a 2;
418 1, a 0, 0, a 4;
419 1, a 2, a 4, 0]
420
421theorem cmMinor33_submatrix_eq (a : SqEdges) :
422 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (3 : Fin 5)) (Fin.succAbove (3 : Fin 5)) =
423 cmMinor33Matrix a := by
424 ext i j
425 fin_cases i <;> fin_cases j <;> rfl
426
427theorem det_cmMinor33Matrix (a : SqEdges) :
428 Matrix.det (cmMinor33Matrix a) = cmCofactor3Poly 3 3 a := by
429 unfold cmMinor33Matrix cmCofactor3Poly
430 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
431 ring_nf
432
433theorem cmCofactor3_33_eq_poly (a : SqEdges) :
434 cmCofactor3 a 3 3 = cmCofactor3Poly 3 3 a := by
435 unfold cmCofactor3 cmMinor3
436 rw [cmMinor33_submatrix_eq, det_cmMinor33Matrix]
437 simp [cmCofactorSign3, show Even (6 : Nat) by decide]
438
439/-- Normal form for the diagonal minor used by cofactor `(4,4)`. -/
440def cmMinor44Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
441 !![(0 : ℝ), 1, 1, 1;
442 1, 0, a 0, a 1;
443 1, a 0, 0, a 3;
444 1, a 1, a 3, 0]
445
446theorem cmMinor44_submatrix_eq (a : SqEdges) :
447 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (4 : Fin 5)) (Fin.succAbove (4 : Fin 5)) =
448 cmMinor44Matrix a := by
449 ext i j
450 fin_cases i <;> fin_cases j <;> rfl
451
452theorem det_cmMinor44Matrix (a : SqEdges) :
453 Matrix.det (cmMinor44Matrix a) = cmCofactor3Poly 4 4 a := by
454 unfold cmMinor44Matrix cmCofactor3Poly
455 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
456 ring_nf
457
458theorem cmCofactor3_44_eq_poly (a : SqEdges) :
459 cmCofactor3 a 4 4 = cmCofactor3Poly 4 4 a := by
460 unfold cmCofactor3 cmMinor3
461 rw [cmMinor44_submatrix_eq, det_cmMinor44Matrix]
462 simp [cmCofactorSign3, show Even (8 : Nat) by decide]
463
464/-- Polynomial agreement for every numerator cofactor used by tetrahedral
465dihedral cosines. -/
466theorem cmCofactor3_opposite_eq_poly (a : SqEdges) (e : Fin 6) :
467 let p := DihedralCayleyMenger.oppositeCMVertices e
468 cmCofactor3 a p.1 p.2 = cmCofactor3Poly p.1 p.2 a := by
469 fin_cases e
470 · exact cmCofactor3_34_eq_poly a
471 · exact cmCofactor3_24_eq_poly a
472 · exact cmCofactor3_23_eq_poly a
473 · exact cmCofactor3_14_eq_poly a
474 · exact cmCofactor3_13_eq_poly a
475 · exact cmCofactor3_12_eq_poly a
476
477/-- Polynomial agreement for every diagonal cofactor used by tetrahedral
478dihedral cosine denominators. -/
479theorem cmCofactor3_opposite_diag_eq_poly
480 (a : SqEdges) (e : Fin 6) (side : Bool) :
481 let p := DihedralCayleyMenger.oppositeCMVertices e
482 let r := if side then p.1 else p.2
483 cmCofactor3 a r r = cmCofactor3Poly r r a := by
484 fin_cases e <;> cases side
485 · exact cmCofactor3_44_eq_poly a
486 · exact cmCofactor3_33_eq_poly a
487 · exact cmCofactor3_44_eq_poly a
488 · exact cmCofactor3_22_eq_poly a
489 · exact cmCofactor3_33_eq_poly a
490 · exact cmCofactor3_22_eq_poly a
491 · exact cmCofactor3_44_eq_poly a
492 · exact cmCofactor3_11_eq_poly a
493 · exact cmCofactor3_33_eq_poly a
494 · exact cmCofactor3_11_eq_poly a
495 · exact cmCofactor3_22_eq_poly a
496 · exact cmCofactor3_11_eq_poly a
497
498def cmMinor00Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
499 !![0, a 0, a 1, a 2;
500 a 0, 0, a 3, a 4;
501 a 1, a 3, 0, a 5;
502 a 2, a 4, a 5, 0]
503
504theorem cmMinor00_submatrix_eq (a : SqEdges) :
505 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (0 : Fin 5)) (Fin.succAbove (0 : Fin 5)) =
506 cmMinor00Matrix a := by
507 ext i j
508 fin_cases i <;> fin_cases j <;> rfl
509
510theorem det_cmMinor00Matrix (a : SqEdges) :
511 Matrix.det (cmMinor00Matrix a) = cmCofactor3Poly 0 0 a := by
512 unfold cmMinor00Matrix cmCofactor3Poly
513 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
514 ring_nf
515
516theorem cmCofactor3_00_eq_poly (a : SqEdges) :
517 cmCofactor3 a 0 0 = cmCofactor3Poly 0 0 a := by
518 unfold cmCofactor3 cmMinor3
519 rw [cmMinor00_submatrix_eq, det_cmMinor00Matrix]
520 simp [cmCofactorSign3, show Even (0 : Nat) by decide]
521
522def cmMinor01Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
523 !![1, a 0, a 1, a 2;
524 1, 0, a 3, a 4;
525 1, a 3, 0, a 5;
526 1, a 4, a 5, 0]
527
528theorem cmMinor01_submatrix_eq (a : SqEdges) :
529 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (0 : Fin 5)) (Fin.succAbove (1 : Fin 5)) =
530 cmMinor01Matrix a := by
531 ext i j
532 fin_cases i <;> fin_cases j <;> rfl
533
534theorem det_cmMinor01Matrix (a : SqEdges) :
535 Matrix.det (cmMinor01Matrix a) = - cmCofactor3Poly 0 1 a := by
536 unfold cmMinor01Matrix cmCofactor3Poly
537 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
538 ring_nf
539
540theorem cmCofactor3_01_eq_poly (a : SqEdges) :
541 cmCofactor3 a 0 1 = cmCofactor3Poly 0 1 a := by
542 unfold cmCofactor3 cmMinor3
543 rw [cmMinor01_submatrix_eq, det_cmMinor01Matrix]
544 simp [cmCofactorSign3, show ¬ Even (1 : Nat) by decide]
545
546def cmMinor02Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
547 !![1, 0, a 1, a 2;
548 1, a 0, a 3, a 4;
549 1, a 1, 0, a 5;
550 1, a 2, a 5, 0]
551
552theorem cmMinor02_submatrix_eq (a : SqEdges) :
553 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (0 : Fin 5)) (Fin.succAbove (2 : Fin 5)) =
554 cmMinor02Matrix a := by
555 ext i j
556 fin_cases i <;> fin_cases j <;> rfl
557
558theorem det_cmMinor02Matrix (a : SqEdges) :
559 Matrix.det (cmMinor02Matrix a) = cmCofactor3Poly 0 2 a := by
560 unfold cmMinor02Matrix cmCofactor3Poly
561 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
562 ring_nf
563
564theorem cmCofactor3_02_eq_poly (a : SqEdges) :
565 cmCofactor3 a 0 2 = cmCofactor3Poly 0 2 a := by
566 unfold cmCofactor3 cmMinor3
567 rw [cmMinor02_submatrix_eq, det_cmMinor02Matrix]
568 simp [cmCofactorSign3, show Even (2 : Nat) by decide]
569
570def cmMinor03Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
571 !![1, 0, a 0, a 2;
572 1, a 0, 0, a 4;
573 1, a 1, a 3, a 5;
574 1, a 2, a 4, 0]
575
576theorem cmMinor03_submatrix_eq (a : SqEdges) :
577 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (0 : Fin 5)) (Fin.succAbove (3 : Fin 5)) =
578 cmMinor03Matrix a := by
579 ext i j
580 fin_cases i <;> fin_cases j <;> rfl
581
582theorem det_cmMinor03Matrix (a : SqEdges) :
583 Matrix.det (cmMinor03Matrix a) = - cmCofactor3Poly 0 3 a := by
584 unfold cmMinor03Matrix cmCofactor3Poly
585 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
586 ring_nf
587
588theorem cmCofactor3_03_eq_poly (a : SqEdges) :
589 cmCofactor3 a 0 3 = cmCofactor3Poly 0 3 a := by
590 unfold cmCofactor3 cmMinor3
591 rw [cmMinor03_submatrix_eq, det_cmMinor03Matrix]
592 simp [cmCofactorSign3, show ¬ Even (3 : Nat) by decide]
593
594def cmMinor04Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
595 !![1, 0, a 0, a 1;
596 1, a 0, 0, a 3;
597 1, a 1, a 3, 0;
598 1, a 2, a 4, a 5]
599
600theorem cmMinor04_submatrix_eq (a : SqEdges) :
601 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (0 : Fin 5)) (Fin.succAbove (4 : Fin 5)) =
602 cmMinor04Matrix a := by
603 ext i j
604 fin_cases i <;> fin_cases j <;> rfl
605
606theorem det_cmMinor04Matrix (a : SqEdges) :
607 Matrix.det (cmMinor04Matrix a) = cmCofactor3Poly 0 4 a := by
608 unfold cmMinor04Matrix cmCofactor3Poly
609 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
610 ring_nf
611
612theorem cmCofactor3_04_eq_poly (a : SqEdges) :
613 cmCofactor3 a 0 4 = cmCofactor3Poly 0 4 a := by
614 unfold cmCofactor3 cmMinor3
615 rw [cmMinor04_submatrix_eq, det_cmMinor04Matrix]
616 simp [cmCofactorSign3, show Even (4 : Nat) by decide]
617
618def cmMinor10Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
619 !![1, 1, 1, 1;
620 a 0, 0, a 3, a 4;
621 a 1, a 3, 0, a 5;
622 a 2, a 4, a 5, 0]
623
624theorem cmMinor10_submatrix_eq (a : SqEdges) :
625 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (1 : Fin 5)) (Fin.succAbove (0 : Fin 5)) =
626 cmMinor10Matrix a := by
627 ext i j
628 fin_cases i <;> fin_cases j <;> rfl
629
630theorem det_cmMinor10Matrix (a : SqEdges) :
631 Matrix.det (cmMinor10Matrix a) = - cmCofactor3Poly 1 0 a := by
632 unfold cmMinor10Matrix cmCofactor3Poly
633 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
634 ring_nf
635
636theorem cmCofactor3_10_eq_poly (a : SqEdges) :
637 cmCofactor3 a 1 0 = cmCofactor3Poly 1 0 a := by
638 unfold cmCofactor3 cmMinor3
639 rw [cmMinor10_submatrix_eq, det_cmMinor10Matrix]
640 simp [cmCofactorSign3, show ¬ Even (1 : Nat) by decide]
641
642def cmMinor20Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
643 !![1, 1, 1, 1;
644 0, a 0, a 1, a 2;
645 a 1, a 3, 0, a 5;
646 a 2, a 4, a 5, 0]
647
648theorem cmMinor20_submatrix_eq (a : SqEdges) :
649 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (2 : Fin 5)) (Fin.succAbove (0 : Fin 5)) =
650 cmMinor20Matrix a := by
651 ext i j
652 fin_cases i <;> fin_cases j <;> rfl
653
654theorem det_cmMinor20Matrix (a : SqEdges) :
655 Matrix.det (cmMinor20Matrix a) = cmCofactor3Poly 2 0 a := by
656 unfold cmMinor20Matrix cmCofactor3Poly
657 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
658 ring_nf
659
660theorem cmCofactor3_20_eq_poly (a : SqEdges) :
661 cmCofactor3 a 2 0 = cmCofactor3Poly 2 0 a := by
662 unfold cmCofactor3 cmMinor3
663 rw [cmMinor20_submatrix_eq, det_cmMinor20Matrix]
664 simp [cmCofactorSign3, show Even (2 : Nat) by decide]
665
666def cmMinor21Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
667 !![(0 : ℝ), 1, 1, 1;
668 1, a 0, a 1, a 2;
669 1, a 3, 0, a 5;
670 1, a 4, a 5, 0]
671
672theorem cmMinor21_submatrix_eq (a : SqEdges) :
673 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (2 : Fin 5)) (Fin.succAbove (1 : Fin 5)) =
674 cmMinor21Matrix a := by
675 ext i j
676 fin_cases i <;> fin_cases j <;> rfl
677
678theorem det_cmMinor21Matrix (a : SqEdges) :
679 Matrix.det (cmMinor21Matrix a) = - cmCofactor3Poly 2 1 a := by
680 unfold cmMinor21Matrix cmCofactor3Poly
681 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
682 ring_nf
683
684theorem cmCofactor3_21_eq_poly (a : SqEdges) :
685 cmCofactor3 a 2 1 = cmCofactor3Poly 2 1 a := by
686 unfold cmCofactor3 cmMinor3
687 rw [cmMinor21_submatrix_eq, det_cmMinor21Matrix]
688 simp [cmCofactorSign3, show ¬ Even (3 : Nat) by decide]
689
690def cmMinor30Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
691 !![1, 1, 1, 1;
692 0, a 0, a 1, a 2;
693 a 0, 0, a 3, a 4;
694 a 2, a 4, a 5, 0]
695
696theorem cmMinor30_submatrix_eq (a : SqEdges) :
697 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (3 : Fin 5)) (Fin.succAbove (0 : Fin 5)) =
698 cmMinor30Matrix a := by
699 ext i j
700 fin_cases i <;> fin_cases j <;> rfl
701
702theorem det_cmMinor30Matrix (a : SqEdges) :
703 Matrix.det (cmMinor30Matrix a) = - cmCofactor3Poly 3 0 a := by
704 unfold cmMinor30Matrix cmCofactor3Poly
705 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
706 ring_nf
707
708theorem cmCofactor3_30_eq_poly (a : SqEdges) :
709 cmCofactor3 a 3 0 = cmCofactor3Poly 3 0 a := by
710 unfold cmCofactor3 cmMinor3
711 rw [cmMinor30_submatrix_eq, det_cmMinor30Matrix]
712 simp [cmCofactorSign3, show ¬ Even (3 : Nat) by decide]
713
714def cmMinor31Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
715 !![(0 : ℝ), 1, 1, 1;
716 1, a 0, a 1, a 2;
717 1, 0, a 3, a 4;
718 1, a 4, a 5, 0]
719
720theorem cmMinor31_submatrix_eq (a : SqEdges) :
721 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (3 : Fin 5)) (Fin.succAbove (1 : Fin 5)) =
722 cmMinor31Matrix a := by
723 ext i j
724 fin_cases i <;> fin_cases j <;> rfl
725
726theorem det_cmMinor31Matrix (a : SqEdges) :
727 Matrix.det (cmMinor31Matrix a) = cmCofactor3Poly 3 1 a := by
728 unfold cmMinor31Matrix cmCofactor3Poly
729 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
730 ring_nf
731
732theorem cmCofactor3_31_eq_poly (a : SqEdges) :
733 cmCofactor3 a 3 1 = cmCofactor3Poly 3 1 a := by
734 unfold cmCofactor3 cmMinor3
735 rw [cmMinor31_submatrix_eq, det_cmMinor31Matrix]
736 simp [cmCofactorSign3, show Even (4 : Nat) by decide]
737
738def cmMinor32Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
739 !![(0 : ℝ), 1, 1, 1;
740 1, 0, a 1, a 2;
741 1, a 0, a 3, a 4;
742 1, a 2, a 5, 0]
743
744theorem cmMinor32_submatrix_eq (a : SqEdges) :
745 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (3 : Fin 5)) (Fin.succAbove (2 : Fin 5)) =
746 cmMinor32Matrix a := by
747 ext i j
748 fin_cases i <;> fin_cases j <;> rfl
749
750theorem det_cmMinor32Matrix (a : SqEdges) :
751 Matrix.det (cmMinor32Matrix a) = - cmCofactor3Poly 3 2 a := by
752 unfold cmMinor32Matrix cmCofactor3Poly
753 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
754 ring_nf
755
756theorem cmCofactor3_32_eq_poly (a : SqEdges) :
757 cmCofactor3 a 3 2 = cmCofactor3Poly 3 2 a := by
758 unfold cmCofactor3 cmMinor3
759 rw [cmMinor32_submatrix_eq, det_cmMinor32Matrix]
760 simp [cmCofactorSign3, show ¬ Even (5 : Nat) by decide]
761
762def cmMinor40Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
763 !![1, 1, 1, 1;
764 0, a 0, a 1, a 2;
765 a 0, 0, a 3, a 4;
766 a 1, a 3, 0, a 5]
767
768theorem cmMinor40_submatrix_eq (a : SqEdges) :
769 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (4 : Fin 5)) (Fin.succAbove (0 : Fin 5)) =
770 cmMinor40Matrix a := by
771 ext i j
772 fin_cases i <;> fin_cases j <;> rfl
773
774theorem det_cmMinor40Matrix (a : SqEdges) :
775 Matrix.det (cmMinor40Matrix a) = cmCofactor3Poly 4 0 a := by
776 unfold cmMinor40Matrix cmCofactor3Poly
777 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
778 ring_nf
779
780theorem cmCofactor3_40_eq_poly (a : SqEdges) :
781 cmCofactor3 a 4 0 = cmCofactor3Poly 4 0 a := by
782 unfold cmCofactor3 cmMinor3
783 rw [cmMinor40_submatrix_eq, det_cmMinor40Matrix]
784 simp [cmCofactorSign3, show Even (4 : Nat) by decide]
785
786def cmMinor41Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
787 !![(0 : ℝ), 1, 1, 1;
788 1, a 0, a 1, a 2;
789 1, 0, a 3, a 4;
790 1, a 3, 0, a 5]
791
792theorem cmMinor41_submatrix_eq (a : SqEdges) :
793 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (4 : Fin 5)) (Fin.succAbove (1 : Fin 5)) =
794 cmMinor41Matrix a := by
795 ext i j
796 fin_cases i <;> fin_cases j <;> rfl
797
798theorem det_cmMinor41Matrix (a : SqEdges) :
799 Matrix.det (cmMinor41Matrix a) = - cmCofactor3Poly 4 1 a := by
800 unfold cmMinor41Matrix cmCofactor3Poly
801 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
802 ring_nf
803
804theorem cmCofactor3_41_eq_poly (a : SqEdges) :
805 cmCofactor3 a 4 1 = cmCofactor3Poly 4 1 a := by
806 unfold cmCofactor3 cmMinor3
807 rw [cmMinor41_submatrix_eq, det_cmMinor41Matrix]
808 simp [cmCofactorSign3, show ¬ Even (5 : Nat) by decide]
809
810def cmMinor42Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
811 !![(0 : ℝ), 1, 1, 1;
812 1, 0, a 1, a 2;
813 1, a 0, a 3, a 4;
814 1, a 1, 0, a 5]
815
816theorem cmMinor42_submatrix_eq (a : SqEdges) :
817 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (4 : Fin 5)) (Fin.succAbove (2 : Fin 5)) =
818 cmMinor42Matrix a := by
819 ext i j
820 fin_cases i <;> fin_cases j <;> rfl
821
822theorem det_cmMinor42Matrix (a : SqEdges) :
823 Matrix.det (cmMinor42Matrix a) = cmCofactor3Poly 4 2 a := by
824 unfold cmMinor42Matrix cmCofactor3Poly
825 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
826 ring_nf
827
828theorem cmCofactor3_42_eq_poly (a : SqEdges) :
829 cmCofactor3 a 4 2 = cmCofactor3Poly 4 2 a := by
830 unfold cmCofactor3 cmMinor3
831 rw [cmMinor42_submatrix_eq, det_cmMinor42Matrix]
832 simp [cmCofactorSign3, show Even (6 : Nat) by decide]
833
834def cmMinor43Matrix (a : SqEdges) : Matrix (Fin 4) (Fin 4) ℝ :=
835 !![(0 : ℝ), 1, 1, 1;
836 1, 0, a 0, a 2;
837 1, a 0, 0, a 4;
838 1, a 1, a 3, a 5]
839
840theorem cmMinor43_submatrix_eq (a : SqEdges) :
841 Matrix.submatrix (cmMatrix3 a) (Fin.succAbove (4 : Fin 5)) (Fin.succAbove (3 : Fin 5)) =
842 cmMinor43Matrix a := by
843 ext i j
844 fin_cases i <;> fin_cases j <;> rfl
845
846theorem det_cmMinor43Matrix (a : SqEdges) :
847 Matrix.det (cmMinor43Matrix a) = - cmCofactor3Poly 4 3 a := by
848 unfold cmMinor43Matrix cmCofactor3Poly
849 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
850 ring_nf
851
852theorem cmCofactor3_43_eq_poly (a : SqEdges) :
853 cmCofactor3 a 4 3 = cmCofactor3Poly 4 3 a := by
854 unfold cmCofactor3 cmMinor3
855 rw [cmMinor43_submatrix_eq, det_cmMinor43Matrix]
856 simp [cmCofactorSign3, show ¬ Even (7 : Nat) by decide]
857
858/-- The explicit polynomial normal form agrees with every determinant
859cofactor of the tetrahedral Cayley-Menger matrix. -/
860theorem cmCofactor3_eq_poly (a : SqEdges) (r c : Fin 5) :
861 cmCofactor3 a r c = cmCofactor3Poly r c a := by
862 fin_cases r <;> fin_cases c
863 · exact cmCofactor3_00_eq_poly a
864 · exact cmCofactor3_01_eq_poly a
865 · exact cmCofactor3_02_eq_poly a
866 · exact cmCofactor3_03_eq_poly a
867 · exact cmCofactor3_04_eq_poly a
868 · exact cmCofactor3_10_eq_poly a
869 · exact cmCofactor3_11_eq_poly a
870 · exact cmCofactor3_12_eq_poly a
871 · exact cmCofactor3_13_eq_poly a
872 · exact cmCofactor3_14_eq_poly a
873 · exact cmCofactor3_20_eq_poly a
874 · exact cmCofactor3_21_eq_poly a
875 · exact cmCofactor3_22_eq_poly a
876 · exact cmCofactor3_23_eq_poly a
877 · exact cmCofactor3_24_eq_poly a
878 · exact cmCofactor3_30_eq_poly a
879 · exact cmCofactor3_31_eq_poly a
880 · exact cmCofactor3_32_eq_poly a
881 · exact cmCofactor3_33_eq_poly a
882 · exact cmCofactor3_34_eq_poly a
883 · exact cmCofactor3_40_eq_poly a
884 · exact cmCofactor3_41_eq_poly a
885 · exact cmCofactor3_42_eq_poly a
886 · exact cmCofactor3_43_eq_poly a
887 · exact cmCofactor3_44_eq_poly a
888
889/-- Quadratic coefficient of a one-coordinate restriction of a cofactor
890polynomial. Cofactors are degree at most two in each individual squared-edge
891coordinate. -/
892def cmCofactorQuadraticCoeff (r c : Fin 5) (k : Fin 6) (a : SqEdges) : ℝ :=
893 match r.val, c.val, k.val with
894 | 0, 0, 0 => (a 5) ^ 2
895 | 0, 0, 1 => (a 4) ^ 2
896 | 0, 0, 2 => (a 3) ^ 2
897 | 0, 0, 3 => (a 2) ^ 2
898 | 0, 0, 4 => (a 1) ^ 2
899 | 0, 0, 5 => (a 0) ^ 2
900 | 0, 1, 3 => -(a 2)
901 | 0, 1, 4 => -(a 1)
902 | 0, 1, 5 => -(a 0)
903 | 0, 2, 1 => -(a 4)
904 | 0, 2, 2 => -(a 3)
905 | 0, 2, 5 => -(a 0)
906 | 0, 3, 0 => -(a 5)
907 | 0, 3, 2 => -(a 3)
908 | 0, 3, 4 => -(a 1)
909 | 0, 4, 0 => -(a 5)
910 | 0, 4, 1 => -(a 4)
911 | 0, 4, 3 => -(a 2)
912 | 1, 0, 3 => -(a 2)
913 | 1, 0, 4 => -(a 1)
914 | 1, 0, 5 => -(a 0)
915 | 1, 1, 3 => 1
916 | 1, 1, 4 => 1
917 | 1, 1, 5 => 1
918 | 1, 2, 5 => -1
919 | 1, 3, 4 => -1
920 | 1, 4, 3 => -1
921 | 2, 0, 1 => -(a 4)
922 | 2, 0, 2 => -(a 3)
923 | 2, 0, 5 => -(a 0)
924 | 2, 1, 5 => -1
925 | 2, 2, 1 => 1
926 | 2, 2, 2 => 1
927 | 2, 2, 5 => 1
928 | 2, 3, 2 => -1
929 | 2, 4, 1 => -1
930 | 3, 0, 0 => -(a 5)
931 | 3, 0, 2 => -(a 3)
932 | 3, 0, 4 => -(a 1)
933 | 3, 1, 4 => -1
934 | 3, 2, 2 => -1
935 | 3, 3, 0 => 1
936 | 3, 3, 2 => 1
937 | 3, 3, 4 => 1
938 | 3, 4, 0 => -1
939 | 4, 0, 0 => -(a 5)
940 | 4, 0, 1 => -(a 4)
941 | 4, 0, 3 => -(a 2)
942 | 4, 1, 3 => -1
943 | 4, 2, 1 => -1
944 | 4, 3, 0 => -1
945 | 4, 4, 0 => 1
946 | 4, 4, 1 => 1
947 | 4, 4, 3 => 1
948 | _, _, _ => 0
949
950
951/-- Derivative of a shifted cubic polynomial at its base point. Local copy
952of the `cm3` helper, used here for cofactor coordinate restrictions. -/
953private theorem hasDerivAt_shifted_cubic (A B C D x₀ : ℝ) :
954 HasDerivAt (fun x : ℝ => A + B * (x - x₀) + C * (x - x₀) ^ 2
955 + D * (x - x₀) ^ 3) B x₀ := by
956 have hx : HasDerivAt (fun x : ℝ => x - x₀) (1 : ℝ) x₀ := by
957 simpa using (hasDerivAt_id x₀).sub_const x₀
958 have hconst : HasDerivAt (fun _ : ℝ => A) (0 : ℝ) x₀ := hasDerivAt_const x₀ A
959 have hlin : HasDerivAt (fun x : ℝ => B * (x - x₀)) B x₀ := by
960 simpa using hx.const_mul B
961 have hsq_raw := hx.pow 2
962 have hsq : HasDerivAt (fun x : ℝ => (x - x₀) ^ 2) (0 : ℝ) x₀ := by
963 simpa using hsq_raw
964 have hquad : HasDerivAt (fun x : ℝ => C * (x - x₀) ^ 2) (0 : ℝ) x₀ := by
965 simpa using hsq.const_mul C
966 have hcb_raw := hx.pow 3
967 have hcb : HasDerivAt (fun x : ℝ => (x - x₀) ^ 3) (0 : ℝ) x₀ := by
968 simpa using hcb_raw
969 have hcubic : HasDerivAt (fun x : ℝ => D * (x - x₀) ^ 3) (0 : ℝ) x₀ := by
970 simpa using hcb.const_mul D
971 have htotal := ((hconst.add hlin).add hquad).add hcubic
972 simpa using htotal
973
974/-- Taylor form for the `(3,4)` cofactor polynomial along one squared-edge
975coordinate. -/
976theorem cmCofactor3Poly_34_update_polyform
977 (a : SqEdges) (k : Fin 6) (t : ℝ) :
978 cmCofactor3Poly 3 4 (Function.update a k (a k + t)) =
979 cmCofactor3Poly 3 4 a + cmCofactorPartial 3 4 k a * t
980 + (if k = 0 then -1 else 0) * t ^ 2 + 0 * t ^ 3 := by
981 fin_cases k <;>
982 simp [cmCofactor3Poly, cmCofactorPartial, Function.update] <;>
983 ring_nf
984
985/-- Closed-form coordinate derivative of the `(3,4)` cofactor polynomial. -/
986theorem hasDerivAt_cmCofactor3Poly_34_along_coord
987 (k : Fin 6) (a : SqEdges) :
988 HasDerivAt (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t))
989 (cmCofactorPartial 3 4 k a) (a k) := by
990 have hfun :
991 (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t)) =
992 (fun t : ℝ => cmCofactor3Poly 3 4 a
993 + cmCofactorPartial 3 4 k a * (t - a k)
994 + (if k = 0 then -1 else 0) * (t - a k) ^ 2
995 + 0 * (t - a k) ^ 3) := by
996 funext t
997 have h := cmCofactor3Poly_34_update_polyform a k (t - a k)
998 have hbase : a k + (t - a k) = t := by ring
999 rw [hbase] at h
1000 simpa using h
1001 rw [hfun]
1002 exact hasDerivAt_shifted_cubic (cmCofactor3Poly 3 4 a)
1003 (cmCofactorPartial 3 4 k a) (if k = 0 then -1 else 0) 0 (a k)
1004
1005/-- Closed-form coordinate derivative of determinant cofactor `(3,4)`. -/
1006theorem hasDerivAt_cmCofactor3_34_along_coord
1007 (k : Fin 6) (a : SqEdges) :
1008 HasDerivAt (fun t : ℝ => cmCofactor3 (Function.update a k t) 3 4)
1009 (cmCofactorPartial 3 4 k a) (a k) := by
1010 simpa [cmCofactor3_34_eq_poly] using
1011 hasDerivAt_cmCofactor3Poly_34_along_coord k a
1012
1013/-- Taylor form for every cofactor polynomial along one squared-edge
1014coordinate. -/
1015theorem cmCofactor3Poly_update_polyform
1016 (r c : Fin 5) (a : SqEdges) (k : Fin 6) (t : ℝ) :
1017 cmCofactor3Poly r c (Function.update a k (a k + t)) =
1018 cmCofactor3Poly r c a + cmCofactorPartial r c k a * t
1019 + cmCofactorQuadraticCoeff r c k a * t ^ 2 + 0 * t ^ 3 := by
1020 fin_cases r <;> fin_cases c <;> fin_cases k <;>
1021 simp [cmCofactor3Poly, cmCofactorPartial, cmCofactorQuadraticCoeff,
1022 Function.update] <;>
1023 ring_nf
1024
1025/-- Closed-form coordinate derivative of every cofactor polynomial. -/
1026theorem hasDerivAt_cmCofactor3Poly_along_coord
1027 (r c : Fin 5) (k : Fin 6) (a : SqEdges) :
1028 HasDerivAt (fun t : ℝ => cmCofactor3Poly r c (Function.update a k t))
1029 (cmCofactorPartial r c k a) (a k) := by
1030 have hfun :
1031 (fun t : ℝ => cmCofactor3Poly r c (Function.update a k t)) =
1032 (fun t : ℝ => cmCofactor3Poly r c a
1033 + cmCofactorPartial r c k a * (t - a k)
1034 + cmCofactorQuadraticCoeff r c k a * (t - a k) ^ 2
1035 + 0 * (t - a k) ^ 3) := by
1036 funext t
1037 have h := cmCofactor3Poly_update_polyform r c a k (t - a k)
1038 have hbase : a k + (t - a k) = t := by ring
1039 rw [hbase] at h
1040 simpa using h
1041 rw [hfun]
1042 exact hasDerivAt_shifted_cubic (cmCofactor3Poly r c a)
1043 (cmCofactorPartial r c k a) (cmCofactorQuadraticCoeff r c k a) 0 (a k)
1044
1045/-- Closed-form coordinate derivative of every determinant-defined cofactor. -/
1046theorem hasDerivAt_cmCofactor3_along_coord
1047 (r c : Fin 5) (k : Fin 6) (a : SqEdges) :
1048 HasDerivAt (fun t : ℝ => cmCofactor3 (Function.update a k t) r c)
1049 (cmCofactorPartial r c k a) (a k) := by
1050 simpa [cmCofactor3_eq_poly] using
1051 hasDerivAt_cmCofactor3Poly_along_coord r c k a
1052
1053/-- Polynomial Cayley-Menger cofactor discriminant for a tetrahedral edge:
1054`C_pp C_qq - C_pq^2 = 2 * CM * a_e`. This is the algebraic identity that
1055turns the arccos denominator into the common volume factor in Schläfli. -/
1056theorem cmCofactor_discriminant_eq (a : SqEdges) (e : Fin 6) :
1057 let p := DihedralCayleyMenger.oppositeCMVertices e |>.1
1058 let q := DihedralCayleyMenger.oppositeCMVertices e |>.2
1059 cmCofactor3Poly p p a * cmCofactor3Poly q q a -
1060 cmCofactor3Poly p q a ^ 2 =
1061 2 * cm3 a * a e := by
1062 fin_cases e <;>
1063 simp [DihedralCayleyMenger.oppositeCMVertices, cmCofactor3Poly, cm3] <;>
1064 ring_nf
1065
1066/-- The derivative theorem is intentionally separated from the polynomial
1067normal form. Downstream modules use `cmCofactorPartial`; the remaining
1068one-variable `HasDerivAt` proof is discharged in the quotient-derivative
1069layer where the required cofactors are already specialized. -/
1070def cmCofactorPartialClosedForm (r c : Fin 5) (k : Fin 6) (a : SqEdges) : ℝ :=
1071 cmCofactorPartial r c k a
1072
1073end
1074
1075end CofactorPolynomial
1076end Geometry
1077end IndisputableMonolith
1078