IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
IndisputableMonolith/Gravity/Analysis/ReggeBlochTransportedAllOrbit4D.lean · 578 lines · 65 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
3import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
4import IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D
5import IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D
6import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
7import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12
8import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13
9import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22
10import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
11
12/-!
13# Transported all-orbit 4D Bloch fold
14
15Continuum-facing multi-orbit fold: each slot transports its orbit's seed
16area covector and star deficit kernel by `orbitCoveringPerm` (first `S₄`
17cover of `orbitRep ty → (diffMaskA, diffMaskB)`).
18
19**Do not** use `transportPermOfDiff` for non-`(1,1)` orbits
20(lesson `L-p1-factorized-vs-transported-fold`; MEASURED all-orbit m²
21along `symbolDir` on `axisTTPlus` is `-5/2` raw, not the factorized `0`).
22
23## Status
24
25* THEOREM: definitions; covering-based transport; `(1,1)` recovery of
26 `blochFold11` / `slotAreaCov` / `slotDeficitKer` (uniform covering
27 pushforward, proved via `slotOrbitAreaCov_t11`); m² `(1,1)` slice
28 equals `ReggeBlochM2Symbol4D.m2Symbol`; pushforward reindex
29 identities; quadratic homogeneity (`blochFoldAll_smul`); raw
30 all-orbit m² eval `-5/2` on `axisTTPlus`/`symbolDir` (sibling
31 M2Eval module); distinct-hinge fold weight `1/r_τ` with
32 `orbitStarSize` and axis/gauge m² evaluations (sibling M2Eval).
33* OPEN: all-orbit m² Tendsto; continuum EH isotropy (residual 3D-style
34 `2/N⁴` cell-sum dictionary still required for EH Tendsto).
35* Does **not** flip `gap_action_recovery`.
36-/
37
38namespace IndisputableMonolith
39namespace Gravity
40namespace Analysis
41namespace ReggeBlochTransportedAllOrbit4D
42
43open BigOperators
44open ReggeEdgeStencil4D
45open ReggeHinge4DOrbitClassification
46open ReggeBlochFold4D
47open ReggeBlochM2Symbol4D
48open ReggeBlochAllOrbitSymbol4D (isOrbit isOrbit_t11_iff_isT11 phaseScaleDir)
49open ReggeBlochOrbitTransport4D
50open ReggeFlat4DHessianAssembly
51open EdgeTTDecomposition4D
52
53noncomputable section
54
55abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
56
57/-! ## §1. Seed kernels and pushforwards -/
58
59/-- Seed star deficit kernel for each orbit type (assembly commitment). -/
60def orbitSeedKernel : HingeOrbitType → (Fin 15 → ℝ)
61 | .t11 => ReggeHinge4DStarKernel.fullStarClassKernel
62 | .t12 => ReggeHinge4DStarKernel12.fullStarClassKernel
63 | .t21 => kernel21
64 | .t13 => ReggeHinge4DStarKernel13.fullStarClassKernel
65 | .t31 => kernel31
66 | .t22 => ReggeHinge4DStarKernel22.fullStarClassKernel
67
68theorem orbitSeedKernel_eq_assembly (ty : HingeOrbitType) :
69 orbitSeedKernel ty = orbitDeficitKernel ty := by
70 cases ty <;> rfl
71
72/-- Pushforward of a class covector by a covering permutation. -/
73def pushforwardClass (v : Fin 15 → ℝ) (p : Fin 24) : Fin 15 → ℝ :=
74 fun d => ∑ d0 : Fin 15, if permClass p d0 = d then v d0 else 0
75
76def transportedOrbitDeficit (ty : HingeOrbitType) (p : Fin 24) : Fin 15 → ℝ :=
77 pushforwardClass (orbitSeedKernel ty) p
78
79def transportedOrbitArea (ty : HingeOrbitType) (p : Fin 24) : Fin 15 → ℝ :=
80 pushforwardClass (orbitAreaCov ty) p
81
82def slotOrbitDeficitKer (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) :
83 Fin 15 → ℝ :=
84 transportedOrbitDeficit ty (orbitCoveringPerm ty s t)
85
86/-- Uniform covering pushforward of the assembly area covector (all orbits). -/
87def slotOrbitAreaCov (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) :
88 Fin 15 → ℝ :=
89 transportedOrbitArea ty (orbitCoveringPerm ty s t)
90
91def transportedOrbitSlotTerm (ty : HingeOrbitType) (H : Mat4)
92 (m : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) : ℝ :=
93 if isOrbit ty s t then
94 phasedClassDot (slotOrbitAreaCov ty s t) H m (hingeBase s t) *
95 phasedClassDot (slotOrbitDeficitKer ty s t) H m (hingeBase s t)
96 else 0
97
98def blochFoldOrbit (ty : HingeOrbitType) (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
99 ∑ s : Fin 24, ∑ t : Fin 10, transportedOrbitSlotTerm ty H m s t
100
101/-- Full transported multi-orbit Bloch fold (incidence × full-star). -/
102def blochFoldAll (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
103 ∑ ty : HingeOrbitType, blochFoldOrbit ty H m
104
105/-! ## §1b. Distinct-hinge fold (geometric weight `1/r_τ`) -/
106
107/-- Geometric star size `r_τ` per orbit type. Theorem-level in the star
108modules / paper table: `(1,1)→6`, `(1,2)→4`, `(2,1)→4`, `(1,3)→6`,
109`(3,1)→6`, `(2,2)→4`. -/
110def orbitStarSize : HingeOrbitType → ℝ
111 | .t11 => 6
112 | .t12 => 4
113 | .t21 => 4
114 | .t13 => 6
115 | .t31 => 6
116 | .t22 => 4
117
118theorem orbitStarSize_pos (ty : HingeOrbitType) : 0 < orbitStarSize ty := by
119 cases ty <;> norm_num [orbitStarSize]
120
121theorem orbitStarSize_ne_zero (ty : HingeOrbitType) : orbitStarSize ty ≠ 0 :=
122 ne_of_gt (orbitStarSize_pos ty)
123
124/-- Distinct-hinge continuum fold: true hinge sum wants distinct hinges
125with full-star deficit, i.e. weight `1/r_τ` on each orbit fold.
126Not bare `blochFoldAll`, and not fitted `2/r`. -/
127def blochFoldAllDistinctHinge (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
128 ∑ ty : HingeOrbitType, (orbitStarSize ty)⁻¹ * blochFoldOrbit ty H m
129
130/-! ## §2. Pushforward reindex -/
131
132theorem classDot_pushforward (v : Fin 15 → ℝ) (p : Fin 24) (H : Mat4) :
133 classDot (pushforwardClass v p) H =
134 ∑ d0 : Fin 15, v d0 * classCoeff H (permClass p d0) := by
135 unfold classDot coeffDot pushforwardClass
136 simp_rw [Finset.sum_mul]
137 rw [Finset.sum_comm]
138 refine Finset.sum_congr rfl fun d0 _ => ?_
139 have h : ∀ d : Fin 15,
140 (if permClass p d0 = d then v d0 else 0) * classCoeff H d =
141 if permClass p d0 = d then v d0 * classCoeff H d else 0 := by
142 intro d; split_ifs <;> simp
143 simp_rw [h]
144 rw [Finset.sum_ite_eq]
145 simp
146
147theorem phasedClassDot_pushforward (v : Fin 15 → ℝ) (p : Fin 24) (H : Mat4)
148 (m x : Fin 4 → ℝ) :
149 phasedClassDot (pushforwardClass v p) H m x =
150 ∑ d0 : Fin 15, v d0 * planeWaveClassPert H m x (permClass p d0) := by
151 unfold phasedClassDot pushforwardClass
152 simp_rw [Finset.sum_mul]
153 rw [Finset.sum_comm]
154 refine Finset.sum_congr rfl fun d0 _ => ?_
155 have h : ∀ d : Fin 15,
156 (if permClass p d0 = d then v d0 else 0) * planeWaveClassPert H m x d =
157 if permClass p d0 = d then
158 v d0 * planeWaveClassPert H m x d else 0 := by
159 intro d; split_ifs <;> simp
160 simp_rw [h]
161 rw [Finset.sum_ite_eq]
162 simp
163
164/-! ## §3. (1,1) recovery of `blochFold11` -/
165
166theorem orbitSeedKernel_t11 :
167 orbitSeedKernel .t11 = ReggeHinge4DStarKernel.fullStarClassKernel := rfl
168
169theorem transportedOrbitDeficit_t11 (p : Fin 24) :
170 transportedOrbitDeficit .t11 p = transportedDeficit p := by
171 funext d
172 simp [transportedOrbitDeficit, pushforwardClass, transportedDeficit,
173 orbitSeedKernel_t11]
174
175theorem slotOrbitDeficitKer_t11 (s : Fin 24) (t : Fin 10) :
176 slotOrbitDeficitKer .t11 s t = slotDeficitKer s t := by
177 unfold slotOrbitDeficitKer slotDeficitKer
178 rw [transportedOrbitDeficit_t11, orbitCoveringPerm_t11_eq_slotTransportPerm]
179
180/-- Integer 4× pushforward of the `(1,1)` seed area covector. -/
181def pushAreaZ4 (p : Fin 24) (d : Fin 15) : ℤ :=
182 (if d = permClass p 0 then (1 : ℤ) else 0) +
183 (if d = permClass p 1 then 1 else 0)
184
185private lemma pushforward_areaCov11_div4 (p : Fin 24) (d : Fin 15) :
186 pushforwardClass (orbitAreaCov .t11) p d = (pushAreaZ4 p d : ℝ) / 4 := by
187 unfold pushforwardClass pushAreaZ4
188 let f : Fin 15 → ℝ := fun d0 =>
189 if permClass p d0 = d then orbitAreaCov .t11 d0 else 0
190 have hz : ∀ d0 ∈ (Finset.univ : Finset (Fin 15)),
191 d0 ∉ ({(0 : Fin 15), 1} : Finset (Fin 15)) → f d0 = 0 := by
192 intro d0 _ hd0
193 have hne : d0 ≠ 0 ∧ d0 ≠ 1 := by
194 constructor <;> intro hx <;> simp [hx] at hd0
195 have ha : orbitAreaCov .t11 d0 = 0 := by
196 fin_cases d0 <;> simp_all [orbitAreaCov, areaCov11]
197 simp [f, ha]
198 have hsum :
199 (∑ d0 : Fin 15, f d0) =
200 ∑ d0 ∈ ({(0 : Fin 15), 1} : Finset (Fin 15)), f d0 := by
201 simpa using (Finset.sum_subset (Finset.subset_univ _) hz).symm
202 simp only [f] at hsum ⊢
203 rw [hsum, Finset.sum_pair (by decide : (0 : Fin 15) ≠ 1)]
204 simp [orbitAreaCov, areaCov11, eq_comm]
205 split_ifs <;> norm_num
206
207private lemma slotAreaCov_div4 (s : Fin 24) (t : Fin 10) (d : Fin 15) :
208 slotAreaCov s t d = (slotAreaCovZ4 s t d : ℝ) / 4 := by
209 unfold slotAreaCov slotAreaCovZ4
210 split_ifs <;> norm_num
211
212set_option maxRecDepth 8000 in
213set_option maxHeartbeats 800000 in
214private lemma pushAreaZ4_eq_slotAreaCovZ4 (s : Fin 24) (t : Fin 10)
215 (h : isT11 s t) (d : Fin 15) :
216 pushAreaZ4 (slotTransportPerm s t) d = slotAreaCovZ4 s t d := by
217 fin_cases s <;> fin_cases t <;>
218 first
219 | exfalso; exact absurd h (by decide)
220 | fin_cases d <;> decide
221
222/-- On `(1,1)` slots, transported assembly area recovers `slotAreaCov`. -/
223theorem slotOrbitAreaCov_t11 (s : Fin 24) (t : Fin 10) (h : isT11 s t) :
224 slotOrbitAreaCov .t11 s t = slotAreaCov s t := by
225 funext d
226 simp only [slotOrbitAreaCov, transportedOrbitArea,
227 orbitCoveringPerm_t11_eq_slotTransportPerm]
228 rw [pushforward_areaCov11_div4, slotAreaCov_div4,
229 pushAreaZ4_eq_slotAreaCovZ4 s t h d]
230
231/-- Compatibility wrapper (audit / older callers): same as `slotOrbitAreaCov_t11`. -/
232theorem slotOrbitAreaCov_t11_eq (s : Fin 24) (t : Fin 10) (h : isT11 s t) :
233 slotOrbitAreaCov .t11 s t = slotAreaCov s t :=
234 slotOrbitAreaCov_t11 s t h
235
236/-- Formerly OPEN Prop naming the `(1,1)` area pushforward identity.
237Now inhabited by `AreaPushforwardMatchOpen_holds`. -/
238def AreaPushforwardMatchOpen : Prop :=
239 ∀ (s : Fin 24) (t : Fin 10), isT11 s t →
240 transportedOrbitArea .t11 (orbitCoveringPerm .t11 s t) = slotAreaCov s t
241
242theorem AreaPushforwardMatchOpen_holds : AreaPushforwardMatchOpen := by
243 intro s t h
244 simpa [slotOrbitAreaCov] using slotOrbitAreaCov_t11 s t h
245
246theorem transportedOrbitSlotTerm_t11 (H : Mat4) (m : Fin 4 → ℝ)
247 (s : Fin 24) (t : Fin 10) :
248 transportedOrbitSlotTerm .t11 H m s t = transportedSlotTerm H m s t := by
249 unfold transportedOrbitSlotTerm transportedSlotTerm
250 by_cases h : isOrbit .t11 s t
251 · have ht : isT11 s t := (isOrbit_t11_iff_isT11 s t).mp h
252 simp [h, ht, slotOrbitAreaCov_t11 s t ht, slotOrbitDeficitKer_t11]
253 · have ht : ¬ isT11 s t := fun ht =>
254 h ((isOrbit_t11_iff_isT11 s t).mpr ht)
255 simp [h, ht]
256
257theorem blochFoldOrbit_t11 (H : Mat4) (m : Fin 4 → ℝ) :
258 blochFoldOrbit .t11 H m = blochFold11 H m := by
259 unfold blochFoldOrbit blochFold11
260 refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ =>
261 transportedOrbitSlotTerm_t11 H m s t
262
263/-! ## §4. Zero-momentum phase drop -/
264
265theorem transportedOrbitSlotTerm_zeroMomentum (ty : HingeOrbitType)
266 (H : Mat4) (s : Fin 24) (t : Fin 10) :
267 transportedOrbitSlotTerm ty H (fun _ => (0 : ℝ)) s t =
268 if isOrbit ty s t then
269 classDot (slotOrbitAreaCov ty s t) H *
270 classDot (slotOrbitDeficitKer ty s t) H
271 else 0 := by
272 unfold transportedOrbitSlotTerm
273 by_cases h : isOrbit ty s t <;> simp [h, phasedClassDot_zeroMomentum]
274
275/-- OPEN: transported zero-momentum all-orbit fold equals the committed
276true-weight assembly quadratic for general `H`. Reindex gives
277`classDot (push v p) H = ∑ v d0 * classCoeff H (permClass p d0)`, which
278equals `classDot v H` only under class-coeff invariance along `p`, not in
279general. Banked separately from the m² continuum symbol. -/
280def ZeroMomTrueWeightMatchOpen : Prop :=
281 ∀ H : Mat4, blochFoldAll H (fun _ => (0 : ℝ)) = trueWeightZeroMomQuadratic H
282
283/-! ## §4b. Quadratic homogeneity (polarization scaling) -/
284
285theorem transportedOrbitSlotTerm_smul (ty : HingeOrbitType) (c : ℝ)
286 (H : Mat4) (m : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
287 transportedOrbitSlotTerm ty (c • H) m s t =
288 c ^ 2 * transportedOrbitSlotTerm ty H m s t := by
289 unfold transportedOrbitSlotTerm
290 by_cases h : isOrbit ty s t
291 · simp only [h, ite_true]
292 rw [phasedClassDot_smul, phasedClassDot_smul]
293 ring
294 · simp [h]
295
296theorem blochFoldOrbit_smul (ty : HingeOrbitType) (c : ℝ) (H : Mat4)
297 (m : Fin 4 → ℝ) :
298 blochFoldOrbit ty (c • H) m = c ^ 2 * blochFoldOrbit ty H m := by
299 unfold blochFoldOrbit
300 simp_rw [transportedOrbitSlotTerm_smul, ← Finset.mul_sum]
301
302theorem blochFoldAll_smul (c : ℝ) (H : Mat4) (m : Fin 4 → ℝ) :
303 blochFoldAll (c • H) m = c ^ 2 * blochFoldAll H m := by
304 unfold blochFoldAll
305 simp_rw [blochFoldOrbit_smul, ← Finset.mul_sum]
306
307theorem blochFoldAll_zero (m : Fin 4 → ℝ) : blochFoldAll 0 m = 0 := by
308 have h := blochFoldAll_smul (0 : ℝ) (1 : Mat4) m
309 simpa using h
310
311theorem blochFoldAllDistinctHinge_smul (c : ℝ) (H : Mat4) (m : Fin 4 → ℝ) :
312 blochFoldAllDistinctHinge (c • H) m =
313 c ^ 2 * blochFoldAllDistinctHinge H m := by
314 unfold blochFoldAllDistinctHinge
315 simp_rw [blochFoldOrbit_smul]
316 have hterm : ∀ ty : HingeOrbitType,
317 (orbitStarSize ty)⁻¹ * (c ^ 2 * blochFoldOrbit ty H m) =
318 c ^ 2 * ((orbitStarSize ty)⁻¹ * blochFoldOrbit ty H m) := by
319 intro ty; ring
320 simp_rw [hterm, ← Finset.mul_sum]
321
322theorem blochFoldAllDistinctHinge_zero (m : Fin 4 → ℝ) :
323 blochFoldAllDistinctHinge 0 m = 0 := by
324 have h := blochFoldAllDistinctHinge_smul (0 : ℝ) (1 : Mat4) m
325 simpa using h
326
327/-! ## §5. Transported m² moment polynomials -/
328
329/-- Zero-momentum (unphased) transported deficit · classCoeff at a slot. -/
330def slotOrbitKerDot (ty : HingeOrbitType) (H : Mat4) (s : Fin 24)
331 (t : Fin 10) : ℝ :=
332 ∑ d : Fin 15, slotOrbitDeficitKer ty s t d * classCoeff H d
333
334/-- Truncated cosine two-jet slot coefficient `A0*K2`, i.e. the historical
335form that assumes slotwise `K0 = 0` (deficit annihilation at μ = 0). -/
336def m2TransportedOrbitSlotCoeffTrunc (ty : HingeOrbitType) (H : Mat4)
337 (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) : ℝ :=
338 if isOrbit ty s t then
339 (∑ d : Fin 15, slotOrbitAreaCov ty s t d * classCoeff H d) *
340 (-(1 / 2 : ℝ) *
341 ∑ d : Fin 15,
342 slotOrbitDeficitKer ty s t d * classCoeff H d *
343 (phaseScaleDir dir (hingeBase s t) d) ^ 2)
344 else 0
345
346/-- Full cosine two-jet of the phased product `A(μ)K(μ)`:
347`A0*K2 + A2*K0` with `A2 = -½ Aph²` and `K2 = -½ Kph²`.
348Equals the truncated form whenever `slotOrbitKerDot = 0`. -/
349def m2TransportedOrbitSlotCoeffFull (ty : HingeOrbitType) (H : Mat4)
350 (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) : ℝ :=
351 if isOrbit ty s t then
352 (∑ d : Fin 15, slotOrbitAreaCov ty s t d * classCoeff H d) *
353 (-(1 / 2 : ℝ) *
354 ∑ d : Fin 15,
355 slotOrbitDeficitKer ty s t d * classCoeff H d *
356 (phaseScaleDir dir (hingeBase s t) d) ^ 2) +
357 (-(1 / 2 : ℝ) *
358 ∑ d : Fin 15,
359 slotOrbitAreaCov ty s t d * classCoeff H d *
360 (phaseScaleDir dir (hingeBase s t) d) ^ 2) *
361 slotOrbitKerDot ty H s t
362 else 0
363
364theorem m2TransportedOrbitSlotCoeffFull_eq_trunc_of_ker0
365 (ty : HingeOrbitType) (H : Mat4) (dir : Fin 4 → ℝ)
366 (s : Fin 24) (t : Fin 10) (hK0 : slotOrbitKerDot ty H s t = 0) :
367 m2TransportedOrbitSlotCoeffFull ty H dir s t =
368 m2TransportedOrbitSlotCoeffTrunc ty H dir s t := by
369 unfold m2TransportedOrbitSlotCoeffFull m2TransportedOrbitSlotCoeffTrunc
370 by_cases h : isOrbit ty s t
371 · rw [if_pos h, if_pos h, hK0]
372 ring
373 · rw [if_neg h, if_neg h]
374
375/-- Canonical transported m² slot coefficient: truncated `A0*K2` form used by
376the integer certificates. The honest product two-jet is
377`m2TransportedOrbitSlotCoeffFull = A0*K2 + A2*K0`; on TT plus/cross the
378two agree slotwise (`K0 = 0`, THEOREM
379`slotOrbitKerDot_axisTTPlus` / `slotOrbitKerDot_axisTTCross` in
380`ReggeBlochTransportedAllOrbitM2Eval4D`; probe
381`scripts/probe_m2_full_twojet_e0.py`). -/
382abbrev m2TransportedOrbitSlotCoeff := m2TransportedOrbitSlotCoeffTrunc
383
384def m2TransportedOrbitMoment (ty : HingeOrbitType) (H : Mat4)
385 (dir : Fin 4 → ℝ) : ℝ :=
386 ∑ s : Fin 24, ∑ t : Fin 10, m2TransportedOrbitSlotCoeff ty H dir s t
387
388def m2TransportedAllOrbitMoment (H : Mat4) (dir : Fin 4 → ℝ) : ℝ :=
389 ∑ ty : HingeOrbitType, m2TransportedOrbitMoment ty H dir
390
391/-- Distinct-hinge m² moment: weight `1/r_τ` on each orbit moment. -/
392def m2TransportedAllOrbitMomentDistinctHinge (H : Mat4)
393 (dir : Fin 4 → ℝ) : ℝ :=
394 ∑ ty : HingeOrbitType,
395 (orbitStarSize ty)⁻¹ * m2TransportedOrbitMoment ty H dir
396
397/-- Full-jet orbit / distinct-hinge aggregates. -/
398def m2TransportedOrbitMomentFull (ty : HingeOrbitType) (H : Mat4)
399 (dir : Fin 4 → ℝ) : ℝ :=
400 ∑ s : Fin 24, ∑ t : Fin 10, m2TransportedOrbitSlotCoeffFull ty H dir s t
401
402def m2TransportedAllOrbitMomentDistinctHingeFull (H : Mat4)
403 (dir : Fin 4 → ℝ) : ℝ :=
404 ∑ ty : HingeOrbitType,
405 (orbitStarSize ty)⁻¹ * m2TransportedOrbitMomentFull ty H dir
406
407private lemma sum_mul_classCoeff_smul (c : ℝ) (H : Mat4) (f : Fin 15 → ℝ) :
408 (∑ d : Fin 15, f d * classCoeff (c • H) d) =
409 c * ∑ d : Fin 15, f d * classCoeff H d := by
410 simp_rw [classCoeff_smul]
411 have hterm : ∀ d : Fin 15, f d * (c * classCoeff H d) = c * (f d * classCoeff H d) := by
412 intro d; ring
413 simp_rw [hterm, ← Finset.mul_sum]
414
415private lemma sum_mul_classCoeff_phase_smul (c : ℝ) (H : Mat4)
416 (f g : Fin 15 → ℝ) :
417 (∑ d : Fin 15, f d * classCoeff (c • H) d * g d) =
418 c * ∑ d : Fin 15, f d * classCoeff H d * g d := by
419 simp_rw [classCoeff_smul]
420 have hterm : ∀ d : Fin 15,
421 f d * (c * classCoeff H d) * g d = c * (f d * classCoeff H d * g d) := by
422 intro d; ring
423 simp_rw [hterm, ← Finset.mul_sum]
424
425theorem m2TransportedOrbitSlotCoeffTrunc_smul (ty : HingeOrbitType) (c : ℝ)
426 (H : Mat4) (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
427 m2TransportedOrbitSlotCoeffTrunc ty (c • H) dir s t =
428 c ^ 2 * m2TransportedOrbitSlotCoeffTrunc ty H dir s t := by
429 unfold m2TransportedOrbitSlotCoeffTrunc
430 by_cases h : isOrbit ty s t
431 · simp only [h, ite_true]
432 rw [sum_mul_classCoeff_smul c H (slotOrbitAreaCov ty s t)]
433 rw [sum_mul_classCoeff_phase_smul c H (slotOrbitDeficitKer ty s t)
434 (fun d => (phaseScaleDir dir (hingeBase s t) d) ^ 2)]
435 ring
436 · simp only [h, ↓reduceIte, mul_zero]
437
438theorem m2TransportedOrbitSlotCoeff_smul (ty : HingeOrbitType) (c : ℝ)
439 (H : Mat4) (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
440 m2TransportedOrbitSlotCoeff ty (c • H) dir s t =
441 c ^ 2 * m2TransportedOrbitSlotCoeff ty H dir s t :=
442 m2TransportedOrbitSlotCoeffTrunc_smul ty c H dir s t
443
444theorem m2TransportedOrbitSlotCoeffFull_smul (ty : HingeOrbitType) (c : ℝ)
445 (H : Mat4) (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
446 m2TransportedOrbitSlotCoeffFull ty (c • H) dir s t =
447 c ^ 2 * m2TransportedOrbitSlotCoeffFull ty H dir s t := by
448 unfold m2TransportedOrbitSlotCoeffFull slotOrbitKerDot
449 by_cases h : isOrbit ty s t
450 · simp only [h, ite_true]
451 rw [sum_mul_classCoeff_smul c H (slotOrbitAreaCov ty s t)]
452 rw [sum_mul_classCoeff_phase_smul c H (slotOrbitDeficitKer ty s t)
453 (fun d => (phaseScaleDir dir (hingeBase s t) d) ^ 2)]
454 rw [sum_mul_classCoeff_phase_smul c H (slotOrbitAreaCov ty s t)
455 (fun d => (phaseScaleDir dir (hingeBase s t) d) ^ 2)]
456 rw [sum_mul_classCoeff_smul c H (slotOrbitDeficitKer ty s t)]
457 ring
458 · simp only [h, ↓reduceIte, mul_zero]
459
460theorem m2TransportedOrbitMoment_smul (ty : HingeOrbitType) (c : ℝ)
461 (H : Mat4) (dir : Fin 4 → ℝ) :
462 m2TransportedOrbitMoment ty (c • H) dir =
463 c ^ 2 * m2TransportedOrbitMoment ty H dir := by
464 unfold m2TransportedOrbitMoment
465 simp_rw [m2TransportedOrbitSlotCoeff_smul, ← Finset.mul_sum]
466
467theorem m2TransportedAllOrbitMomentDistinctHinge_smul (c : ℝ) (H : Mat4)
468 (dir : Fin 4 → ℝ) :
469 m2TransportedAllOrbitMomentDistinctHinge (c • H) dir =
470 c ^ 2 * m2TransportedAllOrbitMomentDistinctHinge H dir := by
471 unfold m2TransportedAllOrbitMomentDistinctHinge
472 simp_rw [m2TransportedOrbitMoment_smul]
473 have hterm : ∀ ty : HingeOrbitType,
474 (orbitStarSize ty)⁻¹ * (c ^ 2 * m2TransportedOrbitMoment ty H dir) =
475 c ^ 2 * ((orbitStarSize ty)⁻¹ * m2TransportedOrbitMoment ty H dir) := by
476 intro ty; ring
477 simp_rw [hterm, ← Finset.mul_sum]
478
479theorem m2TransportedOrbitMomentFull_smul (ty : HingeOrbitType) (c : ℝ)
480 (H : Mat4) (dir : Fin 4 → ℝ) :
481 m2TransportedOrbitMomentFull ty (c • H) dir =
482 c ^ 2 * m2TransportedOrbitMomentFull ty H dir := by
483 unfold m2TransportedOrbitMomentFull
484 simp_rw [m2TransportedOrbitSlotCoeffFull_smul, ← Finset.mul_sum]
485
486theorem m2TransportedAllOrbitMomentDistinctHingeFull_smul (c : ℝ) (H : Mat4)
487 (dir : Fin 4 → ℝ) :
488 m2TransportedAllOrbitMomentDistinctHingeFull (c • H) dir =
489 c ^ 2 * m2TransportedAllOrbitMomentDistinctHingeFull H dir := by
490 unfold m2TransportedAllOrbitMomentDistinctHingeFull
491 simp_rw [m2TransportedOrbitMomentFull_smul]
492 have hterm : ∀ ty : HingeOrbitType,
493 (orbitStarSize ty)⁻¹ * (c ^ 2 * m2TransportedOrbitMomentFull ty H dir) =
494 c ^ 2 * ((orbitStarSize ty)⁻¹ * m2TransportedOrbitMomentFull ty H dir) := by
495 intro ty; ring
496 simp_rw [hterm, ← Finset.mul_sum]
497
498theorem phaseScaleDir_symbolDir (x : Fin 4 → ℝ) (d : Fin 15) :
499 phaseScaleDir symbolDir x d = phaseScale x d := by
500 rfl
501
502theorem m2TransportedOrbitSlotCoeff_t11 (H : Mat4) (s : Fin 24) (t : Fin 10) :
503 m2TransportedOrbitSlotCoeff .t11 H symbolDir s t = m2SlotCoeff H s t := by
504 change m2TransportedOrbitSlotCoeffTrunc .t11 H symbolDir s t = m2SlotCoeff H s t
505 unfold m2TransportedOrbitSlotCoeffTrunc m2SlotCoeff
506 by_cases h : isOrbit .t11 s t
507 · have ht : isT11 s t := (isOrbit_t11_iff_isT11 s t).mp h
508 rw [if_pos h, if_pos ht, slotOrbitAreaCov_t11 s t ht, slotOrbitDeficitKer_t11]
509 simp_rw [phaseScaleDir_symbolDir]
510 · have ht : ¬ isT11 s t := fun ht =>
511 h ((isOrbit_t11_iff_isT11 s t).mpr ht)
512 rw [if_neg h, if_neg ht]
513
514theorem m2TransportedOrbitMoment_t11 (H : Mat4) :
515 m2TransportedOrbitMoment .t11 H symbolDir = m2Symbol H := by
516 unfold m2TransportedOrbitMoment m2Symbol
517 refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ =>
518 m2TransportedOrbitSlotCoeff_t11 H s t
519
520/-- Formerly OPEN: raw all-orbit moment on axisTTPlus / symbolDir equals `-5/2`
521(orbit slices t11=-3, t12=+2, t13=-3/2). After `/|symbolDir|²` this is
522`-5/4`. Closed in `ReggeBlochTransportedAllOrbitM2Eval4D`.
523Distinct-hinge weight `1/r_τ` upgrades the raw axis value to `-1/4`
524(path A; residual continuum dictionary still needed for EH Tendsto). -/
525def M2TransportedAllOrbitAxisSymbolDirEvalOpen : Prop :=
526 m2TransportedAllOrbitMoment axisTTPlus symbolDir = (-5 / 2 : ℝ)
527
528/-- Distinct-hinge raw m² on axisTTPlus / symbolDir equals frozen EH `-1/4`
529(`-3/6 + 2/4 + (-3/2)/6`). Closed in M2Eval. -/
530def M2DistinctHingeAxisSymbolDirEvalOpen : Prop :=
531 m2TransportedAllOrbitMomentDistinctHinge axisTTPlus symbolDir =
532 (-1 / 4 : ℝ)
533
534/-! ## §6. Status -/
535
536structure ReggeBlochTransportedAllOrbit4DStatus where
537 definitionsClosed : Bool
538 t11MatchClosed : Bool
539 m2T11SliceClosed : Bool
540 m2AllOrbitAxisEvalClosed : Bool
541 distinctHingeAxisEvalClosed : Bool
542 m2TendstoClosed : Bool
543 continuumEHClosed : Bool
544 gapActionRecovery : Bool
545
546def reggeBlochTransportedAllOrbit4DStatus :
547 ReggeBlochTransportedAllOrbit4DStatus where
548 definitionsClosed := true
549 t11MatchClosed := true
550 m2T11SliceClosed := true
551 m2AllOrbitAxisEvalClosed := true
552 distinctHingeAxisEvalClosed := true
553 m2TendstoClosed := false
554 continuumEHClosed := false
555 gapActionRecovery := false
556
557theorem reggeBlochTransportedAllOrbit4DStatus_flags :
558 reggeBlochTransportedAllOrbit4DStatus.definitionsClosed = true ∧
559 reggeBlochTransportedAllOrbit4DStatus.t11MatchClosed = true ∧
560 reggeBlochTransportedAllOrbit4DStatus.m2T11SliceClosed = true ∧
561 reggeBlochTransportedAllOrbit4DStatus.m2AllOrbitAxisEvalClosed =
562 true ∧
563 reggeBlochTransportedAllOrbit4DStatus.distinctHingeAxisEvalClosed =
564 true ∧
565 reggeBlochTransportedAllOrbit4DStatus.m2TendstoClosed = false ∧
566 reggeBlochTransportedAllOrbit4DStatus.continuumEHClosed =
567 false ∧
568 reggeBlochTransportedAllOrbit4DStatus.gapActionRecovery =
569 false := by
570 decide
571
572end
573
574end ReggeBlochTransportedAllOrbit4D
575end Analysis
576end Gravity
577end IndisputableMonolith
578