IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DStarKernel12.lean · 1003 lines · 109 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, type (1,2)
8
9QG full-theory campaign, next kernel-checked increment after
10`ReggeHinge4DStarKernel` (type `(1,1)` seed orbit). Imports the
11Freudenthal incidence layer, the 15-class stencil, and the committed
12Gram-projection / cleared-denominator cosine calculus; never redefines
13their API.
14
15## Tier tags (binding)
16
17* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
18 `admit`, no new axioms, no `native_decide`, no `: True` shells).
19* Scope: the type `(1,2)` triangle hinge `{0, e₀, e₀+e₁+e₂}` (masks
20 `0,1,7`; difference masks `(1,6)`) and its **full** periodic
21 Freudenthal star in the integer lattice (two containing unit cubes,
22 four incident 4-simplices). The complement-related type `(2,1)` is
23 **OPEN** (not transported in this module). Other hinge orbits remain
24 OPEN.
25* This does **not** complete the flat Hessian assembly over all hinges.
26* This does **not** prove `S_RS_converges_EH_4d`.
27* This does **not** flip `gap_action_recovery`.
28* This does **not** reverse-engineer weights from Einstein–Hilbert.
29
30## What is proved (deliverable A)
31
321. **Star enumeration.** Exactly four `(cube translate, Kuhn simplex)`
33 pairs contain the `(1,2)` representative hinge.
342. **Flat cosine multiset.** All four simplices have flat cosine `0`
35 (two local squared-length orbits), recomputed from each orbit's own
36 Gram vector via the committed `cosDihedral` pattern.
373. **Flatness gate.** Star angle sum equals exactly `2π`
38 (`4 · arccos 0 = 4 · π/2`).
394. **Full-star deficit class kernel** on all 15 stencil classes with
40 values `±√2/2`.
415. **Gates:** nonvacuity, swap-`1↔2` hinge-fixing symmetry,
42 uniform-scaling decoy `√2/2`, homothety stationarity `0`.
43
44Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
45-/
46
47namespace IndisputableMonolith
48namespace Gravity
49namespace Analysis
50namespace ReggeHinge4DStarKernel12
51
52open BigOperators
53open ReggeHinge4DFlatKernel
54open ReggeHinge4DDihedralKernel
55open ReggeEdgeStencil4D
56
57noncomputable section
58
59/-! ## §1. Cube translates and star enumeration -/
60
61inductive CubeTranslate
62 | origin
63 | minusE3
64 deriving DecidableEq, Repr, Fintype
65
66def localHingeMasks : CubeTranslate → Finset ℕ
67 | .origin => {0, 1, 7}
68 | .minusE3 => {8, 9, 15}
69
70def containsHinge (c : CubeTranslate) (s : Fin 24) : Bool :=
71 decide (∀ m ∈ localHingeMasks c, ∃ i : Fin 5, vertexMask s i = m)
72
73structure StarMember where
74 cube : CubeTranslate
75 simplex : Fin 24
76 deriving DecidableEq, Repr
77
78def starMembers : List StarMember :=
79 [ ⟨.origin, 0⟩, ⟨.origin, 2⟩
80 , ⟨.minusE3, 18⟩, ⟨.minusE3, 19⟩ ]
81
82theorem starMembers_length : starMembers.length = 4 := 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 = 4 := by
91 decide
92
93/-! ## §2. Flat squared-length orbit representatives -/
94
95def nearFlatSqEdges : SqEdges4
96 | 0 => 1 | 1 => 3 | 2 => 2 | 3 => 4 | 4 => 2
97 | 5 => 1 | 6 => 3 | 7 => 1 | 8 => 1 | 9 => 2
98def farFlatSqEdges : SqEdges4
99 | 0 => 1 | 1 => 3 | 2 => 1 | 3 => 2 | 4 => 2
100 | 5 => 2 | 6 => 1 | 7 => 4 | 8 => 1 | 9 => 3
101
102theorem hingeGramDet_near : hingeGramDet nearFlatSqEdges = 8 := by
103 norm_num [hingeGramDet, nearFlatSqEdges]
104theorem apexDotNum_near : apexDotNum nearFlatSqEdges = 0 := by
105 norm_num [apexDotNum, hingeGramDet, nearFlatSqEdges]
106theorem apex3NormSqNum_near : apex3NormSqNum nearFlatSqEdges = 4 := by
107 norm_num [apex3NormSqNum, hingeGramDet, nearFlatSqEdges]
108theorem apex4NormSqNum_near : apex4NormSqNum nearFlatSqEdges = 8 := by
109 norm_num [apex4NormSqNum, hingeGramDet, nearFlatSqEdges]
110
111theorem hingeGramDet_far : hingeGramDet farFlatSqEdges = 8 := by
112 norm_num [hingeGramDet, farFlatSqEdges]
113theorem apexDotNum_far : apexDotNum farFlatSqEdges = 0 := by
114 norm_num [apexDotNum, hingeGramDet, farFlatSqEdges]
115theorem apex3NormSqNum_far : apex3NormSqNum farFlatSqEdges = 8 := by
116 norm_num [apex3NormSqNum, hingeGramDet, farFlatSqEdges]
117theorem apex4NormSqNum_far : apex4NormSqNum farFlatSqEdges = 4 := by
118 norm_num [apex4NormSqNum, hingeGramDet, farFlatSqEdges]
119
120theorem cosDihedral_near_flat : cosDihedral nearFlatSqEdges = 0 := by
121 rw [cos_numForm _ (by rw [hingeGramDet_near]; norm_num),
122 apexDotNum_near, apex3NormSqNum_near, apex4NormSqNum_near]
123 norm_num
124
125theorem cosDihedral_far_flat : cosDihedral farFlatSqEdges = 0 := by
126 rw [cos_numForm _ (by rw [hingeGramDet_far]; norm_num),
127 apexDotNum_far, apex3NormSqNum_far, apex4NormSqNum_far]
128 norm_num
129
130/-! ## §3. Flatness gate -/
131
132def flatAngleRight : ℝ := Real.arccos 0
133theorem flatAngleRight_eq : flatAngleRight = Real.pi / 2 := Real.arccos_zero
134def starFlatAngleSum : ℝ := 4 * flatAngleRight
135theorem star_flat_angle_sum_two_pi : starFlatAngleSum = 2 * Real.pi := by
136 simp only [starFlatAngleSum, flatAngleRight_eq]; ring
137
138def starFlatCosines : Fin 4 → ℝ
139 | _ => 0
140
141theorem starFlatCosines_match_orbits :
142 starFlatCosines 0 = cosDihedral nearFlatSqEdges ∧
143 starFlatCosines 2 = cosDihedral farFlatSqEdges :=
144 ⟨cosDihedral_near_flat.symm, cosDihedral_far_flat.symm⟩
145
146/-! ## §4. Coordinate paths and cosine kernels -/
147
148def nearCoordPath (k : Fin 10) (t : ℝ) : SqEdges4 :=
149 fun j => if j = k then t else nearFlatSqEdges j
150
151def farCoordPath (k : Fin 10) (t : ℝ) : SqEdges4 :=
152 fun j => if j = k then t else farFlatSqEdges j
153
154def nearCosKernel : Fin 10 → ℝ
155 | ⟨4, _⟩ => (-4 : ℝ) / (8 * Real.sqrt 2)
156 | ⟨6, _⟩ => (4 : ℝ) / (8 * Real.sqrt 2)
157 | ⟨7, _⟩ => (8 : ℝ) / (8 * Real.sqrt 2)
158 | ⟨8, _⟩ => (4 : ℝ) / (8 * Real.sqrt 2)
159 | ⟨9, _⟩ => (-8 : ℝ) / (8 * Real.sqrt 2)
160 | _ => 0
161def farCosKernel : Fin 10 → ℝ
162 | ⟨0, _⟩ => (-4 : ℝ) / (8 * Real.sqrt 2)
163 | ⟨1, _⟩ => (-4 : ℝ) / (8 * Real.sqrt 2)
164 | ⟨3, _⟩ => (8 : ℝ) / (8 * Real.sqrt 2)
165 | ⟨5, _⟩ => (4 : ℝ) / (8 * Real.sqrt 2)
166 | ⟨7, _⟩ => (4 : ℝ) / (8 * Real.sqrt 2)
167 | ⟨9, _⟩ => (-8 : ℝ) / (8 * Real.sqrt 2)
168 | _ => 0
169
170private lemma hasDerivAt_quadPoly (a b c t0 : ℝ) :
171 HasDerivAt (fun t : ℝ => a * t ^ 2 + b * t + c) (2 * a * t0 + b) t0 := by
172 have h1 : HasDerivAt (fun t : ℝ => t ^ 2) (2 * t0) t0 := by
173 simpa using hasDerivAt_pow 2 t0
174 have h2 : HasDerivAt (fun t : ℝ => a * t ^ 2) (a * (2 * t0)) t0 :=
175 h1.const_mul a
176 have h3 : HasDerivAt (fun t : ℝ => b * t) b t0 := by
177 simpa using (hasDerivAt_id t0).const_mul b
178 have h4 := (h2.add h3).add_const c
179 convert h4 using 1
180 ring
181
182private lemma hasDerivAt_numForm_zeroDot {N P Q : ℝ → ℝ} {t0 N' P' Q' : ℝ}
183 (hN : HasDerivAt N N' t0) (hP : HasDerivAt P P' t0)
184 (hQ : HasDerivAt Q Q' t0)
185 (hN0 : N t0 = 0) (hPQ0 : P t0 * Q t0 = 32) :
186 HasDerivAt (fun t => N t / (2 * Real.sqrt (P t * Q t)))
187 (N' / (8 * Real.sqrt 2)) t0 := by
188 have hPQ : HasDerivAt (fun t => P t * Q t)
189 (P' * Q t0 + P t0 * Q') t0 := hP.mul hQ
190 have hPQne : P t0 * Q t0 ≠ 0 := by rw [hPQ0]; norm_num
191 have hsqrt : HasDerivAt (fun t => Real.sqrt (P t * Q t))
192 ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0))) t0 :=
193 hPQ.sqrt hPQne
194 have hden : HasDerivAt (fun t => 2 * Real.sqrt (P t * Q t))
195 (2 * ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0)))) t0 :=
196 hsqrt.const_mul 2
197 have hdenne : 2 * Real.sqrt (P t0 * Q t0) ≠ 0 := by
198 rw [hPQ0]; positivity
199 have hdiv := hN.div hden hdenne
200 have h32 : Real.sqrt (P t0 * Q t0) = 4 * Real.sqrt 2 := by
201 rw [hPQ0, show (32 : ℝ) = 4 ^ 2 * 2 by norm_num,
202 Real.sqrt_mul (by positivity : (0 : ℝ) ≤ 4 ^ 2) 2,
203 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
204 have hs : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
205 -- Match the quotient-rule derivative at N=0, PQ=32 to N'/(8√2).
206 convert hdiv using 1
207 simp [h32, hN0]
208 field_simp [hs]
209 ring
210
211private lemma hasDerivAt_near_slot (k : Fin 10) (t0 : ℝ)
212 (aN bN cN aP bP cP aQ bQ cQ aD bD cD : ℝ)
213 (hpath : ∀ t : ℝ,
214 apexDotNum (nearCoordPath k t) = aN * t ^ 2 + bN * t + cN
215 ∧ apex3NormSqNum (nearCoordPath k t) = aP * t ^ 2 + bP * t + cP
216 ∧ apex4NormSqNum (nearCoordPath k t) = aQ * t ^ 2 + bQ * t + cQ
217 ∧ hingeGramDet (nearCoordPath k t) = aD * t ^ 2 + bD * t + cD)
218 (hN0 : aN * t0 ^ 2 + bN * t0 + cN = 0)
219 (hPQ0 : (aP * t0 ^ 2 + bP * t0 + cP) * (aQ * t0 ^ 2 + bQ * t0 + cQ) = 32)
220 (hD0 : 0 < aD * t0 ^ 2 + bD * t0 + cD) :
221 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath k t))
222 ((2 * aN * t0 + bN) / (8 * Real.sqrt 2)) t0 := by
223 have hN := hasDerivAt_quadPoly aN bN cN t0
224 have hP := hasDerivAt_quadPoly aP bP cP t0
225 have hQ := hasDerivAt_quadPoly aQ bQ cQ t0
226 have hmain :=
227 hasDerivAt_numForm_zeroDot hN hP hQ hN0 (by simpa using hPQ0)
228 refine hmain.congr_of_eventuallyEq ?_
229 have hDcont : Continuous fun t : ℝ => aD * t ^ 2 + bD * t + cD := by
230 continuity
231 have hDev : ∀ᶠ t in nhds t0, 0 < aD * t ^ 2 + bD * t + cD :=
232 (hDcont.tendsto t0).eventually (eventually_gt_nhds hD0)
233 filter_upwards [hDev] with t ht
234 have hp := hpath t
235 rw [cos_numForm (nearCoordPath k t) (by rw [hp.2.2.2]; exact ht),
236 hp.1, hp.2.1, hp.2.2.1]
237
238private lemma hasDerivAt_far_slot (k : Fin 10) (t0 : ℝ)
239 (aN bN cN aP bP cP aQ bQ cQ aD bD cD : ℝ)
240 (hpath : ∀ t : ℝ,
241 apexDotNum (farCoordPath k t) = aN * t ^ 2 + bN * t + cN
242 ∧ apex3NormSqNum (farCoordPath k t) = aP * t ^ 2 + bP * t + cP
243 ∧ apex4NormSqNum (farCoordPath k t) = aQ * t ^ 2 + bQ * t + cQ
244 ∧ hingeGramDet (farCoordPath k t) = aD * t ^ 2 + bD * t + cD)
245 (hN0 : aN * t0 ^ 2 + bN * t0 + cN = 0)
246 (hPQ0 : (aP * t0 ^ 2 + bP * t0 + cP) * (aQ * t0 ^ 2 + bQ * t0 + cQ) = 32)
247 (hD0 : 0 < aD * t0 ^ 2 + bD * t0 + cD) :
248 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath k t))
249 ((2 * aN * t0 + bN) / (8 * Real.sqrt 2)) t0 := by
250 have hN := hasDerivAt_quadPoly aN bN cN t0
251 have hP := hasDerivAt_quadPoly aP bP cP t0
252 have hQ := hasDerivAt_quadPoly aQ bQ cQ t0
253 have hmain :=
254 hasDerivAt_numForm_zeroDot hN hP hQ hN0 (by simpa using hPQ0)
255 refine hmain.congr_of_eventuallyEq ?_
256 have hDcont : Continuous fun t : ℝ => aD * t ^ 2 + bD * t + cD := by
257 continuity
258 have hDev : ∀ᶠ t in nhds t0, 0 < aD * t ^ 2 + bD * t + cD :=
259 (hDcont.tendsto t0).eventually (eventually_gt_nhds hD0)
260 filter_upwards [hDev] with t ht
261 have hp := hpath t
262 rw [cos_numForm (farCoordPath k t) (by rw [hp.2.2.2]; exact ht),
263 hp.1, hp.2.1, hp.2.2.1]
264
265private lemma near_path0_polys : ∀ t : ℝ,
266 apexDotNum (nearCoordPath 0 t) = (0) * t ^ 2 + (0) * t + (0)
267 ∧ apex3NormSqNum (nearCoordPath 0 t) = (-1) * t ^ 2 + (6) * t + (-1)
268 ∧ apex4NormSqNum (nearCoordPath 0 t) = (-1) * t ^ 2 + (10) * t + (-1)
269 ∧ hingeGramDet (nearCoordPath 0 t) = (-1) * t ^ 2 + (10) * t + (-1) := by
270 intro t
271 refine ⟨?_, ?_, ?_, ?_⟩ <;>
272 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
273 nearCoordPath, nearFlatSqEdges] <;> ring
274
275theorem hasDerivAt_near_slot0 :
276 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 0 t))
277 (0) 1 := by
278 have h := hasDerivAt_near_slot 0 1 (0) (0) (0) (-1) (6) (-1)
279 (-1) (10) (-1) (-1) (10) (-1) near_path0_polys
280 (by norm_num) (by norm_num) (by norm_num)
281 convert h using 1
282 norm_num
283
284private lemma near_path1_polys : ∀ t : ℝ,
285 apexDotNum (nearCoordPath 1 t) = (-2) * t ^ 2 + (12) * t + (-18)
286 ∧ apex3NormSqNum (nearCoordPath 1 t) = (-1) * t ^ 2 + (6) * t + (-5)
287 ∧ apex4NormSqNum (nearCoordPath 1 t) = (-3) * t ^ 2 + (18) * t + (-19)
288 ∧ hingeGramDet (nearCoordPath 1 t) = (-1) * t ^ 2 + (6) * t + (-1) := by
289 intro t
290 refine ⟨?_, ?_, ?_, ?_⟩ <;>
291 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
292 nearCoordPath, nearFlatSqEdges] <;> ring
293
294theorem hasDerivAt_near_slot1 :
295 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 1 t))
296 (0) 3 := by
297 have h := hasDerivAt_near_slot 1 3 (-2) (12) (-18) (-1) (6) (-5)
298 (-3) (18) (-19) (-1) (6) (-1) near_path1_polys
299 (by norm_num) (by norm_num) (by norm_num)
300 convert h using 1
301 norm_num
302
303private lemma near_path2_polys : ∀ t : ℝ,
304 apexDotNum (nearCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (0)
305 ∧ apex3NormSqNum (nearCoordPath 2 t) = (-2) * t ^ 2 + (8) * t + (-4)
306 ∧ apex4NormSqNum (nearCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (8)
307 ∧ hingeGramDet (nearCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (8) := by
308 intro t
309 refine ⟨?_, ?_, ?_, ?_⟩ <;>
310 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
311 nearCoordPath, nearFlatSqEdges] <;> ring
312
313theorem hasDerivAt_near_slot2 :
314 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 2 t))
315 (0) 2 := by
316 have h := hasDerivAt_near_slot 2 2 (0) (0) (0) (-2) (8) (-4)
317 (0) (0) (8) (0) (0) (8) near_path2_polys
318 (by norm_num) (by norm_num) (by norm_num)
319 convert h using 1
320 norm_num
321
322private lemma near_path3_polys : ∀ t : ℝ,
323 apexDotNum (nearCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (0)
324 ∧ apex3NormSqNum (nearCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (4)
325 ∧ apex4NormSqNum (nearCoordPath 3 t) = (-2) * t ^ 2 + (16) * t + (-24)
326 ∧ hingeGramDet (nearCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (8) := by
327 intro t
328 refine ⟨?_, ?_, ?_, ?_⟩ <;>
329 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
330 nearCoordPath, nearFlatSqEdges] <;> ring
331
332theorem hasDerivAt_near_slot3 :
333 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 3 t))
334 (0) 4 := by
335 have h := hasDerivAt_near_slot 3 4 (0) (0) (0) (0) (0) (4)
336 (-2) (16) (-24) (0) (0) (8) near_path3_polys
337 (by norm_num) (by norm_num) (by norm_num)
338 convert h using 1
339 norm_num
340
341private lemma near_path4_polys : ∀ t : ℝ,
342 apexDotNum (nearCoordPath 4 t) = (-4) * t ^ 2 + (12) * t + (-8)
343 ∧ apex3NormSqNum (nearCoordPath 4 t) = (-2) * t ^ 2 + (8) * t + (-4)
344 ∧ apex4NormSqNum (nearCoordPath 4 t) = (-4) * t ^ 2 + (20) * t + (-16)
345 ∧ hingeGramDet (nearCoordPath 4 t) = (-1) * t ^ 2 + (8) * t + (-4) := by
346 intro t
347 refine ⟨?_, ?_, ?_, ?_⟩ <;>
348 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
349 nearCoordPath, nearFlatSqEdges] <;> ring
350
351theorem hasDerivAt_near_slot4 :
352 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 4 t))
353 ((-4 : ℝ) / (8 * Real.sqrt 2)) 2 := by
354 have h := hasDerivAt_near_slot 4 2 (-4) (12) (-8) (-2) (8) (-4)
355 (-4) (20) (-16) (-1) (8) (-4) near_path4_polys
356 (by norm_num) (by norm_num) (by norm_num)
357 convert h using 1
358 norm_num
359
360private lemma near_path5_polys : ∀ t : ℝ,
361 apexDotNum (nearCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (0)
362 ∧ apex3NormSqNum (nearCoordPath 5 t) = (-3) * t ^ 2 + (10) * t + (-3)
363 ∧ apex4NormSqNum (nearCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (8)
364 ∧ hingeGramDet (nearCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (8) := by
365 intro t
366 refine ⟨?_, ?_, ?_, ?_⟩ <;>
367 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
368 nearCoordPath, nearFlatSqEdges] <;> ring
369
370theorem hasDerivAt_near_slot5 :
371 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 5 t))
372 (0) 1 := by
373 have h := hasDerivAt_near_slot 5 1 (0) (0) (0) (-3) (10) (-3)
374 (0) (0) (8) (0) (0) (8) near_path5_polys
375 (by norm_num) (by norm_num) (by norm_num)
376 convert h using 1
377 norm_num
378
379private lemma near_path6_polys : ∀ t : ℝ,
380 apexDotNum (nearCoordPath 6 t) = (0) * t ^ 2 + (4) * t + (-12)
381 ∧ apex3NormSqNum (nearCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (4)
382 ∧ apex4NormSqNum (nearCoordPath 6 t) = (-3) * t ^ 2 + (18) * t + (-19)
383 ∧ hingeGramDet (nearCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (8) := by
384 intro t
385 refine ⟨?_, ?_, ?_, ?_⟩ <;>
386 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
387 nearCoordPath, nearFlatSqEdges] <;> ring
388
389theorem hasDerivAt_near_slot6 :
390 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 6 t))
391 ((4 : ℝ) / (8 * Real.sqrt 2)) 3 := by
392 have h := hasDerivAt_near_slot 6 3 (0) (4) (-12) (0) (0) (4)
393 (-3) (18) (-19) (0) (0) (8) near_path6_polys
394 (by norm_num) (by norm_num) (by norm_num)
395 convert h using 1
396 norm_num
397
398private lemma near_path7_polys : ∀ t : ℝ,
399 apexDotNum (nearCoordPath 7 t) = (0) * t ^ 2 + (8) * t + (-8)
400 ∧ apex3NormSqNum (nearCoordPath 7 t) = (-1) * t ^ 2 + (6) * t + (-1)
401 ∧ apex4NormSqNum (nearCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (8)
402 ∧ hingeGramDet (nearCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (8) := by
403 intro t
404 refine ⟨?_, ?_, ?_, ?_⟩ <;>
405 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
406 nearCoordPath, nearFlatSqEdges] <;> ring
407
408theorem hasDerivAt_near_slot7 :
409 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 7 t))
410 ((8 : ℝ) / (8 * Real.sqrt 2)) 1 := by
411 have h := hasDerivAt_near_slot 7 1 (0) (8) (-8) (-1) (6) (-1)
412 (0) (0) (8) (0) (0) (8) near_path7_polys
413 (by norm_num) (by norm_num) (by norm_num)
414 convert h using 1
415 norm_num
416
417private lemma near_path8_polys : ∀ t : ℝ,
418 apexDotNum (nearCoordPath 8 t) = (0) * t ^ 2 + (4) * t + (-4)
419 ∧ apex3NormSqNum (nearCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (4)
420 ∧ apex4NormSqNum (nearCoordPath 8 t) = (-1) * t ^ 2 + (10) * t + (-1)
421 ∧ hingeGramDet (nearCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (8) := by
422 intro t
423 refine ⟨?_, ?_, ?_, ?_⟩ <;>
424 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
425 nearCoordPath, nearFlatSqEdges] <;> ring
426
427theorem hasDerivAt_near_slot8 :
428 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 8 t))
429 ((4 : ℝ) / (8 * Real.sqrt 2)) 1 := by
430 have h := hasDerivAt_near_slot 8 1 (0) (4) (-4) (0) (0) (4)
431 (-1) (10) (-1) (0) (0) (8) near_path8_polys
432 (by norm_num) (by norm_num) (by norm_num)
433 convert h using 1
434 norm_num
435
436private lemma near_path9_polys : ∀ t : ℝ,
437 apexDotNum (nearCoordPath 9 t) = (0) * t ^ 2 + (-8) * t + (16)
438 ∧ apex3NormSqNum (nearCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (4)
439 ∧ apex4NormSqNum (nearCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8)
440 ∧ hingeGramDet (nearCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8) := by
441 intro t
442 refine ⟨?_, ?_, ?_, ?_⟩ <;>
443 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
444 nearCoordPath, nearFlatSqEdges] <;> ring
445
446theorem hasDerivAt_near_slot9 :
447 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath 9 t))
448 ((-8 : ℝ) / (8 * Real.sqrt 2)) 2 := by
449 have h := hasDerivAt_near_slot 9 2 (0) (-8) (16) (0) (0) (4)
450 (0) (0) (8) (0) (0) (8) near_path9_polys
451 (by norm_num) (by norm_num) (by norm_num)
452 convert h using 1
453 norm_num
454
455theorem hasDerivAt_near_coord (k : Fin 10) :
456 HasDerivAt (fun t : ℝ => cosDihedral (nearCoordPath k t))
457 (nearCosKernel k) (nearFlatSqEdges k) := by
458 fin_cases k
459 · exact hasDerivAt_near_slot0
460 · exact hasDerivAt_near_slot1
461 · exact hasDerivAt_near_slot2
462 · exact hasDerivAt_near_slot3
463 · exact hasDerivAt_near_slot4
464 · exact hasDerivAt_near_slot5
465 · exact hasDerivAt_near_slot6
466 · exact hasDerivAt_near_slot7
467 · exact hasDerivAt_near_slot8
468 · exact hasDerivAt_near_slot9
469
470private lemma far_path0_polys : ∀ t : ℝ,
471 apexDotNum (farCoordPath 0 t) = (-2) * t ^ 2 + (0) * t + (2)
472 ∧ apex3NormSqNum (farCoordPath 0 t) = (-4) * t ^ 2 + (16) * t + (-4)
473 ∧ apex4NormSqNum (farCoordPath 0 t) = (-1) * t ^ 2 + (6) * t + (-1)
474 ∧ hingeGramDet (farCoordPath 0 t) = (-1) * t ^ 2 + (10) * t + (-1) := by
475 intro t
476 refine ⟨?_, ?_, ?_, ?_⟩ <;>
477 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
478 farCoordPath, farFlatSqEdges] <;> ring
479
480theorem hasDerivAt_far_slot0 :
481 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 0 t))
482 ((-4 : ℝ) / (8 * Real.sqrt 2)) 1 := by
483 have h := hasDerivAt_far_slot 0 1 (-2) (0) (2) (-4) (16) (-4)
484 (-1) (6) (-1) (-1) (10) (-1) far_path0_polys
485 (by norm_num) (by norm_num) (by norm_num)
486 convert h using 1
487 norm_num
488
489private lemma far_path1_polys : ∀ t : ℝ,
490 apexDotNum (farCoordPath 1 t) = (0) * t ^ 2 + (-4) * t + (12)
491 ∧ apex3NormSqNum (farCoordPath 1 t) = (-2) * t ^ 2 + (12) * t + (-10)
492 ∧ apex4NormSqNum (farCoordPath 1 t) = (-1) * t ^ 2 + (6) * t + (-5)
493 ∧ hingeGramDet (farCoordPath 1 t) = (-1) * t ^ 2 + (6) * t + (-1) := by
494 intro t
495 refine ⟨?_, ?_, ?_, ?_⟩ <;>
496 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
497 farCoordPath, farFlatSqEdges] <;> ring
498
499theorem hasDerivAt_far_slot1 :
500 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 1 t))
501 ((-4 : ℝ) / (8 * Real.sqrt 2)) 3 := by
502 have h := hasDerivAt_far_slot 1 3 (0) (-4) (12) (-2) (12) (-10)
503 (-1) (6) (-5) (-1) (6) (-1) far_path1_polys
504 (by norm_num) (by norm_num) (by norm_num)
505 convert h using 1
506 norm_num
507
508private lemma far_path2_polys : ∀ t : ℝ,
509 apexDotNum (farCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (0)
510 ∧ apex3NormSqNum (farCoordPath 2 t) = (-2) * t ^ 2 + (12) * t + (-2)
511 ∧ apex4NormSqNum (farCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (4)
512 ∧ hingeGramDet (farCoordPath 2 t) = (0) * t ^ 2 + (0) * t + (8) := by
513 intro t
514 refine ⟨?_, ?_, ?_, ?_⟩ <;>
515 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
516 farCoordPath, farFlatSqEdges] <;> ring
517
518theorem hasDerivAt_far_slot2 :
519 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 2 t))
520 (0) 1 := by
521 have h := hasDerivAt_far_slot 2 1 (0) (0) (0) (-2) (12) (-2)
522 (0) (0) (4) (0) (0) (8) far_path2_polys
523 (by norm_num) (by norm_num) (by norm_num)
524 convert h using 1
525 norm_num
526
527private lemma far_path3_polys : ∀ t : ℝ,
528 apexDotNum (farCoordPath 3 t) = (0) * t ^ 2 + (8) * t + (-16)
529 ∧ apex3NormSqNum (farCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (8)
530 ∧ apex4NormSqNum (farCoordPath 3 t) = (-2) * t ^ 2 + (8) * t + (-4)
531 ∧ hingeGramDet (farCoordPath 3 t) = (0) * t ^ 2 + (0) * t + (8) := by
532 intro t
533 refine ⟨?_, ?_, ?_, ?_⟩ <;>
534 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
535 farCoordPath, farFlatSqEdges] <;> ring
536
537theorem hasDerivAt_far_slot3 :
538 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 3 t))
539 ((8 : ℝ) / (8 * Real.sqrt 2)) 2 := by
540 have h := hasDerivAt_far_slot 3 2 (0) (8) (-16) (0) (0) (8)
541 (-2) (8) (-4) (0) (0) (8) far_path3_polys
542 (by norm_num) (by norm_num) (by norm_num)
543 convert h using 1
544 norm_num
545
546private lemma far_path4_polys : ∀ t : ℝ,
547 apexDotNum (farCoordPath 4 t) = (0) * t ^ 2 + (0) * t + (0)
548 ∧ apex3NormSqNum (farCoordPath 4 t) = (-1) * t ^ 2 + (8) * t + (-4)
549 ∧ apex4NormSqNum (farCoordPath 4 t) = (-2) * t ^ 2 + (8) * t + (-4)
550 ∧ hingeGramDet (farCoordPath 4 t) = (-1) * t ^ 2 + (8) * t + (-4) := by
551 intro t
552 refine ⟨?_, ?_, ?_, ?_⟩ <;>
553 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
554 farCoordPath, farFlatSqEdges] <;> ring
555
556theorem hasDerivAt_far_slot4 :
557 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 4 t))
558 (0) 2 := by
559 have h := hasDerivAt_far_slot 4 2 (0) (0) (0) (-1) (8) (-4)
560 (-2) (8) (-4) (-1) (8) (-4) far_path4_polys
561 (by norm_num) (by norm_num) (by norm_num)
562 convert h using 1
563 norm_num
564
565private lemma far_path5_polys : ∀ t : ℝ,
566 apexDotNum (farCoordPath 5 t) = (0) * t ^ 2 + (4) * t + (-8)
567 ∧ apex3NormSqNum (farCoordPath 5 t) = (-3) * t ^ 2 + (12) * t + (-4)
568 ∧ apex4NormSqNum (farCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (4)
569 ∧ hingeGramDet (farCoordPath 5 t) = (0) * t ^ 2 + (0) * t + (8) := by
570 intro t
571 refine ⟨?_, ?_, ?_, ?_⟩ <;>
572 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
573 farCoordPath, farFlatSqEdges] <;> ring
574
575theorem hasDerivAt_far_slot5 :
576 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 5 t))
577 ((4 : ℝ) / (8 * Real.sqrt 2)) 2 := by
578 have h := hasDerivAt_far_slot 5 2 (0) (4) (-8) (-3) (12) (-4)
579 (0) (0) (4) (0) (0) (8) far_path5_polys
580 (by norm_num) (by norm_num) (by norm_num)
581 convert h using 1
582 norm_num
583
584private lemma far_path6_polys : ∀ t : ℝ,
585 apexDotNum (farCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (0)
586 ∧ apex3NormSqNum (farCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (8)
587 ∧ apex4NormSqNum (farCoordPath 6 t) = (-3) * t ^ 2 + (10) * t + (-3)
588 ∧ hingeGramDet (farCoordPath 6 t) = (0) * t ^ 2 + (0) * t + (8) := by
589 intro t
590 refine ⟨?_, ?_, ?_, ?_⟩ <;>
591 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
592 farCoordPath, farFlatSqEdges] <;> ring
593
594theorem hasDerivAt_far_slot6 :
595 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 6 t))
596 (0) 1 := by
597 have h := hasDerivAt_far_slot 6 1 (0) (0) (0) (0) (0) (8)
598 (-3) (10) (-3) (0) (0) (8) far_path6_polys
599 (by norm_num) (by norm_num) (by norm_num)
600 convert h using 1
601 norm_num
602
603private lemma far_path7_polys : ∀ t : ℝ,
604 apexDotNum (farCoordPath 7 t) = (0) * t ^ 2 + (4) * t + (-16)
605 ∧ apex3NormSqNum (farCoordPath 7 t) = (-1) * t ^ 2 + (8) * t + (-8)
606 ∧ apex4NormSqNum (farCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (4)
607 ∧ hingeGramDet (farCoordPath 7 t) = (0) * t ^ 2 + (0) * t + (8) := by
608 intro t
609 refine ⟨?_, ?_, ?_, ?_⟩ <;>
610 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
611 farCoordPath, farFlatSqEdges] <;> ring
612
613theorem hasDerivAt_far_slot7 :
614 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 7 t))
615 ((4 : ℝ) / (8 * Real.sqrt 2)) 4 := by
616 have h := hasDerivAt_far_slot 7 4 (0) (4) (-16) (-1) (8) (-8)
617 (0) (0) (4) (0) (0) (8) far_path7_polys
618 (by norm_num) (by norm_num) (by norm_num)
619 convert h using 1
620 norm_num
621
622private lemma far_path8_polys : ∀ t : ℝ,
623 apexDotNum (farCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (0)
624 ∧ apex3NormSqNum (farCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (8)
625 ∧ apex4NormSqNum (farCoordPath 8 t) = (-1) * t ^ 2 + (6) * t + (-1)
626 ∧ hingeGramDet (farCoordPath 8 t) = (0) * t ^ 2 + (0) * t + (8) := by
627 intro t
628 refine ⟨?_, ?_, ?_, ?_⟩ <;>
629 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
630 farCoordPath, farFlatSqEdges] <;> ring
631
632theorem hasDerivAt_far_slot8 :
633 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 8 t))
634 (0) 1 := by
635 have h := hasDerivAt_far_slot 8 1 (0) (0) (0) (0) (0) (8)
636 (-1) (6) (-1) (0) (0) (8) far_path8_polys
637 (by norm_num) (by norm_num) (by norm_num)
638 convert h using 1
639 norm_num
640
641private lemma far_path9_polys : ∀ t : ℝ,
642 apexDotNum (farCoordPath 9 t) = (0) * t ^ 2 + (-8) * t + (24)
643 ∧ apex3NormSqNum (farCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8)
644 ∧ apex4NormSqNum (farCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (4)
645 ∧ hingeGramDet (farCoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8) := by
646 intro t
647 refine ⟨?_, ?_, ?_, ?_⟩ <;>
648 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
649 farCoordPath, farFlatSqEdges] <;> ring
650
651theorem hasDerivAt_far_slot9 :
652 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath 9 t))
653 ((-8 : ℝ) / (8 * Real.sqrt 2)) 3 := by
654 have h := hasDerivAt_far_slot 9 3 (0) (-8) (24) (0) (0) (8)
655 (0) (0) (4) (0) (0) (8) far_path9_polys
656 (by norm_num) (by norm_num) (by norm_num)
657 convert h using 1
658 norm_num
659
660theorem hasDerivAt_far_coord (k : Fin 10) :
661 HasDerivAt (fun t : ℝ => cosDihedral (farCoordPath k t))
662 (farCosKernel k) (farFlatSqEdges k) := by
663 fin_cases k
664 · exact hasDerivAt_far_slot0
665 · exact hasDerivAt_far_slot1
666 · exact hasDerivAt_far_slot2
667 · exact hasDerivAt_far_slot3
668 · exact hasDerivAt_far_slot4
669 · exact hasDerivAt_far_slot5
670 · exact hasDerivAt_far_slot6
671 · exact hasDerivAt_far_slot7
672 · exact hasDerivAt_far_slot8
673 · exact hasDerivAt_far_slot9
674
675/-! ## §5. Full-star deficit class kernel -/
676
677def chainRight : ℝ := (-1 : ℝ)
678def nearDeficitKernel : Fin 10 → ℝ := nearCosKernel
679def farDeficitKernel : Fin 10 → ℝ := farCosKernel
680
681theorem nearDeficitKernel_eq_chain (k : Fin 10) :
682 nearDeficitKernel k = -chainRight * nearCosKernel k := by
683 simp [nearDeficitKernel, chainRight]
684
685theorem farDeficitKernel_eq_chain (k : Fin 10) :
686 farDeficitKernel k = -chainRight * farCosKernel k := by
687 simp [farDeficitKernel, chainRight]
688
689def starSlotClass : Fin 4 → Fin 10 → Fin 15
690 | 0, 0 => 0
691 | 0, 1 => 6
692 | 0, 2 => 2
693 | 0, 3 => 14
694 | 0, 4 => 5
695 | 0, 5 => 1
696 | 0, 6 => 13
697 | 0, 7 => 3
698 | 0, 8 => 7
699 | 0, 9 => 11
700 | 1, 0 => 0
701 | 1, 1 => 6
702 | 1, 2 => 4
703 | 1, 3 => 14
704 | 1, 4 => 5
705 | 1, 5 => 3
706 | 1, 6 => 13
707 | 1, 7 => 1
708 | 1, 8 => 7
709 | 1, 9 => 9
710 | 2, 0 => 0
711 | 2, 1 => 6
712 | 2, 2 => 7
713 | 2, 3 => 2
714 | 2, 4 => 5
715 | 2, 5 => 8
716 | 2, 6 => 1
717 | 2, 7 => 14
718 | 2, 8 => 3
719 | 2, 9 => 10
720 | 3, 0 => 0
721 | 3, 1 => 6
722 | 3, 2 => 7
723 | 3, 3 => 4
724 | 3, 4 => 5
725 | 3, 5 => 8
726 | 3, 6 => 3
727 | 3, 7 => 14
728 | 3, 8 => 1
729 | 3, 9 => 12
730
731def starLocalDeficitKernel : Fin 4 → Fin 10 → ℝ
732 | 0 | 1 => nearDeficitKernel
733 | 2 | 3 => farDeficitKernel
734
735def assembleStarMember (m : Fin 4) : Fin 15 → ℝ :=
736 fun d => ∑ e : Fin 10,
737 if starSlotClass m e = d then starLocalDeficitKernel m e else 0
738
739def fullStarClassKernelAssembled : Fin 15 → ℝ :=
740 fun d => ∑ m : Fin 4, assembleStarMember m d
741
742def fullStarClassKernel : Fin 15 → ℝ
743 | ⟨0, _⟩ => -(Real.sqrt 2) / 2
744 | ⟨1, _⟩ => Real.sqrt 2 / 2
745 | ⟨2, _⟩ => Real.sqrt 2 / 2
746 | ⟨3, _⟩ => Real.sqrt 2 / 2
747 | ⟨4, _⟩ => Real.sqrt 2 / 2
748 | ⟨5, _⟩ => -(Real.sqrt 2) / 2
749 | ⟨6, _⟩ => -(Real.sqrt 2) / 2
750 | ⟨7, _⟩ => Real.sqrt 2 / 2
751 | ⟨8, _⟩ => Real.sqrt 2 / 2
752 | ⟨9, _⟩ => -(Real.sqrt 2) / 2
753 | ⟨10, _⟩ => -(Real.sqrt 2) / 2
754 | ⟨11, _⟩ => -(Real.sqrt 2) / 2
755 | ⟨12, _⟩ => -(Real.sqrt 2) / 2
756 | ⟨13, _⟩ => Real.sqrt 2 / 2
757 | ⟨14, _⟩ => Real.sqrt 2 / 2
758
759private lemma sum4 (f : Fin 4 → ℝ) :
760 (∑ m : Fin 4, f m) = f 0 + f 1 + f 2 + f 3 := by
761 rw [show (Finset.univ : Finset (Fin 4)) =
762 insert (0 : Fin 4) (insert (1 : Fin 4) (insert (2 : Fin 4)
763 (insert (3 : Fin 4) (∅ : Finset (Fin 4))))) from by decide]
764 simp [Finset.sum_insert]
765 ring
766
767private lemma sum_support_near (f : Fin 10 → ℝ)
768 (hz : ∀ e : Fin 10, e ≠ 4 → e ≠ 6 → e ≠ 7 → e ≠ 8 → e ≠ 9 → f e = 0) :
769 (∑ e : Fin 10, f e) = f 4 + f 6 + f 7 + f 8 + f 9 := by
770 rw [show (Finset.univ : Finset (Fin 10)) =
771 insert (4 : Fin 10) (insert (6 : Fin 10) (insert (7 : Fin 10)
772 (insert (8 : Fin 10) (insert (9 : Fin 10)
773 ({0, 1, 2, 3, 5} : Finset (Fin 10)))))) from by decide]
774 rw [Finset.sum_insert (by decide), Finset.sum_insert (by decide),
775 Finset.sum_insert (by decide), Finset.sum_insert (by decide),
776 Finset.sum_insert (by decide),
777 Finset.sum_eq_zero (fun e he => by
778 fin_cases e <;> simp at he ⊢ <;>
779 exact hz _ (by decide) (by decide) (by decide) (by decide) (by decide))]
780 abel
781
782private lemma sum_support_far (f : Fin 10 → ℝ)
783 (hz : ∀ e : Fin 10, e ≠ 0 → e ≠ 1 → e ≠ 3 → e ≠ 5 → e ≠ 7 → e ≠ 9 →
784 f e = 0) :
785 (∑ e : Fin 10, f e) = f 0 + f 1 + f 3 + f 5 + f 7 + f 9 := by
786 rw [show (Finset.univ : Finset (Fin 10)) =
787 insert (0 : Fin 10) (insert (1 : Fin 10) (insert (3 : Fin 10)
788 (insert (5 : Fin 10) (insert (7 : Fin 10) (insert (9 : Fin 10)
789 ({2, 4, 6, 8} : Finset (Fin 10))))))) from by decide]
790 rw [Finset.sum_insert (by decide), Finset.sum_insert (by decide),
791 Finset.sum_insert (by decide), Finset.sum_insert (by decide),
792 Finset.sum_insert (by decide), Finset.sum_insert (by decide),
793 Finset.sum_eq_zero (fun e he => by
794 fin_cases e <;> simp at he ⊢ <;>
795 exact hz _ (by decide) (by decide) (by decide) (by decide)
796 (by decide) (by decide))]
797 abel
798
799private lemma near_kernel_zero_off (e : Fin 10)
800 (h4 : e ≠ 4) (h6 : e ≠ 6) (h7 : e ≠ 7) (h8 : e ≠ 8) (h9 : e ≠ 9) :
801 nearDeficitKernel e = 0 := by
802 fin_cases e <;> first | rfl | contradiction
803
804private lemma far_kernel_zero_off (e : Fin 10)
805 (h0 : e ≠ 0) (h1 : e ≠ 1) (h3 : e ≠ 3) (h5 : e ≠ 5) (h7 : e ≠ 7)
806 (h9 : e ≠ 9) :
807 farDeficitKernel e = 0 := by
808 fin_cases e <;> first | rfl | contradiction
809
810private lemma member0_eval (d : Fin 15) :
811 assembleStarMember 0 d =
812 (if d = 5 then (-4 : ℝ) / (8 * Real.sqrt 2) else 0) +
813 (if d = 13 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
814 (if d = 3 then (8 : ℝ) / (8 * Real.sqrt 2) else 0) +
815 (if d = 7 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
816 (if d = 11 then (-8 : ℝ) / (8 * Real.sqrt 2) else 0) := by
817 simp only [assembleStarMember, starLocalDeficitKernel]
818 rw [sum_support_near (fun e =>
819 if starSlotClass 0 e = d then nearDeficitKernel e else 0)
820 (fun e h4 h6 h7 h8 h9 => by simp [near_kernel_zero_off e h4 h6 h7 h8 h9])]
821 simp only [starSlotClass, nearDeficitKernel, nearCosKernel]
822 aesop
823
824private lemma member1_eval (d : Fin 15) :
825 assembleStarMember 1 d =
826 (if d = 5 then (-4 : ℝ) / (8 * Real.sqrt 2) else 0) +
827 (if d = 13 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
828 (if d = 1 then (8 : ℝ) / (8 * Real.sqrt 2) else 0) +
829 (if d = 7 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
830 (if d = 9 then (-8 : ℝ) / (8 * Real.sqrt 2) else 0) := by
831 simp only [assembleStarMember, starLocalDeficitKernel]
832 rw [sum_support_near (fun e =>
833 if starSlotClass 1 e = d then nearDeficitKernel e else 0)
834 (fun e h4 h6 h7 h8 h9 => by simp [near_kernel_zero_off e h4 h6 h7 h8 h9])]
835 simp only [starSlotClass, nearDeficitKernel, nearCosKernel]
836 aesop
837
838private lemma member2_eval (d : Fin 15) :
839 assembleStarMember 2 d =
840 (if d = 0 then (-4 : ℝ) / (8 * Real.sqrt 2) else 0) +
841 (if d = 6 then (-4 : ℝ) / (8 * Real.sqrt 2) else 0) +
842 (if d = 2 then (8 : ℝ) / (8 * Real.sqrt 2) else 0) +
843 (if d = 8 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
844 (if d = 14 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
845 (if d = 10 then (-8 : ℝ) / (8 * Real.sqrt 2) else 0) := by
846 simp only [assembleStarMember, starLocalDeficitKernel]
847 rw [sum_support_far (fun e =>
848 if starSlotClass 2 e = d then farDeficitKernel e else 0)
849 (fun e h0 h1 h3 h5 h7 h9 => by
850 simp [far_kernel_zero_off e h0 h1 h3 h5 h7 h9])]
851 simp only [starSlotClass, farDeficitKernel, farCosKernel]
852 aesop
853
854private lemma member3_eval (d : Fin 15) :
855 assembleStarMember 3 d =
856 (if d = 0 then (-4 : ℝ) / (8 * Real.sqrt 2) else 0) +
857 (if d = 6 then (-4 : ℝ) / (8 * Real.sqrt 2) else 0) +
858 (if d = 4 then (8 : ℝ) / (8 * Real.sqrt 2) else 0) +
859 (if d = 8 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
860 (if d = 14 then (4 : ℝ) / (8 * Real.sqrt 2) else 0) +
861 (if d = 12 then (-8 : ℝ) / (8 * Real.sqrt 2) else 0) := by
862 simp only [assembleStarMember, starLocalDeficitKernel]
863 rw [sum_support_far (fun e =>
864 if starSlotClass 3 e = d then farDeficitKernel e else 0)
865 (fun e h0 h1 h3 h5 h7 h9 => by
866 simp [far_kernel_zero_off e h0 h1 h3 h5 h7 h9])]
867 simp only [starSlotClass, farDeficitKernel, farCosKernel]
868 aesop
869
870
871theorem fullStarClassKernel_eq (d : Fin 15) :
872 fullStarClassKernelAssembled d = fullStarClassKernel d := by
873 simp only [fullStarClassKernelAssembled]
874 rw [sum4, member0_eval, member1_eval, member2_eval, member3_eval]
875 have hs : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
876 have hs2 : Real.sqrt 2 * Real.sqrt 2 = 2 :=
877 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 2)
878 fin_cases d <;> simp [fullStarClassKernel] <;> field_simp <;>
879 ring_nf <;> simp only [hs2, pow_two] <;> try ring
880
881theorem fullStarClassKernel_values :
882 fullStarClassKernel 0 = -(Real.sqrt 2) / 2 ∧
883 fullStarClassKernel 1 = Real.sqrt 2 / 2 ∧
884 fullStarClassKernel 5 = -(Real.sqrt 2) / 2 ∧
885 fullStarClassKernel 14 = Real.sqrt 2 / 2 :=
886 ⟨rfl, rfl, rfl, rfl⟩
887
888/-! ## §6. Gates -/
889
890theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 0 ≠ 0 := by
891 have hs : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
892 simp [fullStarClassKernel, hs]
893
894def swap12Mask (m : ℕ) : ℕ :=
895 (if Nat.testBit m 0 then 1 else 0) +
896 (if Nat.testBit m 1 then 4 else 0) +
897 (if Nat.testBit m 2 then 2 else 0) +
898 (if Nat.testBit m 3 then 8 else 0)
899
900theorem swap12Mask_bounds (d : Fin 15) :
901 0 < swap12Mask (maskOf d) ∧ swap12Mask (maskOf d) ≤ 15 := by
902 fin_cases d <;> decide
903
904def swap12Class (d : Fin 15) : Fin 15 :=
905 ⟨swap12Mask (maskOf d) - 1, by
906 have h := swap12Mask_bounds d
907 omega⟩
908
909theorem fullStarClassKernel_swap12 (d : Fin 15) :
910 fullStarClassKernel (swap12Class d) = fullStarClassKernel d := by
911 fin_cases d <;> rfl
912
913def fullStarDirectional (v : Fin 15 → ℝ) : ℝ :=
914 ∑ d : Fin 15, v d * fullStarClassKernel d
915
916private lemma sum15_all (f : Fin 15 → ℝ) :
917 (∑ d : Fin 15, f d) =
918 f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8 + f 9 +
919 f 10 + f 11 + f 12 + f 13 + f 14 := by
920 rw [show (Finset.univ : Finset (Fin 15)) =
921 insert (0 : Fin 15) (insert (1 : Fin 15) (insert (2 : Fin 15)
922 (insert (3 : Fin 15) (insert (4 : Fin 15) (insert (5 : Fin 15)
923 (insert (6 : Fin 15) (insert (7 : Fin 15) (insert (8 : Fin 15)
924 (insert (9 : Fin 15) (insert (10 : Fin 15) (insert (11 : Fin 15)
925 (insert (12 : Fin 15) (insert (13 : Fin 15) (insert (14 : Fin 15)
926 (∅ : Finset (Fin 15)))))))))))))))) from by decide]
927 simp [Finset.sum_insert]
928 ring
929
930theorem fullStar_uniformScale_decoy :
931 fullStarDirectional (fun _ => (1 : ℝ)) = Real.sqrt 2 / 2 := by
932 simp only [fullStarDirectional]
933 rw [sum15_all]
934 have hs : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
935 simp [fullStarClassKernel]
936 field_simp
937 ring
938
939theorem fullStar_homothety_stationary :
940 fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
941 simp only [fullStarDirectional]
942 rw [sum15_all]
943 have hs : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
944 have w0 : classWeightNat 0 = 1 := by decide
945 have w1 : classWeightNat 1 = 1 := by decide
946 have w2 : classWeightNat 2 = 2 := by decide
947 have w3 : classWeightNat 3 = 1 := by decide
948 have w4 : classWeightNat 4 = 2 := by decide
949 have w5 : classWeightNat 5 = 2 := by decide
950 have w6 : classWeightNat 6 = 3 := by decide
951 have w7 : classWeightNat 7 = 1 := by decide
952 have w8 : classWeightNat 8 = 2 := by decide
953 have w9 : classWeightNat 9 = 2 := by decide
954 have w10 : classWeightNat 10 = 3 := by decide
955 have w11 : classWeightNat 11 = 2 := by decide
956 have w12 : classWeightNat 12 = 3 := by decide
957 have w13 : classWeightNat 13 = 3 := by decide
958 have w14 : classWeightNat 14 = 4 := by decide
959 simp [fullStarClassKernel, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9,
960 w10, w11, w12, w13, w14]
961 field_simp
962 ring
963
964/-! ## §7. Status -/
965
966structure Hinge4DStarKernel12Status where
967 starEnumerationClosed : Bool
968 flatnessGateClosed : Bool
969 fullStarClassKernelClosed : Bool
970 type21ComplementOrbitOpen : Bool
971 otherHingeOrbitsOpen : Bool
972 flatHessianAssemblyOpen : Bool
973 convergesEH4d : Bool
974 gapActionRecovery : Bool
975
976def hinge4DStarKernel12Status : Hinge4DStarKernel12Status where
977 starEnumerationClosed := true
978 flatnessGateClosed := true
979 fullStarClassKernelClosed := true
980 type21ComplementOrbitOpen := true
981 otherHingeOrbitsOpen := true
982 flatHessianAssemblyOpen := true
983 convergesEH4d := false
984 gapActionRecovery := false
985
986theorem hinge4DStarKernel12Status_flags :
987 hinge4DStarKernel12Status.starEnumerationClosed = true ∧
988 hinge4DStarKernel12Status.flatnessGateClosed = true ∧
989 hinge4DStarKernel12Status.fullStarClassKernelClosed = true ∧
990 hinge4DStarKernel12Status.type21ComplementOrbitOpen = true ∧
991 hinge4DStarKernel12Status.otherHingeOrbitsOpen = true ∧
992 hinge4DStarKernel12Status.flatHessianAssemblyOpen = true ∧
993 hinge4DStarKernel12Status.convergesEH4d = false ∧
994 hinge4DStarKernel12Status.gapActionRecovery = false := by
995 decide
996
997end
998
999end ReggeHinge4DStarKernel12
1000end Analysis
1001end Gravity
1002end IndisputableMonolith
1003