IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOrigins4D
IndisputableMonolith/Gravity/Analysis/ReggeBlochStarEdgeOrigins4D.lean · 572 lines · 25 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
3import IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D
4import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
5import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
6import IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D
7import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
8
9/-!
10# Position-resolved star edge origins (fold repair)
11
12Typed blocker `fold_position_resolved_star_phase` (2026-07-21).
13Seed star edges carry lattice origins; covering perms transport both class
14index and origin into the deficit phase for non-`t11` orbits.
15
16Python gate: `scripts/qg/regge_4d_fold_position_resolved_20260721.py`
17(banked gauges → 0; TT plus=cross=-1/4 on `symbolDir`; t11 untouched).
18
19Does **not** flip `gap_action_recovery`. Forbidden: base0 half-repair.
20-/
21
22namespace IndisputableMonolith
23namespace Gravity
24namespace Analysis
25namespace ReggeBlochStarEdgeOrigins4D
26
27open BigOperators
28open ReggeEdgeStencil4D
29open ReggeBlochFold4D
30open ReggeBlochOrbitTransport4D
31open ReggeBlochTransportedAllOrbit4D
32open ReggeBlochAllOrbitSymbol4D (isOrbit phaseScaleDir)
33open ReggeHinge4DOrbitClassification
34
35noncomputable section
36
37abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
38abbrev Wave4 := Fin 4 → ℝ
39
40/-- One seed-frame star edge contribution: class index, weight, origin. -/
41structure SeedEdgeContrib where
42 cls : Fin 15
43 weight : ℝ
44 origin : Wave4
45
46/-- Seed contributions for orbit seed `t12`. -/
47def seedEdgeContribs_t12 : List SeedEdgeContrib :=
48 [
49 {
50 cls := (5 : Fin 15)
51 weight := ((-1 : ℤ) : ℝ) * Real.sqrt 2 / 4
52 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
53 },
54 {
55 cls := (13 : Fin 15)
56 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
57 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
58 },
59 {
60 cls := (3 : Fin 15)
61 weight := ((2 : ℤ) : ℝ) * Real.sqrt 2 / 4
62 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
63 },
64 {
65 cls := (7 : Fin 15)
66 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
67 origin := fun i => ((![1, 1, 1, 0] : Fin 4 → ℤ) i : ℝ)
68 },
69 {
70 cls := (11 : Fin 15)
71 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 2 / 4
72 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
73 },
74 {
75 cls := (5 : Fin 15)
76 weight := ((-1 : ℤ) : ℝ) * Real.sqrt 2 / 4
77 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
78 },
79 {
80 cls := (13 : Fin 15)
81 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
82 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
83 },
84 {
85 cls := (1 : Fin 15)
86 weight := ((2 : ℤ) : ℝ) * Real.sqrt 2 / 4
87 origin := fun i => ((![1, 0, 1, 0] : Fin 4 → ℤ) i : ℝ)
88 },
89 {
90 cls := (7 : Fin 15)
91 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
92 origin := fun i => ((![1, 1, 1, 0] : Fin 4 → ℤ) i : ℝ)
93 },
94 {
95 cls := (9 : Fin 15)
96 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 2 / 4
97 origin := fun i => ((![1, 0, 1, 0] : Fin 4 → ℤ) i : ℝ)
98 },
99 {
100 cls := (0 : Fin 15)
101 weight := ((-1 : ℤ) : ℝ) * Real.sqrt 2 / 4
102 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
103 },
104 {
105 cls := (6 : Fin 15)
106 weight := ((-1 : ℤ) : ℝ) * Real.sqrt 2 / 4
107 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
108 },
109 {
110 cls := (2 : Fin 15)
111 weight := ((2 : ℤ) : ℝ) * Real.sqrt 2 / 4
112 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
113 },
114 {
115 cls := (8 : Fin 15)
116 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
117 origin := fun i => ((![0, 0, 0, -1] : Fin 4 → ℤ) i : ℝ)
118 },
119 {
120 cls := (14 : Fin 15)
121 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
122 origin := fun i => ((![0, 0, 0, -1] : Fin 4 → ℤ) i : ℝ)
123 },
124 {
125 cls := (10 : Fin 15)
126 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 2 / 4
127 origin := fun i => ((![0, 0, 0, -1] : Fin 4 → ℤ) i : ℝ)
128 },
129 {
130 cls := (0 : Fin 15)
131 weight := ((-1 : ℤ) : ℝ) * Real.sqrt 2 / 4
132 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
133 },
134 {
135 cls := (6 : Fin 15)
136 weight := ((-1 : ℤ) : ℝ) * Real.sqrt 2 / 4
137 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
138 },
139 {
140 cls := (4 : Fin 15)
141 weight := ((2 : ℤ) : ℝ) * Real.sqrt 2 / 4
142 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
143 },
144 {
145 cls := (8 : Fin 15)
146 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
147 origin := fun i => ((![0, 0, 0, -1] : Fin 4 → ℤ) i : ℝ)
148 },
149 {
150 cls := (14 : Fin 15)
151 weight := ((1 : ℤ) : ℝ) * Real.sqrt 2 / 4
152 origin := fun i => ((![0, 0, 0, -1] : Fin 4 → ℤ) i : ℝ)
153 },
154 {
155 cls := (12 : Fin 15)
156 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 2 / 4
157 origin := fun i => ((![0, 0, 0, -1] : Fin 4 → ℤ) i : ℝ)
158 }
159 ]
160
161theorem seedEdgeContribs_t12_length :
162 seedEdgeContribs_t12.length = 22 := rfl
163
164/-- Seed contributions for orbit seed `t13`. -/
165def seedEdgeContribs_t13 : List SeedEdgeContrib :=
166 [
167 {
168 cls := (13 : Fin 15)
169 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 3 / 12
170 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
171 },
172 {
173 cls := (5 : Fin 15)
174 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
175 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
176 },
177 {
178 cls := (11 : Fin 15)
179 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
180 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
181 },
182 {
183 cls := (3 : Fin 15)
184 weight := ((-6 : ℤ) : ℝ) * Real.sqrt 3 / 12
185 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
186 },
187 {
188 cls := (13 : Fin 15)
189 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 3 / 12
190 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
191 },
192 {
193 cls := (9 : Fin 15)
194 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
195 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
196 },
197 {
198 cls := (11 : Fin 15)
199 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
200 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
201 },
202 {
203 cls := (7 : Fin 15)
204 weight := ((-6 : ℤ) : ℝ) * Real.sqrt 3 / 12
205 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
206 },
207 {
208 cls := (13 : Fin 15)
209 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 3 / 12
210 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
211 },
212 {
213 cls := (5 : Fin 15)
214 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
215 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
216 },
217 {
218 cls := (9 : Fin 15)
219 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
220 origin := fun i => ((![1, 0, 1, 0] : Fin 4 → ℤ) i : ℝ)
221 },
222 {
223 cls := (1 : Fin 15)
224 weight := ((-6 : ℤ) : ℝ) * Real.sqrt 3 / 12
225 origin := fun i => ((![1, 0, 1, 0] : Fin 4 → ℤ) i : ℝ)
226 },
227 {
228 cls := (13 : Fin 15)
229 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 3 / 12
230 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
231 },
232 {
233 cls := (11 : Fin 15)
234 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
235 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
236 },
237 {
238 cls := (9 : Fin 15)
239 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
240 origin := fun i => ((![1, 0, 1, 0] : Fin 4 → ℤ) i : ℝ)
241 },
242 {
243 cls := (7 : Fin 15)
244 weight := ((-6 : ℤ) : ℝ) * Real.sqrt 3 / 12
245 origin := fun i => ((![1, 0, 1, 0] : Fin 4 → ℤ) i : ℝ)
246 },
247 {
248 cls := (13 : Fin 15)
249 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 3 / 12
250 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
251 },
252 {
253 cls := (9 : Fin 15)
254 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
255 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
256 },
257 {
258 cls := (5 : Fin 15)
259 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
260 origin := fun i => ((![1, 0, 0, 1] : Fin 4 → ℤ) i : ℝ)
261 },
262 {
263 cls := (1 : Fin 15)
264 weight := ((-6 : ℤ) : ℝ) * Real.sqrt 3 / 12
265 origin := fun i => ((![1, 0, 0, 1] : Fin 4 → ℤ) i : ℝ)
266 },
267 {
268 cls := (13 : Fin 15)
269 weight := ((-2 : ℤ) : ℝ) * Real.sqrt 3 / 12
270 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
271 },
272 {
273 cls := (11 : Fin 15)
274 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
275 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
276 },
277 {
278 cls := (5 : Fin 15)
279 weight := ((3 : ℤ) : ℝ) * Real.sqrt 3 / 12
280 origin := fun i => ((![1, 0, 0, 1] : Fin 4 → ℤ) i : ℝ)
281 },
282 {
283 cls := (3 : Fin 15)
284 weight := ((-6 : ℤ) : ℝ) * Real.sqrt 3 / 12
285 origin := fun i => ((![1, 0, 0, 1] : Fin 4 → ℤ) i : ℝ)
286 }
287 ]
288
289theorem seedEdgeContribs_t13_length :
290 seedEdgeContribs_t13.length = 24 := rfl
291
292/-- Seed contributions for orbit seed `t22`. -/
293def seedEdgeContribs_t22 : List SeedEdgeContrib :=
294 [
295 {
296 cls := (2 : Fin 15)
297 weight := ((-1 : ℤ) : ℝ) / 4
298 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
299 },
300 {
301 cls := (14 : Fin 15)
302 weight := ((-1 : ℤ) : ℝ) / 4
303 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
304 },
305 {
306 cls := (6 : Fin 15)
307 weight := ((2 : ℤ) : ℝ) / 4
308 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
309 },
310 {
311 cls := (11 : Fin 15)
312 weight := ((-1 : ℤ) : ℝ) / 4
313 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
314 },
315 {
316 cls := (1 : Fin 15)
317 weight := ((2 : ℤ) : ℝ) / 4
318 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
319 },
320 {
321 cls := (3 : Fin 15)
322 weight := ((2 : ℤ) : ℝ) / 4
323 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
324 },
325 {
326 cls := (13 : Fin 15)
327 weight := ((2 : ℤ) : ℝ) / 4
328 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
329 },
330 {
331 cls := (5 : Fin 15)
332 weight := ((-4 : ℤ) : ℝ) / 4
333 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
334 },
335 {
336 cls := (2 : Fin 15)
337 weight := ((-1 : ℤ) : ℝ) / 4
338 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
339 },
340 {
341 cls := (14 : Fin 15)
342 weight := ((-1 : ℤ) : ℝ) / 4
343 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
344 },
345 {
346 cls := (10 : Fin 15)
347 weight := ((2 : ℤ) : ℝ) / 4
348 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
349 },
350 {
351 cls := (11 : Fin 15)
352 weight := ((-1 : ℤ) : ℝ) / 4
353 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
354 },
355 {
356 cls := (1 : Fin 15)
357 weight := ((2 : ℤ) : ℝ) / 4
358 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
359 },
360 {
361 cls := (7 : Fin 15)
362 weight := ((2 : ℤ) : ℝ) / 4
363 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
364 },
365 {
366 cls := (13 : Fin 15)
367 weight := ((2 : ℤ) : ℝ) / 4
368 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
369 },
370 {
371 cls := (9 : Fin 15)
372 weight := ((-4 : ℤ) : ℝ) / 4
373 origin := fun i => ((![1, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
374 },
375 {
376 cls := (2 : Fin 15)
377 weight := ((-1 : ℤ) : ℝ) / 4
378 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
379 },
380 {
381 cls := (14 : Fin 15)
382 weight := ((-1 : ℤ) : ℝ) / 4
383 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
384 },
385 {
386 cls := (6 : Fin 15)
387 weight := ((2 : ℤ) : ℝ) / 4
388 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
389 },
390 {
391 cls := (11 : Fin 15)
392 weight := ((-1 : ℤ) : ℝ) / 4
393 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
394 },
395 {
396 cls := (0 : Fin 15)
397 weight := ((2 : ℤ) : ℝ) / 4
398 origin := fun i => ((![0, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
399 },
400 {
401 cls := (3 : Fin 15)
402 weight := ((2 : ℤ) : ℝ) / 4
403 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
404 },
405 {
406 cls := (12 : Fin 15)
407 weight := ((2 : ℤ) : ℝ) / 4
408 origin := fun i => ((![0, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
409 },
410 {
411 cls := (4 : Fin 15)
412 weight := ((-4 : ℤ) : ℝ) / 4
413 origin := fun i => ((![0, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
414 },
415 {
416 cls := (2 : Fin 15)
417 weight := ((-1 : ℤ) : ℝ) / 4
418 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
419 },
420 {
421 cls := (14 : Fin 15)
422 weight := ((-1 : ℤ) : ℝ) / 4
423 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
424 },
425 {
426 cls := (10 : Fin 15)
427 weight := ((2 : ℤ) : ℝ) / 4
428 origin := fun i => ((![0, 0, 0, 0] : Fin 4 → ℤ) i : ℝ)
429 },
430 {
431 cls := (11 : Fin 15)
432 weight := ((-1 : ℤ) : ℝ) / 4
433 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
434 },
435 {
436 cls := (0 : Fin 15)
437 weight := ((2 : ℤ) : ℝ) / 4
438 origin := fun i => ((![0, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
439 },
440 {
441 cls := (7 : Fin 15)
442 weight := ((2 : ℤ) : ℝ) / 4
443 origin := fun i => ((![1, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
444 },
445 {
446 cls := (12 : Fin 15)
447 weight := ((2 : ℤ) : ℝ) / 4
448 origin := fun i => ((![0, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
449 },
450 {
451 cls := (8 : Fin 15)
452 weight := ((-4 : ℤ) : ℝ) / 4
453 origin := fun i => ((![0, 1, 0, 0] : Fin 4 → ℤ) i : ℝ)
454 }
455 ]
456
457theorem seedEdgeContribs_t22_length :
458 seedEdgeContribs_t22.length = 32 := rfl
459
460/-- Identity-transport complements (Lean `kernel21 = kernel12`, `kernel31 = kernel13`). -/
461def seedEdgeContribs_t21 : List SeedEdgeContrib := seedEdgeContribs_t12
462def seedEdgeContribs_t31 : List SeedEdgeContrib := seedEdgeContribs_t13
463
464def seedEdgeContribs : HingeOrbitType → List SeedEdgeContrib
465 | .t11 => []
466 | .t12 => seedEdgeContribs_t12
467 | .t21 => seedEdgeContribs_t21
468 | .t13 => seedEdgeContribs_t13
469 | .t31 => seedEdgeContribs_t31
470 | .t22 => seedEdgeContribs_t22
471
472/-- Transport a seed-frame origin by covering perm `p`. -/
473def transportOrigin (p : Fin 24) (off : Wave4) : Wave4 :=
474 fun i => ∑ j : Fin 4, if coordPermOf p j = i then off j else 0
475
476/-- One contribution evaluated at a transported slot. -/
477def edgeContribPhased (p : Fin 24) (base : Wave4) (H : Mat4) (m : Wave4)
478 (c : SeedEdgeContrib) : ℝ :=
479 c.weight *
480 planeWaveClassPert H m
481 (fun i => base i + transportOrigin p c.origin i) (permClass p c.cls)
482
483/-- Position-resolved deficit phased class-dot from seed edge contributions. -/
484def phasedDeficitDotEdgeOrigins (ty : HingeOrbitType) (H : Mat4)
485 (m : Wave4) (s : Fin 24) (t : Fin 10) : ℝ :=
486 ((seedEdgeContribs ty).map
487 (edgeContribPhased (orbitCoveringPerm ty s t) (hingeBase s t) H m)).sum
488
489private lemma list_sum_map_smul_planeWave (c : ℝ) (H : Mat4) (m : Wave4)
490 (p : Fin 24) (base : Wave4) (cs : List SeedEdgeContrib) :
491 (cs.map (fun e =>
492 e.weight *
493 planeWaveClassPert (c • H) m
494 (fun i => base i + transportOrigin p e.origin i)
495 (permClass p e.cls))).sum =
496 c *
497 (cs.map (fun e =>
498 e.weight *
499 planeWaveClassPert H m
500 (fun i => base i + transportOrigin p e.origin i)
501 (permClass p e.cls))).sum := by
502 induction cs with
503 | nil => simp
504 | cons hd tl ih =>
505 simp only [List.map_cons, List.sum_cons]
506 rw [planeWaveClassPert_smul, ih]
507 ring
508
509theorem phasedDeficitDotEdgeOrigins_smul (c : ℝ) (ty : HingeOrbitType)
510 (H : Mat4) (m : Wave4) (s : Fin 24) (t : Fin 10) :
511 phasedDeficitDotEdgeOrigins ty (c • H) m s t =
512 c * phasedDeficitDotEdgeOrigins ty H m s t := by
513 unfold phasedDeficitDotEdgeOrigins edgeContribPhased
514 exact list_sum_map_smul_planeWave c H m (orbitCoveringPerm ty s t)
515 (hingeBase s t) (seedEdgeContribs ty)
516
517/-- Two-jet phase² sum for m² trunc: `Σ w_e c_d phase(origin_e, d)²`. -/
518def edgeContribPhase2 (p : Fin 24) (base : Wave4) (H : Mat4) (dir : Wave4)
519 (c : SeedEdgeContrib) : ℝ :=
520 c.weight * classCoeff H (permClass p c.cls) *
521 (phaseScaleDir dir (fun i => base i + transportOrigin p c.origin i)
522 (permClass p c.cls)) ^ 2
523
524def slotOrbitDeficitPhase2EdgeOrigins (ty : HingeOrbitType) (H : Mat4)
525 (dir : Wave4) (s : Fin 24) (t : Fin 10) : ℝ :=
526 ((seedEdgeContribs ty).map
527 (edgeContribPhase2 (orbitCoveringPerm ty s t) (hingeBase s t) H dir)).sum
528
529/-- Position-resolved m² trunc slot coefficient for non-`t11` orbits. -/
530def m2OrbitSlotCoeffEdgeOrigins (ty : HingeOrbitType) (H : Mat4)
531 (dir : Wave4) (s : Fin 24) (t : Fin 10) : ℝ :=
532 if isOrbit ty s t then
533 (∑ d : Fin 15, slotOrbitAreaCov ty s t d * classCoeff H d) *
534 (-(1 / 2 : ℝ) * slotOrbitDeficitPhase2EdgeOrigins ty H dir s t)
535 else 0
536
537def m2OrbitMomentEdgeOrigins (ty : HingeOrbitType) (H : Mat4)
538 (dir : Wave4) : ℝ :=
539 ∑ s : Fin 24, ∑ t : Fin 10, m2OrbitSlotCoeffEdgeOrigins ty H dir s t
540
541/-- Mixed fold: t11 keeps legacy transported m²; others use edge origins. -/
542def m2AllOrbitMomentDistinctHingeEdgeOrigins (H : Mat4) (dir : Wave4) : ℝ :=
543 (orbitStarSize .t11)⁻¹ * m2TransportedOrbitMoment .t11 H dir +
544 (orbitStarSize .t12)⁻¹ * m2OrbitMomentEdgeOrigins .t12 H dir +
545 (orbitStarSize .t21)⁻¹ * m2OrbitMomentEdgeOrigins .t21 H dir +
546 (orbitStarSize .t13)⁻¹ * m2OrbitMomentEdgeOrigins .t13 H dir +
547 (orbitStarSize .t31)⁻¹ * m2OrbitMomentEdgeOrigins .t31 H dir +
548 (orbitStarSize .t22)⁻¹ * m2OrbitMomentEdgeOrigins .t22 H dir
549
550structure StarEdgeOriginsStatus where
551 tablesLanded : Bool
552 gapActionRecovery : Bool
553 base0Forbidden : Bool
554
555def starEdgeOriginsStatus : StarEdgeOriginsStatus where
556 tablesLanded := true
557 gapActionRecovery := false
558 base0Forbidden := true
559
560theorem starEdgeOriginsStatus_flags :
561 starEdgeOriginsStatus.tablesLanded = true ∧
562 starEdgeOriginsStatus.gapActionRecovery = false ∧
563 starEdgeOriginsStatus.base0Forbidden = true := by
564 decide
565
566end
567
568end ReggeBlochStarEdgeOrigins4D
569end Analysis
570end Gravity
571end IndisputableMonolith
572