IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DStarKernel.lean · 1083 lines · 114 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
3import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
4import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
5
6/-!
7# Regge 4D full periodic-lattice star deficit class kernel
8
9QG full-theory campaign, next kernel-checked increment after
10`ReggeHinge4DDihedralKernel`. Imports the Freudenthal incidence layer,
11the 15-class stencil, and the seed two-simplex dihedral cosine calculus;
12never redefines their API.
13
14## Tier tags (binding)
15
16* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
17 `admit`, no new axioms, no `native_decide`, no `: True` shells).
18* Scope: the seed triangle hinge `{0, e₀, e₀+e₁}` and its **full**
19 periodic Freudenthal star in the integer lattice (four containing
20 unit cubes, six incident 4-simplices). Other hinge orbits of the
21 lattice are OPEN.
22* This does **not** complete the flat Hessian assembly over all hinges.
23* This does **not** prove `S_RS_converges_EH_4d`.
24* This does **not** flip `gap_action_recovery`.
25* This does **not** reverse-engineer weights from Einstein–Hilbert.
26
27## What is proved (deliverable A)
28
291. **Star enumeration.** Exactly six `(cube translate, Kuhn simplex)`
30 pairs contain the seed hinge.
312. **Flat cosine multiset.** Four simplices have flat cosine `1/√2`
32 and two have flat cosine `0`, from each orbit's own Gram vector.
333. **Flatness gate.** Star angle sum equals exactly `2π`.
344. **Full-star deficit class kernel** on classes
35 `(2,3,6,7,10,11,14)` with values `(-1,-1,+1,-1,+1,+1,-1)`.
365. **Gates:** nonvacuity, swap-`2↔3` symmetry, uniform-scaling decoy,
37 homothety stationarity.
38
39Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
40-/
41
42namespace IndisputableMonolith
43namespace Gravity
44namespace Analysis
45namespace ReggeHinge4DStarKernel
46
47open BigOperators
48open ReggeHinge4DFlatKernel
49open ReggeHinge4DDihedralKernel
50open ReggeEdgeStencil4D
51
52noncomputable section
53
54/-! ## §1. Cube translates and star enumeration -/
55
56inductive CubeTranslate
57 | origin
58 | minusE2
59 | minusE3
60 | minusE2E3
61 deriving DecidableEq, Repr, Fintype
62
63def localHingeMasks : CubeTranslate → Finset ℕ
64 | .origin => {0, 1, 3}
65 | .minusE2 => {4, 5, 7}
66 | .minusE3 => {8, 9, 11}
67 | .minusE2E3 => {12, 13, 15}
68
69def containsHinge (c : CubeTranslate) (s : Fin 24) : Bool :=
70 decide (∀ m ∈ localHingeMasks c, ∃ i : Fin 5, vertexMask s i = m)
71
72structure StarMember where
73 cube : CubeTranslate
74 simplex : Fin 24
75 deriving DecidableEq, Repr
76
77def starMembers : List StarMember :=
78 [ ⟨.origin, 0⟩, ⟨.origin, 1⟩
79 , ⟨.minusE2, 12⟩, ⟨.minusE3, 18⟩
80 , ⟨.minusE2E3, 16⟩, ⟨.minusE2E3, 22⟩ ]
81
82theorem starMembers_length : starMembers.length = 6 := rfl
83
84theorem starMembers_complete (c : CubeTranslate) (s : Fin 24) :
85 containsHinge c s = true ↔ ⟨c, s⟩ ∈ starMembers := by
86 cases c <;> fin_cases s <;> decide
87
88theorem star_cardinality :
89 (Finset.univ.filter (fun p : CubeTranslate × Fin 24 =>
90 containsHinge p.1 p.2 = true)).card = 6 := by
91 decide
92
93/-! ## §2. Flat squared-length orbit representatives -/
94
95def oppFlatSqEdges : SqEdges4
96 | 0 => 1 | 1 => 2 | 2 => 2 | 3 => 1 | 4 => 1
97 | 5 => 3 | 6 => 2 | 7 => 4 | 8 => 3 | 9 => 1
98
99def orthFlatSqEdges : SqEdges4
100 | 0 => 1 | 1 => 2 | 2 => 1 | 3 => 3 | 4 => 1
101 | 5 => 2 | 6 => 2 | 7 => 3 | 8 => 1 | 9 => 4
102
103theorem hingeGramDet_opp : hingeGramDet oppFlatSqEdges = 4 := by
104 norm_num [hingeGramDet, oppFlatSqEdges]
105theorem apexDotNum_opp : apexDotNum oppFlatSqEdges = 8 := by
106 norm_num [apexDotNum, hingeGramDet, oppFlatSqEdges]
107theorem apex3NormSqNum_opp : apex3NormSqNum oppFlatSqEdges = 8 := by
108 norm_num [apex3NormSqNum, hingeGramDet, oppFlatSqEdges]
109theorem apex4NormSqNum_opp : apex4NormSqNum oppFlatSqEdges = 4 := by
110 norm_num [apex4NormSqNum, hingeGramDet, oppFlatSqEdges]
111
112theorem hingeGramDet_orth : hingeGramDet orthFlatSqEdges = 4 := by
113 norm_num [hingeGramDet, orthFlatSqEdges]
114theorem apexDotNum_orth : apexDotNum orthFlatSqEdges = 0 := by
115 norm_num [apexDotNum, hingeGramDet, orthFlatSqEdges]
116theorem apex3NormSqNum_orth : apex3NormSqNum orthFlatSqEdges = 4 := by
117 norm_num [apex3NormSqNum, hingeGramDet, orthFlatSqEdges]
118theorem apex4NormSqNum_orth : apex4NormSqNum orthFlatSqEdges = 4 := by
119 norm_num [apex4NormSqNum, hingeGramDet, orthFlatSqEdges]
120
121theorem cosDihedral_opp_flat :
122 cosDihedral oppFlatSqEdges = 1 / Real.sqrt 2 := by
123 rw [cos_numForm _ (by rw [hingeGramDet_opp]; norm_num),
124 apexDotNum_opp, apex3NormSqNum_opp, apex4NormSqNum_opp]
125 rw [show (8 : ℝ) * 4 = 32 by norm_num,
126 show (32 : ℝ) = 4 ^ 2 * 2 by norm_num,
127 Real.sqrt_mul (by positivity : (0 : ℝ) ≤ 4 ^ 2) 2,
128 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
129 rw [div_eq_div_iff (by positivity)
130 (ne_of_gt (Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)))]
131 ring
132
133theorem cosDihedral_orth_flat : cosDihedral orthFlatSqEdges = 0 := by
134 rw [cos_numForm _ (by rw [hingeGramDet_orth]; norm_num),
135 apexDotNum_orth, apex3NormSqNum_orth, apex4NormSqNum_orth]
136 norm_num
137
138/-! ## §3. Flatness gate -/
139
140theorem arccos_one_div_sqrt_two :
141 Real.arccos (1 / Real.sqrt 2) = Real.pi / 4 := by
142 have hcos : Real.cos (Real.pi / 4) = Real.sqrt 2 / 2 := Real.cos_pi_div_four
143 have heq : (1 : ℝ) / Real.sqrt 2 = Real.sqrt 2 / 2 := by
144 have hs : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
145 rw [div_eq_div_iff hs (by norm_num : (2 : ℝ) ≠ 0), one_mul,
146 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
147 rw [heq, ← hcos, Real.arccos_cos (by positivity) (by
148 have : (0 : ℝ) < Real.pi := Real.pi_pos
149 linarith)]
150
151def flatAngleSeedOpp : ℝ := Real.arccos (1 / Real.sqrt 2)
152def flatAngleOrth : ℝ := Real.arccos 0
153
154theorem flatAngleSeedOpp_eq : flatAngleSeedOpp = Real.pi / 4 :=
155 arccos_one_div_sqrt_two
156theorem flatAngleOrth_eq : flatAngleOrth = Real.pi / 2 := Real.arccos_zero
157
158def starFlatAngleSum : ℝ := 4 * flatAngleSeedOpp + 2 * flatAngleOrth
159
160theorem star_flat_angle_sum_two_pi : starFlatAngleSum = 2 * Real.pi := by
161 simp only [starFlatAngleSum, flatAngleSeedOpp_eq, flatAngleOrth_eq]
162 ring
163
164def starFlatCosines : Fin 6 → ℝ
165 | ⟨0, _⟩ | ⟨1, _⟩ => 1 / Real.sqrt 2
166 | ⟨2, _⟩ | ⟨3, _⟩ => 0
167 | ⟨4, _⟩ | ⟨5, _⟩ => 1 / Real.sqrt 2
168
169theorem starFlatCosines_match_orbits :
170 starFlatCosines 0 = cosDihedral seedFlatSqEdges ∧
171 starFlatCosines 2 = cosDihedral orthFlatSqEdges ∧
172 starFlatCosines 4 = cosDihedral oppFlatSqEdges :=
173 ⟨cosDihedral_flat.symm, cosDihedral_orth_flat.symm, cosDihedral_opp_flat.symm⟩
174
175
176/-! ## §4. Opposite-orbit cosine derivatives -/
177
178def oppCoordPath (k : Fin 10) (t : ℝ) : SqEdges4 :=
179 fun j => if j = k then t else oppFlatSqEdges j
180
181def oppCosKernel : Fin 10 → ℝ
182 | ⟨2, _⟩ => Real.sqrt 2 / 8
183 | ⟨9, _⟩ => -(Real.sqrt 2) / 4
184 | _ => 0
185
186private lemma hasDerivAt_quadPoly (a b c t0 : ℝ) :
187 HasDerivAt (fun t : ℝ => a * t ^ 2 + b * t + c) (2 * a * t0 + b) t0 := by
188 have h1 : HasDerivAt (fun t : ℝ => t ^ 2) (2 * t0) t0 := by
189 simpa using hasDerivAt_pow 2 t0
190 have h2 : HasDerivAt (fun t : ℝ => a * t ^ 2) (a * (2 * t0)) t0 :=
191 h1.const_mul a
192 have h3 : HasDerivAt (fun t : ℝ => b * t) b t0 := by
193 simpa using (hasDerivAt_id t0).const_mul b
194 have h4 := (h2.add h3).add_const c
195 convert h4 using 1
196 ring
197
198private lemma hasDerivAt_numForm_opp {N P Q : ℝ → ℝ} {t0 N' P' Q' : ℝ}
199 (hN : HasDerivAt N N' t0) (hP : HasDerivAt P P' t0)
200 (hQ : HasDerivAt Q Q' t0)
201 (hN0 : N t0 = 8) (hP0 : P t0 = 8) (hQ0 : Q t0 = 4) :
202 HasDerivAt (fun t => N t / (2 * Real.sqrt (P t * Q t)))
203 (Real.sqrt 2 * (2 * N' - P' - 2 * Q') / 32) t0 := by
204 have hs2 : Real.sqrt 2 * Real.sqrt 2 = 2 :=
205 Real.mul_self_sqrt (by norm_num)
206 have hPQ : HasDerivAt (fun t => P t * Q t)
207 (P' * Q t0 + P t0 * Q') t0 := hP.mul hQ
208 have hPQ0 : P t0 * Q t0 = 32 := by rw [hP0, hQ0]; norm_num
209 have hPQne : P t0 * Q t0 ≠ 0 := by rw [hPQ0]; norm_num
210 have hsqrt : HasDerivAt (fun t => Real.sqrt (P t * Q t))
211 ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0))) t0 :=
212 hPQ.sqrt hPQne
213 have hden : HasDerivAt (fun t => 2 * Real.sqrt (P t * Q t))
214 (2 * ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0)))) t0 :=
215 hsqrt.const_mul 2
216 have hdenne : 2 * Real.sqrt (P t0 * Q t0) ≠ 0 := by
217 rw [hPQ0]; positivity
218 have hdiv := hN.div hden hdenne
219 convert hdiv using 1
220 have h32 : Real.sqrt (P t0 * Q t0) = 4 * Real.sqrt 2 := by
221 rw [hPQ0, show (32 : ℝ) = 4 ^ 2 * 2 by norm_num,
222 Real.sqrt_mul (by positivity : (0 : ℝ) ≤ 4 ^ 2) 2,
223 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
224 -- Quotient-rule value at these constants:
225 -- (N'*den - N*den')/den^2 with den = 8√2, N=8, den' = (4P'+8Q')/(4√2) = (P'+2Q')/√2
226 -- = (8√2 N' - 8(P'+2Q')/√2) / 128
227 -- = (√2 N' - (P'+2Q')/√2) / 16
228 -- = (2N' - P' - 2Q')/(16√2)
229 -- = √2 (2N' - P' - 2Q') / 32
230 rw [h32, hN0, hP0, hQ0]
231 have hpow : (2 * (4 * Real.sqrt 2)) ^ 2 = 128 := by
232 rw [show (2 * (4 * Real.sqrt 2)) ^ 2
233 = 64 * (Real.sqrt 2 * Real.sqrt 2) from by ring, hs2]
234 norm_num
235 rw [hpow]
236 have hden' :
237 2 * ((P' * (4 : ℝ) + (8 : ℝ) * Q') / (2 * (4 * Real.sqrt 2))) =
238 (P' + 2 * Q') / Real.sqrt 2 := by
239 field_simp [hs2]
240 ring
241 -- After convert, goal is equality of the two derivative expressions.
242 -- Rewrite the den' factor appearing in the quotient rule.
243 simp only [hden']
244 -- Clear denominators, then replace √2 ^ 2 by 2.
245 field_simp
246 simp only [pow_two, hs2]
247 ring
248
249private lemma hasDerivAt_opp_slot (k : Fin 10) (t0 : ℝ)
250 (aN bN cN aP bP cP aQ bQ cQ aD bD cD : ℝ)
251 (hpath : ∀ t : ℝ,
252 apexDotNum (oppCoordPath k t) = aN * t ^ 2 + bN * t + cN
253 ∧ apex3NormSqNum (oppCoordPath k t) = aP * t ^ 2 + bP * t + cP
254 ∧ apex4NormSqNum (oppCoordPath k t) = aQ * t ^ 2 + bQ * t + cQ
255 ∧ hingeGramDet (oppCoordPath k t) = aD * t ^ 2 + bD * t + cD)
256 (hN0 : aN * t0 ^ 2 + bN * t0 + cN = 8)
257 (hP0 : aP * t0 ^ 2 + bP * t0 + cP = 8)
258 (hQ0 : aQ * t0 ^ 2 + bQ * t0 + cQ = 4)
259 (hD0 : 0 < aD * t0 ^ 2 + bD * t0 + cD) :
260 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath k t))
261 (Real.sqrt 2 * (2 * (2 * aN * t0 + bN) - (2 * aP * t0 + bP)
262 - 2 * (2 * aQ * t0 + bQ)) / 32) t0 := by
263 have hN := hasDerivAt_quadPoly aN bN cN t0
264 have hP := hasDerivAt_quadPoly aP bP cP t0
265 have hQ := hasDerivAt_quadPoly aQ bQ cQ t0
266 have hmain := hasDerivAt_numForm_opp hN hP hQ hN0 hP0 hQ0
267 refine hmain.congr_of_eventuallyEq ?_
268 have hDcont : Continuous fun t : ℝ => aD * t ^ 2 + bD * t + cD := by
269 continuity
270 have hDev : ∀ᶠ t in nhds t0, 0 < aD * t ^ 2 + bD * t + cD :=
271 (hDcont.tendsto t0).eventually (eventually_gt_nhds hD0)
272 filter_upwards [hDev] with t ht
273 have hp := hpath t
274 rw [cos_numForm (oppCoordPath k t) (by rw [hp.2.2.2]; exact ht),
275 hp.1, hp.2.1, hp.2.2.1]
276
277private lemma opp_path0_polys : ∀ t : ℝ,
278 apexDotNum (oppCoordPath 0 t) = (-6) * t ^ 2 + (20) * t + (-6)
279 ∧ apex3NormSqNum (oppCoordPath 0 t) = (-4) * t ^ 2 + (16) * t + (-4)
280 ∧ apex4NormSqNum (oppCoordPath 0 t) = (-3) * t ^ 2 + (10) * t + (-3)
281 ∧ hingeGramDet (oppCoordPath 0 t) = (-1) * t ^ 2 + (6) * t + (-1) := by
282 intro t
283 refine ⟨?_, ?_, ?_, ?_⟩ <;>
284 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
285 oppCoordPath, oppFlatSqEdges] <;> ring
286
287private lemma opp_path1_polys : ∀ t : ℝ,
288 apexDotNum (oppCoordPath 1 t) = (-4) * t ^ 2 + (16) * t + (-8)
289 ∧ apex3NormSqNum (oppCoordPath 1 t) = (-3) * t ^ 2 + (12) * t + (-4)
290 ∧ apex4NormSqNum (oppCoordPath 1 t) = (-2) * t ^ 2 + (8) * t + (-4)
291 ∧ hingeGramDet (oppCoordPath 1 t) = (-1) * t ^ 2 + (4) * t + (0) := by
292 intro t
293 refine ⟨?_, ?_, ?_, ?_⟩ <;>
294 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
295 oppCoordPath, oppFlatSqEdges] <;> ring
296
297private lemma opp_path2_polys : ∀ t : ℝ,
298 apexDotNum (oppCoordPath 2 t) = (0) * t ^ 2 + (4) * t + (0)
299 ∧ apex3NormSqNum (oppCoordPath 2 t) = (-1) * t ^ 2 + (8) * t + (-4)
300 ∧ apex4NormSqNum (oppCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (4)
301 ∧ hingeGramDet (oppCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (4) := by
302 intro t
303 refine ⟨?_, ?_, ?_, ?_⟩ <;>
304 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
305 oppCoordPath, oppFlatSqEdges] <;> ring
306
307private lemma opp_path3_polys : ∀ t : ℝ,
308 apexDotNum (oppCoordPath 3 t) = (0) * t ^ 2 + (4) * t + (4)
309 ∧ apex3NormSqNum (oppCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (8)
310 ∧ apex4NormSqNum (oppCoordPath 3 t) = (-1) * t ^ 2 + (6) * t + (-1)
311 ∧ hingeGramDet (oppCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (4) := by
312 intro t
313 refine ⟨?_, ?_, ?_, ?_⟩ <;>
314 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
315 oppCoordPath, oppFlatSqEdges] <;> ring
316
317private lemma opp_path4_polys : ∀ t : ℝ,
318 apexDotNum (oppCoordPath 4 t) = (-2) * t ^ 2 + (12) * t + (-2)
319 ∧ apex3NormSqNum (oppCoordPath 4 t) = (-2) * t ^ 2 + (12) * t + (-2)
320 ∧ apex4NormSqNum (oppCoordPath 4 t) = (-1) * t ^ 2 + (6) * t + (-1)
321 ∧ hingeGramDet (oppCoordPath 4 t) = (-1) * t ^ 2 + (6) * t + (-1) := by
322 intro t
323 refine ⟨?_, ?_, ?_, ?_⟩ <;>
324 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
325 oppCoordPath, oppFlatSqEdges] <;> ring
326
327private lemma opp_path5_polys : ∀ t : ℝ,
328 apexDotNum (oppCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (8)
329 ∧ apex3NormSqNum (oppCoordPath 5 t) = (-2) * t ^ 2 + (12) * t + (-10)
330 ∧ apex4NormSqNum (oppCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (4)
331 ∧ hingeGramDet (oppCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (4) := by
332 intro t
333 refine ⟨?_, ?_, ?_, ?_⟩ <;>
334 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
335 oppCoordPath, oppFlatSqEdges] <;> ring
336
337private lemma opp_path6_polys : ∀ t : ℝ,
338 apexDotNum (oppCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (8)
339 ∧ apex3NormSqNum (oppCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (8)
340 ∧ apex4NormSqNum (oppCoordPath 6 t) = (-2) * t ^ 2 + (8) * t + (-4)
341 ∧ hingeGramDet (oppCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (4) := by
342 intro t
343 refine ⟨?_, ?_, ?_, ?_⟩ <;>
344 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
345 oppCoordPath, oppFlatSqEdges] <;> ring
346
347private lemma opp_path7_polys : ∀ t : ℝ,
348 apexDotNum (oppCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (8)
349 ∧ apex3NormSqNum (oppCoordPath 7 t) = (-1) * t ^ 2 + (8) * t + (-8)
350 ∧ apex4NormSqNum (oppCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (4)
351 ∧ hingeGramDet (oppCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (4) := by
352 intro t
353 refine ⟨?_, ?_, ?_, ?_⟩ <;>
354 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
355 oppCoordPath, oppFlatSqEdges] <;> ring
356
357private lemma opp_path8_polys : ∀ t : ℝ,
358 apexDotNum (oppCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (8)
359 ∧ apex3NormSqNum (oppCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (8)
360 ∧ apex4NormSqNum (oppCoordPath 8 t) = (-1) * t ^ 2 + (6) * t + (-5)
361 ∧ hingeGramDet (oppCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (4) := by
362 intro t
363 refine ⟨?_, ?_, ?_, ?_⟩ <;>
364 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
365 oppCoordPath, oppFlatSqEdges] <;> ring
366
367private lemma opp_path9_polys : ∀ t : ℝ,
368 apexDotNum (oppCoordPath 9 t) = (0) * t ^ 2 + (-4) * t + (12)
369 ∧ apex3NormSqNum (oppCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8)
370 ∧ apex4NormSqNum (oppCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (4)
371 ∧ hingeGramDet (oppCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (4) := by
372 intro t
373 refine ⟨?_, ?_, ?_, ?_⟩ <;>
374 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
375 oppCoordPath, oppFlatSqEdges] <;> ring
376
377theorem hasDerivAt_opp_slot0 :
378 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 0 t))
379 (0) 1 := by
380 have h := hasDerivAt_opp_slot 0 1 (-6) (20) (-6) (-4) (16) (-4)
381 (-3) (10) (-3) (-1) (6) (-1) opp_path0_polys
382 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
383 convert h using 1
384 ring
385
386theorem hasDerivAt_opp_slot1 :
387 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 1 t))
388 (0) 2 := by
389 have h := hasDerivAt_opp_slot 1 2 (-4) (16) (-8) (-3) (12) (-4)
390 (-2) (8) (-4) (-1) (4) (0) opp_path1_polys
391 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
392 convert h using 1
393 ring
394
395theorem hasDerivAt_opp_slot2 :
396 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 2 t))
397 (Real.sqrt 2 / 8) 2 := by
398 have h := hasDerivAt_opp_slot 2 2 (0) (4) (0) (-1) (8) (-4)
399 (0) (0) (4) (0) (0) (4) opp_path2_polys
400 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
401 convert h using 1
402 ring
403
404theorem hasDerivAt_opp_slot3 :
405 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 3 t))
406 (0) 1 := by
407 have h := hasDerivAt_opp_slot 3 1 (0) (4) (4) (0) (0) (8)
408 (-1) (6) (-1) (0) (0) (4) opp_path3_polys
409 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
410 convert h using 1
411 ring
412
413theorem hasDerivAt_opp_slot4 :
414 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 4 t))
415 (0) 1 := by
416 have h := hasDerivAt_opp_slot 4 1 (-2) (12) (-2) (-2) (12) (-2)
417 (-1) (6) (-1) (-1) (6) (-1) opp_path4_polys
418 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
419 convert h using 1
420 ring
421
422theorem hasDerivAt_opp_slot5 :
423 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 5 t))
424 (0) 3 := by
425 have h := hasDerivAt_opp_slot 5 3 (0) (0) (8) (-2) (12) (-10)
426 (0) (0) (4) (0) (0) (4) opp_path5_polys
427 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
428 convert h using 1
429 ring
430
431theorem hasDerivAt_opp_slot6 :
432 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 6 t))
433 (0) 2 := by
434 have h := hasDerivAt_opp_slot 6 2 (0) (0) (8) (0) (0) (8)
435 (-2) (8) (-4) (0) (0) (4) opp_path6_polys
436 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
437 convert h using 1
438 ring
439
440theorem hasDerivAt_opp_slot7 :
441 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 7 t))
442 (0) 4 := by
443 have h := hasDerivAt_opp_slot 7 4 (0) (0) (8) (-1) (8) (-8)
444 (0) (0) (4) (0) (0) (4) opp_path7_polys
445 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
446 convert h using 1
447 ring
448
449theorem hasDerivAt_opp_slot8 :
450 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 8 t))
451 (0) 3 := by
452 have h := hasDerivAt_opp_slot 8 3 (0) (0) (8) (0) (0) (8)
453 (-1) (6) (-5) (0) (0) (4) opp_path8_polys
454 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
455 convert h using 1
456 ring
457
458theorem hasDerivAt_opp_slot9 :
459 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath 9 t))
460 (-(Real.sqrt 2) / 4) 1 := by
461 have h := hasDerivAt_opp_slot 9 1 (0) (-4) (12) (0) (0) (8)
462 (0) (0) (4) (0) (0) (4) opp_path9_polys
463 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
464 convert h using 1
465 ring
466
467
468theorem hasDerivAt_opp_coord (k : Fin 10) :
469 HasDerivAt (fun t : ℝ => cosDihedral (oppCoordPath k t))
470 (oppCosKernel k) (oppFlatSqEdges k) := by
471 fin_cases k
472 · exact hasDerivAt_opp_slot0
473 · exact hasDerivAt_opp_slot1
474 · exact hasDerivAt_opp_slot2
475 · exact hasDerivAt_opp_slot3
476 · exact hasDerivAt_opp_slot4
477 · exact hasDerivAt_opp_slot5
478 · exact hasDerivAt_opp_slot6
479 · exact hasDerivAt_opp_slot7
480 · exact hasDerivAt_opp_slot8
481 · exact hasDerivAt_opp_slot9
482
483/-! ## §5. Orthogonal-orbit cosine derivatives -/
484
485def orthCoordPath (k : Fin 10) (t : ℝ) : SqEdges4 :=
486 fun j => if j = k then t else orthFlatSqEdges j
487
488def orthCosKernel : Fin 10 → ℝ
489 | ⟨1, _⟩ => (-1 / 2 : ℝ)
490 | ⟨3, _⟩ => (1 / 2 : ℝ)
491 | ⟨7, _⟩ => (1 / 2 : ℝ)
492 | ⟨9, _⟩ => (-1 / 2 : ℝ)
493 | _ => 0
494
495private lemma hasDerivAt_numForm_orth {N P Q : ℝ → ℝ} {t0 N' P' Q' : ℝ}
496 (hN : HasDerivAt N N' t0) (hP : HasDerivAt P P' t0)
497 (hQ : HasDerivAt Q Q' t0)
498 (hN0 : N t0 = 0) (hP0 : P t0 = 4) (hQ0 : Q t0 = 4) :
499 HasDerivAt (fun t => N t / (2 * Real.sqrt (P t * Q t)))
500 (N' / 8) t0 := by
501 have hPQ : HasDerivAt (fun t => P t * Q t)
502 (P' * Q t0 + P t0 * Q') t0 := hP.mul hQ
503 have hPQ0 : P t0 * Q t0 = 16 := by rw [hP0, hQ0]; norm_num
504 have hPQne : P t0 * Q t0 ≠ 0 := by rw [hPQ0]; norm_num
505 have hsqrt : HasDerivAt (fun t => Real.sqrt (P t * Q t))
506 ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0))) t0 :=
507 hPQ.sqrt hPQne
508 have hden : HasDerivAt (fun t => 2 * Real.sqrt (P t * Q t))
509 (2 * ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0)))) t0 :=
510 hsqrt.const_mul 2
511 have hdenne : 2 * Real.sqrt (P t0 * Q t0) ≠ 0 := by
512 rw [hPQ0]; positivity
513 have hdiv := hN.div hden hdenne
514 convert hdiv using 1
515 have h4 : Real.sqrt (P t0 * Q t0) = 4 := by
516 rw [hPQ0, show (16 : ℝ) = (4 : ℝ) ^ 2 by norm_num,
517 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
518 rw [h4, hN0]
519 ring
520
521private lemma hasDerivAt_orth_slot (k : Fin 10) (t0 : ℝ)
522 (aN bN cN aP bP cP aQ bQ cQ aD bD cD : ℝ)
523 (hpath : ∀ t : ℝ,
524 apexDotNum (orthCoordPath k t) = aN * t ^ 2 + bN * t + cN
525 ∧ apex3NormSqNum (orthCoordPath k t) = aP * t ^ 2 + bP * t + cP
526 ∧ apex4NormSqNum (orthCoordPath k t) = aQ * t ^ 2 + bQ * t + cQ
527 ∧ hingeGramDet (orthCoordPath k t) = aD * t ^ 2 + bD * t + cD)
528 (hN0 : aN * t0 ^ 2 + bN * t0 + cN = 0)
529 (hP0 : aP * t0 ^ 2 + bP * t0 + cP = 4)
530 (hQ0 : aQ * t0 ^ 2 + bQ * t0 + cQ = 4)
531 (hD0 : 0 < aD * t0 ^ 2 + bD * t0 + cD) :
532 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath k t))
533 ((2 * aN * t0 + bN) / 8) t0 := by
534 have hN := hasDerivAt_quadPoly aN bN cN t0
535 have hP := hasDerivAt_quadPoly aP bP cP t0
536 have hQ := hasDerivAt_quadPoly aQ bQ cQ t0
537 have hmain := hasDerivAt_numForm_orth hN hP hQ hN0 hP0 hQ0
538 refine hmain.congr_of_eventuallyEq ?_
539 have hDcont : Continuous fun t : ℝ => aD * t ^ 2 + bD * t + cD := by
540 continuity
541 have hDev : ∀ᶠ t in nhds t0, 0 < aD * t ^ 2 + bD * t + cD :=
542 (hDcont.tendsto t0).eventually (eventually_gt_nhds hD0)
543 filter_upwards [hDev] with t ht
544 have hp := hpath t
545 rw [cos_numForm (orthCoordPath k t) (by rw [hp.2.2.2]; exact ht),
546 hp.1, hp.2.1, hp.2.2.1]
547
548private lemma orth_path0_polys : ∀ t : ℝ,
549 apexDotNum (orthCoordPath 0 t) = (0) * t ^ 2 + (0) * t + (0)
550 ∧ apex3NormSqNum (orthCoordPath 0 t) = (-3) * t ^ 2 + (10) * t + (-3)
551 ∧ apex4NormSqNum (orthCoordPath 0 t) = (-1) * t ^ 2 + (6) * t + (-1)
552 ∧ hingeGramDet (orthCoordPath 0 t) = (-1) * t ^ 2 + (6) * t + (-1) := by
553 intro t
554 refine ⟨?_, ?_, ?_, ?_⟩ <;>
555 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
556 orthCoordPath, orthFlatSqEdges] <;> ring
557
558private lemma orth_path1_polys : ∀ t : ℝ,
559 apexDotNum (orthCoordPath 1 t) = (0) * t ^ 2 + (-4) * t + (8)
560 ∧ apex3NormSqNum (orthCoordPath 1 t) = (-2) * t ^ 2 + (8) * t + (-4)
561 ∧ apex4NormSqNum (orthCoordPath 1 t) = (-2) * t ^ 2 + (8) * t + (-4)
562 ∧ hingeGramDet (orthCoordPath 1 t) = (-1) * t ^ 2 + (4) * t + (0) := by
563 intro t
564 refine ⟨?_, ?_, ?_, ?_⟩ <;>
565 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
566 orthCoordPath, orthFlatSqEdges] <;> ring
567
568private lemma orth_path2_polys : ∀ t : ℝ,
569 apexDotNum (orthCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (0)
570 ∧ apex3NormSqNum (orthCoordPath 2 t) = (-1) * t ^ 2 + (6) * t + (-1)
571 ∧ apex4NormSqNum (orthCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (4)
572 ∧ hingeGramDet (orthCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (4) := by
573 intro t
574 refine ⟨?_, ?_, ?_, ?_⟩ <;>
575 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
576 orthCoordPath, orthFlatSqEdges] <;> ring
577
578private lemma orth_path3_polys : ∀ t : ℝ,
579 apexDotNum (orthCoordPath 3 t) = (0) * t ^ 2 + (4) * t + (-12)
580 ∧ apex3NormSqNum (orthCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (4)
581 ∧ apex4NormSqNum (orthCoordPath 3 t) = (-1) * t ^ 2 + (6) * t + (-5)
582 ∧ hingeGramDet (orthCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (4) := by
583 intro t
584 refine ⟨?_, ?_, ?_, ?_⟩ <;>
585 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
586 orthCoordPath, orthFlatSqEdges] <;> ring
587
588private lemma orth_path4_polys : ∀ t : ℝ,
589 apexDotNum (orthCoordPath 4 t) = (0) * t ^ 2 + (0) * t + (0)
590 ∧ apex3NormSqNum (orthCoordPath 4 t) = (-1) * t ^ 2 + (6) * t + (-1)
591 ∧ apex4NormSqNum (orthCoordPath 4 t) = (-3) * t ^ 2 + (10) * t + (-3)
592 ∧ hingeGramDet (orthCoordPath 4 t) = (-1) * t ^ 2 + (6) * t + (-1) := by
593 intro t
594 refine ⟨?_, ?_, ?_, ?_⟩ <;>
595 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
596 orthCoordPath, orthFlatSqEdges] <;> ring
597
598private lemma orth_path5_polys : ∀ t : ℝ,
599 apexDotNum (orthCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (0)
600 ∧ apex3NormSqNum (orthCoordPath 5 t) = (-2) * t ^ 2 + (8) * t + (-4)
601 ∧ apex4NormSqNum (orthCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (4)
602 ∧ hingeGramDet (orthCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (4) := by
603 intro t
604 refine ⟨?_, ?_, ?_, ?_⟩ <;>
605 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
606 orthCoordPath, orthFlatSqEdges] <;> ring
607
608private lemma orth_path6_polys : ∀ t : ℝ,
609 apexDotNum (orthCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (0)
610 ∧ apex3NormSqNum (orthCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (4)
611 ∧ apex4NormSqNum (orthCoordPath 6 t) = (-2) * t ^ 2 + (8) * t + (-4)
612 ∧ hingeGramDet (orthCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (4) := by
613 intro t
614 refine ⟨?_, ?_, ?_, ?_⟩ <;>
615 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
616 orthCoordPath, orthFlatSqEdges] <;> ring
617
618private lemma orth_path7_polys : ∀ t : ℝ,
619 apexDotNum (orthCoordPath 7 t) = (0) * t ^ 2 + (4) * t + (-12)
620 ∧ apex3NormSqNum (orthCoordPath 7 t) = (-1) * t ^ 2 + (6) * t + (-5)
621 ∧ apex4NormSqNum (orthCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (4)
622 ∧ hingeGramDet (orthCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (4) := by
623 intro t
624 refine ⟨?_, ?_, ?_, ?_⟩ <;>
625 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
626 orthCoordPath, orthFlatSqEdges] <;> ring
627
628private lemma orth_path8_polys : ∀ t : ℝ,
629 apexDotNum (orthCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (0)
630 ∧ apex3NormSqNum (orthCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (4)
631 ∧ apex4NormSqNum (orthCoordPath 8 t) = (-1) * t ^ 2 + (6) * t + (-1)
632 ∧ hingeGramDet (orthCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (4) := by
633 intro t
634 refine ⟨?_, ?_, ?_, ?_⟩ <;>
635 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
636 orthCoordPath, orthFlatSqEdges] <;> ring
637
638private lemma orth_path9_polys : ∀ t : ℝ,
639 apexDotNum (orthCoordPath 9 t) = (0) * t ^ 2 + (-4) * t + (16)
640 ∧ apex3NormSqNum (orthCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (4)
641 ∧ apex4NormSqNum (orthCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (4)
642 ∧ hingeGramDet (orthCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (4) := by
643 intro t
644 refine ⟨?_, ?_, ?_, ?_⟩ <;>
645 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
646 orthCoordPath, orthFlatSqEdges] <;> ring
647
648theorem hasDerivAt_orth_slot0 :
649 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 0 t))
650 (0) 1 := by
651 have h := hasDerivAt_orth_slot 0 1 (0) (0) (0) (-3) (10) (-3)
652 (-1) (6) (-1) (-1) (6) (-1) orth_path0_polys
653 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
654 convert h using 1
655 ring
656
657theorem hasDerivAt_orth_slot1 :
658 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 1 t))
659 ((-1 / 2 : ℝ)) 2 := by
660 have h := hasDerivAt_orth_slot 1 2 (0) (-4) (8) (-2) (8) (-4)
661 (-2) (8) (-4) (-1) (4) (0) orth_path1_polys
662 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
663 convert h using 1
664 ring
665
666theorem hasDerivAt_orth_slot2 :
667 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 2 t))
668 (0) 1 := by
669 have h := hasDerivAt_orth_slot 2 1 (0) (0) (0) (-1) (6) (-1)
670 (0) (0) (4) (0) (0) (4) orth_path2_polys
671 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
672 convert h using 1
673 ring
674
675theorem hasDerivAt_orth_slot3 :
676 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 3 t))
677 ((1 / 2 : ℝ)) 3 := by
678 have h := hasDerivAt_orth_slot 3 3 (0) (4) (-12) (0) (0) (4)
679 (-1) (6) (-5) (0) (0) (4) orth_path3_polys
680 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
681 convert h using 1
682 ring
683
684theorem hasDerivAt_orth_slot4 :
685 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 4 t))
686 (0) 1 := by
687 have h := hasDerivAt_orth_slot 4 1 (0) (0) (0) (-1) (6) (-1)
688 (-3) (10) (-3) (-1) (6) (-1) orth_path4_polys
689 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
690 convert h using 1
691 ring
692
693theorem hasDerivAt_orth_slot5 :
694 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 5 t))
695 (0) 2 := by
696 have h := hasDerivAt_orth_slot 5 2 (0) (0) (0) (-2) (8) (-4)
697 (0) (0) (4) (0) (0) (4) orth_path5_polys
698 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
699 convert h using 1
700 ring
701
702theorem hasDerivAt_orth_slot6 :
703 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 6 t))
704 (0) 2 := by
705 have h := hasDerivAt_orth_slot 6 2 (0) (0) (0) (0) (0) (4)
706 (-2) (8) (-4) (0) (0) (4) orth_path6_polys
707 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
708 convert h using 1
709 ring
710
711theorem hasDerivAt_orth_slot7 :
712 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 7 t))
713 ((1 / 2 : ℝ)) 3 := by
714 have h := hasDerivAt_orth_slot 7 3 (0) (4) (-12) (-1) (6) (-5)
715 (0) (0) (4) (0) (0) (4) orth_path7_polys
716 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
717 convert h using 1
718 ring
719
720theorem hasDerivAt_orth_slot8 :
721 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 8 t))
722 (0) 1 := by
723 have h := hasDerivAt_orth_slot 8 1 (0) (0) (0) (0) (0) (4)
724 (-1) (6) (-1) (0) (0) (4) orth_path8_polys
725 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
726 convert h using 1
727 ring
728
729theorem hasDerivAt_orth_slot9 :
730 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath 9 t))
731 ((-1 / 2 : ℝ)) 4 := by
732 have h := hasDerivAt_orth_slot 9 4 (0) (-4) (16) (0) (0) (4)
733 (0) (0) (4) (0) (0) (4) orth_path9_polys
734 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
735 convert h using 1
736 ring
737
738
739theorem hasDerivAt_orth_coord (k : Fin 10) :
740 HasDerivAt (fun t : ℝ => cosDihedral (orthCoordPath k t))
741 (orthCosKernel k) (orthFlatSqEdges k) := by
742 fin_cases k
743 · exact hasDerivAt_orth_slot0
744 · exact hasDerivAt_orth_slot1
745 · exact hasDerivAt_orth_slot2
746 · exact hasDerivAt_orth_slot3
747 · exact hasDerivAt_orth_slot4
748 · exact hasDerivAt_orth_slot5
749 · exact hasDerivAt_orth_slot6
750 · exact hasDerivAt_orth_slot7
751 · exact hasDerivAt_orth_slot8
752 · exact hasDerivAt_orth_slot9
753
754/-! ## §6. Full-star deficit class kernel -/
755
756def chainSeedOpp : ℝ := -(Real.sqrt 2)
757def chainOrth : ℝ := (-1 : ℝ)
758
759def oppDeficitKernel : Fin 10 → ℝ
760 | ⟨2, _⟩ => (1 / 4 : ℝ)
761 | ⟨9, _⟩ => (-1 / 2 : ℝ)
762 | _ => 0
763
764def orthDeficitKernel : Fin 10 → ℝ
765 | ⟨1, _⟩ => (-1 / 2 : ℝ)
766 | ⟨3, _⟩ => (1 / 2 : ℝ)
767 | ⟨7, _⟩ => (1 / 2 : ℝ)
768 | ⟨9, _⟩ => (-1 / 2 : ℝ)
769 | _ => 0
770
771theorem oppDeficitKernel_eq_chain :
772 oppDeficitKernel 2 = -chainSeedOpp * oppCosKernel 2 ∧
773 oppDeficitKernel 9 = -chainSeedOpp * oppCosKernel 9 := by
774 constructor
775 · simp only [oppDeficitKernel, chainSeedOpp, oppCosKernel]
776 rw [show -(-(Real.sqrt 2)) * (Real.sqrt 2 / 8)
777 = (Real.sqrt 2 * Real.sqrt 2) / 8 from by ring,
778 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 2)]; norm_num
779 · simp only [oppDeficitKernel, chainSeedOpp, oppCosKernel]
780 rw [show -(-(Real.sqrt 2)) * (-(Real.sqrt 2) / 4)
781 = -(Real.sqrt 2 * Real.sqrt 2) / 4 from by ring,
782 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 2)]; norm_num
783
784theorem orthDeficitKernel_eq_chain (k : Fin 10) :
785 orthDeficitKernel k = -chainOrth * orthCosKernel k := by
786 fin_cases k <;> simp [orthDeficitKernel, chainOrth, orthCosKernel]
787
788def starSlotClass : Fin 6 → Fin 10 → Fin 15
789 | 0, e => localEdgeClass 0 e
790 | 1, e => localEdgeClass 1 e
791 | 2, 0 => 0 | 2, 1 => 2 | 2, 2 => 3 | 2, 3 => 10 | 2, 4 => 1
792 | 2, 5 => 4 | 2, 6 => 9 | 2, 7 => 6 | 2, 8 => 7 | 2, 9 => 14
793 | 3, 0 => 0 | 3, 1 => 2 | 3, 2 => 7 | 3, 3 => 6 | 3, 4 => 1
794 | 3, 5 => 8 | 3, 6 => 5 | 3, 7 => 10 | 3, 8 => 3 | 3, 9 => 14
795 | 4, 0 => 0 | 4, 1 => 2 | 4, 2 => 11 | 4, 3 => 7 | 4, 4 => 1
796 | 4, 5 => 12 | 4, 6 => 8 | 4, 7 => 14 | 4, 8 => 10 | 4, 9 => 3
797 | 5, 0 => 0 | 5, 1 => 2 | 5, 2 => 11 | 5, 3 => 3 | 5, 4 => 1
798 | 5, 5 => 12 | 5, 6 => 4 | 5, 7 => 14 | 5, 8 => 6 | 5, 9 => 7
799
800def starLocalDeficitKernel : Fin 6 → Fin 10 → ℝ
801 | 0 | 1 => singleSimplexDeficitKernel
802 | 2 | 3 => orthDeficitKernel
803 | 4 | 5 => oppDeficitKernel
804
805def assembleStarMember (m : Fin 6) : Fin 15 → ℝ :=
806 fun d => ∑ e : Fin 10,
807 if starSlotClass m e = d then starLocalDeficitKernel m e else 0
808
809def fullStarClassKernelAssembled : Fin 15 → ℝ :=
810 fun d => ∑ m : Fin 6, assembleStarMember m d
811
812def fullStarClassKernel : Fin 15 → ℝ
813 | ⟨2, _⟩ => (-1 : ℝ)
814 | ⟨3, _⟩ => (-1 : ℝ)
815 | ⟨6, _⟩ => (1 : ℝ)
816 | ⟨7, _⟩ => (-1 : ℝ)
817 | ⟨10, _⟩ => (1 : ℝ)
818 | ⟨11, _⟩ => (1 : ℝ)
819 | ⟨14, _⟩ => (-1 : ℝ)
820 | _ => 0
821
822private lemma member0_eval (d : Fin 15) :
823 assembleStarMember 0 d =
824 (if d = 11 then (1 / 4 : ℝ) else 0) +
825 (if d = 7 then (-1 / 2 : ℝ) else 0) := by
826 change assembleClassKernel 0 singleSimplexDeficitKernel d = _
827 rw [assembleClassKernel_eval]
828 rw [show localEdgeClass 0 8 = (11 : Fin 15) from by decide,
829 show localEdgeClass 0 9 = (7 : Fin 15) from by decide,
830 singleSimplexDeficitKernel_eight, singleSimplexDeficitKernel_nine]
831 aesop
832
833private lemma member1_eval (d : Fin 15) :
834 assembleStarMember 1 d =
835 (if d = 11 then (1 / 4 : ℝ) else 0) +
836 (if d = 3 then (-1 / 2 : ℝ) else 0) := by
837 change assembleClassKernel 1 singleSimplexDeficitKernel d = _
838 rw [assembleClassKernel_eval]
839 rw [show localEdgeClass 1 8 = (11 : Fin 15) from by decide,
840 show localEdgeClass 1 9 = (3 : Fin 15) from by decide,
841 singleSimplexDeficitKernel_eight, singleSimplexDeficitKernel_nine]
842 aesop
843
844private lemma sum_support4 (f : Fin 10 → ℝ)
845 (hz : ∀ e : Fin 10, e ≠ 1 → e ≠ 3 → e ≠ 7 → e ≠ 9 → f e = 0) :
846 (∑ e : Fin 10, f e) = f 1 + f 3 + f 7 + f 9 := by
847 rw [show (Finset.univ : Finset (Fin 10)) =
848 insert (1 : Fin 10) (insert (3 : Fin 10)
849 (insert (7 : Fin 10) (insert (9 : Fin 10)
850 ({0, 2, 4, 5, 6, 8} : Finset (Fin 10))))) from by decide]
851 rw [Finset.sum_insert (by decide), Finset.sum_insert (by decide),
852 Finset.sum_insert (by decide), Finset.sum_insert (by decide),
853 Finset.sum_eq_zero (fun e he => by
854 fin_cases e <;> simp at he ⊢ <;>
855 exact hz _ (by decide) (by decide) (by decide) (by decide))]
856 abel
857
858private lemma sum_support2_29 (f : Fin 10 → ℝ)
859 (hz : ∀ e : Fin 10, e ≠ 2 → e ≠ 9 → f e = 0) :
860 (∑ e : Fin 10, f e) = f 2 + f 9 := by
861 rw [show (Finset.univ : Finset (Fin 10)) =
862 insert (2 : Fin 10) (insert (9 : Fin 10)
863 ({0, 1, 3, 4, 5, 6, 7, 8} : Finset (Fin 10))) from by decide]
864 rw [Finset.sum_insert (by decide), Finset.sum_insert (by decide),
865 Finset.sum_eq_zero (fun e he => by
866 fin_cases e <;> simp at he ⊢ <;>
867 exact hz _ (by decide) (by decide))]
868 abel
869
870private lemma orth_kernel_zero_off (e : Fin 10)
871 (h1 : e ≠ 1) (h3 : e ≠ 3) (h7 : e ≠ 7) (h9 : e ≠ 9) :
872 orthDeficitKernel e = 0 := by
873 fin_cases e <;> first | rfl | contradiction
874
875private lemma opp_kernel_zero_off (e : Fin 10) (h2 : e ≠ 2) (h9 : e ≠ 9) :
876 oppDeficitKernel e = 0 := by
877 fin_cases e <;> first | rfl | contradiction
878
879private lemma member2_eval (d : Fin 15) :
880 assembleStarMember 2 d =
881 (if d = 2 then (-1 / 2 : ℝ) else 0) +
882 (if d = 10 then (1 / 2 : ℝ) else 0) +
883 (if d = 6 then (1 / 2 : ℝ) else 0) +
884 (if d = 14 then (-1 / 2 : ℝ) else 0) := by
885 simp only [assembleStarMember, starLocalDeficitKernel]
886 rw [sum_support4 (fun e =>
887 if starSlotClass 2 e = d then orthDeficitKernel e else 0)
888 (fun e h1 h3 h7 h9 => by simp [orth_kernel_zero_off e h1 h3 h7 h9])]
889 simp only [starSlotClass, orthDeficitKernel]
890 aesop
891
892private lemma member3_eval (d : Fin 15) :
893 assembleStarMember 3 d =
894 (if d = 2 then (-1 / 2 : ℝ) else 0) +
895 (if d = 6 then (1 / 2 : ℝ) else 0) +
896 (if d = 10 then (1 / 2 : ℝ) else 0) +
897 (if d = 14 then (-1 / 2 : ℝ) else 0) := by
898 simp only [assembleStarMember, starLocalDeficitKernel]
899 rw [sum_support4 (fun e =>
900 if starSlotClass 3 e = d then orthDeficitKernel e else 0)
901 (fun e h1 h3 h7 h9 => by simp [orth_kernel_zero_off e h1 h3 h7 h9])]
902 simp only [starSlotClass, orthDeficitKernel]
903 aesop
904
905private lemma member4_eval (d : Fin 15) :
906 assembleStarMember 4 d =
907 (if d = 11 then (1 / 4 : ℝ) else 0) +
908 (if d = 3 then (-1 / 2 : ℝ) else 0) := by
909 simp only [assembleStarMember, starLocalDeficitKernel]
910 rw [sum_support2_29 (fun e =>
911 if starSlotClass 4 e = d then oppDeficitKernel e else 0)
912 (fun e h2 h9 => by simp [opp_kernel_zero_off e h2 h9])]
913 simp only [starSlotClass, oppDeficitKernel]
914 aesop
915
916private lemma member5_eval (d : Fin 15) :
917 assembleStarMember 5 d =
918 (if d = 11 then (1 / 4 : ℝ) else 0) +
919 (if d = 7 then (-1 / 2 : ℝ) else 0) := by
920 simp only [assembleStarMember, starLocalDeficitKernel]
921 rw [sum_support2_29 (fun e =>
922 if starSlotClass 5 e = d then oppDeficitKernel e else 0)
923 (fun e h2 h9 => by simp [opp_kernel_zero_off e h2 h9])]
924 simp only [starSlotClass, oppDeficitKernel]
925 aesop
926
927private lemma sum6 (f : Fin 6 → ℝ) :
928 (∑ m : Fin 6, f m) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 := by
929 rw [show (Finset.univ : Finset (Fin 6)) =
930 insert (0 : Fin 6) (insert (1 : Fin 6) (insert (2 : Fin 6)
931 (insert (3 : Fin 6) (insert (4 : Fin 6) (insert (5 : Fin 6)
932 (∅ : Finset (Fin 6))))))) from by decide]
933 simp [Finset.sum_insert]
934 ring
935
936theorem fullStarClassKernel_eq (d : Fin 15) :
937 fullStarClassKernelAssembled d = fullStarClassKernel d := by
938 simp only [fullStarClassKernelAssembled]
939 rw [sum6]
940 rw [member0_eval, member1_eval, member2_eval, member3_eval,
941 member4_eval, member5_eval]
942 fin_cases d <;> simp [fullStarClassKernel] <;> norm_num
943
944theorem fullStarClassKernel_values :
945 fullStarClassKernel 2 = (-1 : ℝ) ∧
946 fullStarClassKernel 3 = (-1 : ℝ) ∧
947 fullStarClassKernel 6 = (1 : ℝ) ∧
948 fullStarClassKernel 7 = (-1 : ℝ) ∧
949 fullStarClassKernel 10 = (1 : ℝ) ∧
950 fullStarClassKernel 11 = (1 : ℝ) ∧
951 fullStarClassKernel 14 = (-1 : ℝ) :=
952 ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
953
954theorem fullStarClassKernel_zero_off (d : Fin 15)
955 (h2 : d ≠ 2) (h3 : d ≠ 3) (h6 : d ≠ 6) (h7 : d ≠ 7)
956 (h10 : d ≠ 10) (h11 : d ≠ 11) (h14 : d ≠ 14) :
957 fullStarClassKernel d = 0 := by
958 fin_cases d <;> first | rfl | contradiction
959
960/-! ## §7. Gates -/
961
962theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 11 ≠ 0 := by
963 norm_num [fullStarClassKernel]
964
965theorem fullStarClassKernel_swap23 (d : Fin 15) :
966 fullStarClassKernel (swap23Class d) = fullStarClassKernel d := by
967 have hinv : ∀ x : Fin 15, swap23Class (swap23Class x) = x := by decide
968 have hs2 : swap23Class (2 : Fin 15) = 2 := by decide
969 have hs3 : swap23Class (3 : Fin 15) = 7 := by decide
970 have hs6 : swap23Class (6 : Fin 15) = 10 := by decide
971 have hs7 : swap23Class (7 : Fin 15) = 3 := by decide
972 have hs10 : swap23Class (10 : Fin 15) = 6 := by decide
973 have hs11 : swap23Class (11 : Fin 15) = 11 := by decide
974 have hs14 : swap23Class (14 : Fin 15) = 14 := by decide
975 by_cases h2 : d = 2
976 · subst h2; rw [hs2]
977 by_cases h3 : d = 3
978 · subst h3; rw [hs3]; rfl
979 by_cases h6 : d = 6
980 · subst h6; rw [hs6]; rfl
981 by_cases h7 : d = 7
982 · subst h7; rw [hs7]; rfl
983 by_cases h10 : d = 10
984 · subst h10; rw [hs10]; rfl
985 by_cases h11 : d = 11
986 · subst h11; rw [hs11]
987 by_cases h14 : d = 14
988 · subst h14; rw [hs14]
989 have g2 : swap23Class d ≠ 2 := fun h => h2 (by rw [← hinv d, h, hs2])
990 have g3 : swap23Class d ≠ 3 := fun h => h7 (by rw [← hinv d, h, hs3])
991 have g6 : swap23Class d ≠ 6 := fun h => h10 (by rw [← hinv d, h, hs6])
992 have g7 : swap23Class d ≠ 7 := fun h => h3 (by rw [← hinv d, h, hs7])
993 have g10 : swap23Class d ≠ 10 := fun h => h6 (by rw [← hinv d, h, hs10])
994 have g11 : swap23Class d ≠ 11 := fun h => h11 (by rw [← hinv d, h, hs11])
995 have g14 : swap23Class d ≠ 14 := fun h => h14 (by rw [← hinv d, h, hs14])
996 rw [fullStarClassKernel_zero_off _ g2 g3 g6 g7 g10 g11 g14,
997 fullStarClassKernel_zero_off _ h2 h3 h6 h7 h10 h11 h14]
998
999def fullStarDirectional (v : Fin 15 → ℝ) : ℝ :=
1000 ∑ d : Fin 15, v d * fullStarClassKernel d
1001
1002private lemma sum15_support (f : Fin 15 → ℝ)
1003 (hz : ∀ d : Fin 15, d ≠ 2 → d ≠ 3 → d ≠ 6 → d ≠ 7 → d ≠ 10 → d ≠ 11 →
1004 d ≠ 14 → f d = 0) :
1005 (∑ d : Fin 15, f d) =
1006 f 2 + f 3 + f 6 + f 7 + f 10 + f 11 + f 14 := by
1007 classical
1008 have hrest :
1009 ∑ d ∈ ({0, 1, 4, 5, 8, 9, 12, 13} : Finset (Fin 15)), f d = 0 := by
1010 refine Finset.sum_eq_zero ?_
1011 intro d hd
1012 have : d = 0 ∨ d = 1 ∨ d = 4 ∨ d = 5 ∨ d = 8 ∨ d = 9 ∨ d = 12 ∨ d = 13 := by
1013 fin_cases d <;> simp at hd ⊢
1014 rcases this with (rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl) <;>
1015 exact hz _ (by decide) (by decide) (by decide) (by decide)
1016 (by decide) (by decide) (by decide)
1017 rw [show (Finset.univ : Finset (Fin 15)) =
1018 insert (2 : Fin 15) (insert (3 : Fin 15) (insert (6 : Fin 15)
1019 (insert (7 : Fin 15) (insert (10 : Fin 15) (insert (11 : Fin 15)
1020 (insert (14 : Fin 15)
1021 ({0, 1, 4, 5, 8, 9, 12, 13} : Finset (Fin 15)))))))) from by decide]
1022 simp [Finset.sum_insert, hrest]
1023 ring
1024
1025theorem fullStar_uniformScale_decoy :
1026 fullStarDirectional (fun _ => (1 : ℝ)) = (-1 : ℝ) := by
1027 simp only [fullStarDirectional]
1028 rw [sum15_support _ (fun d h2 h3 h6 h7 h10 h11 h14 => by
1029 rw [fullStarClassKernel_zero_off d h2 h3 h6 h7 h10 h11 h14, mul_zero])]
1030 simp [fullStarClassKernel]
1031
1032theorem fullStar_homothety_stationary :
1033 fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
1034 simp only [fullStarDirectional]
1035 rw [sum15_support _ (fun d h2 h3 h6 h7 h10 h11 h14 => by
1036 rw [fullStarClassKernel_zero_off d h2 h3 h6 h7 h10 h11 h14, mul_zero])]
1037 have w2 : classWeightNat 2 = 2 := by decide
1038 have w3 : classWeightNat 3 = 1 := by decide
1039 have w6 : classWeightNat 6 = 3 := by decide
1040 have w7 : classWeightNat 7 = 1 := by decide
1041 have w10 : classWeightNat 10 = 3 := by decide
1042 have w11 : classWeightNat 11 = 2 := by decide
1043 have w14 : classWeightNat 14 = 4 := by decide
1044 simp [fullStarClassKernel, w2, w3, w6, w7, w10, w11, w14]
1045 norm_num
1046
1047/-! ## §8. Status -/
1048
1049structure Hinge4DStarKernelStatus where
1050 starEnumerationClosed : Bool
1051 flatnessGateClosed : Bool
1052 fullStarClassKernelClosed : Bool
1053 otherHingeOrbitsOpen : Bool
1054 flatHessianAssemblyOpen : Bool
1055 convergesEH4d : Bool
1056 gapActionRecovery : Bool
1057
1058def hinge4DStarKernelStatus : Hinge4DStarKernelStatus where
1059 starEnumerationClosed := true
1060 flatnessGateClosed := true
1061 fullStarClassKernelClosed := true
1062 otherHingeOrbitsOpen := true
1063 flatHessianAssemblyOpen := true
1064 convergesEH4d := false
1065 gapActionRecovery := false
1066
1067theorem hinge4DStarKernelStatus_flags :
1068 hinge4DStarKernelStatus.starEnumerationClosed = true ∧
1069 hinge4DStarKernelStatus.flatnessGateClosed = true ∧
1070 hinge4DStarKernelStatus.fullStarClassKernelClosed = true ∧
1071 hinge4DStarKernelStatus.otherHingeOrbitsOpen = true ∧
1072 hinge4DStarKernelStatus.flatHessianAssemblyOpen = true ∧
1073 hinge4DStarKernelStatus.convergesEH4d = false ∧
1074 hinge4DStarKernelStatus.gapActionRecovery = false := by
1075 decide
1076
1077end
1078
1079end ReggeHinge4DStarKernel
1080end Analysis
1081end Gravity
1082end IndisputableMonolith
1083