IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4D.lean · 510 lines · 47 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochData4D
3import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
4import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
5import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
6import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumAssemble
7import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelGlue
8
9/-!
10# Exact midpoint Bloch m² TT identity (4D)
11
12Closes `exact_midpoint_m2_tt_identity`.
13Script: `scripts/qg/regge_4d_m2_tt_identity_20260721.py`.
14Kernel upgrade: `scripts/qg/regge_4d_m2_kernel_certs_20260721.py`.
15-/
16
17namespace IndisputableMonolith
18namespace Gravity
19namespace Analysis
20namespace ReggeExactMidpointM2TTIdentity4D
21
22open ReggeExactFlatHessianBlochData4D
23open ReggeExactFlatHessianBlochSymbol4D (exactMidpointBlochM2 edgeStrain couplingPhase
24 couplingWeight couplingWeightIdx couplingPhaseIdx CouplingIdx)
25open KernelCert
26open KernelGlue (m2CoeffSum_eq_m2Num_div m2CoeffSum_eq_explicitM2CoeffZ
27 explicitM2CoeffZ closedCoeffZ closedCoeff_eq_closedCoeffZ
28 symFull_scale symFullZ_rat_explicit_eq_closed)
29open EdgeTTDecomposition4D
30 (IsSymmetric IsTT IsTraceless IsTransverse euclideanTrace gaugePart
31 gaugePart_symmetric)
32open BigOperators
33
34set_option maxRecDepth 4096
35set_option maxHeartbeats 40000000
36
37abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
38abbrev Wave4 := Fin 4 → ℝ
39
40def frobeniusNormSq (E : Mat4) : ℝ :=
41 ∑ i : Fin 4, ∑ j : Fin 4, E i j * E i j
42
43def waveNormSq (k : Wave4) : ℝ :=
44 ∑ i : Fin 4, k i * k i
45
46def couplingS (coup : Coupling) : ℚ :=
47 (coup.num : ℚ) / (coup.den : ℚ)
48
49theorem couplingS_eq_s (coup : Coupling) : couplingS coup = coup.s := rfl
50
51def deltaQ (coup : Coupling) (i : Fin 4) : ℚ :=
52 (coup.delta2 i : ℚ) / 2
53
54def m2Coeff (a b c d i j : Fin 4) : ℚ :=
55 ∑ idx : CouplingIdx,
56 (-(1 / 4) : ℚ) * couplingS couplingTable[idx] *
57 (couplingTable[idx].De a : ℚ) * (couplingTable[idx].De b : ℚ) *
58 (couplingTable[idx].Dep c : ℚ) * (couplingTable[idx].Dep d : ℚ) *
59 deltaQ couplingTable[idx] i * deltaQ couplingTable[idx] j
60
61theorem m2Coeff_eq_m2CoeffSum (a b c d i j : Fin 4) :
62 m2Coeff a b c d i j = KernelGlue.m2CoeffSum a b c d i j := by
63 unfold m2Coeff KernelGlue.m2CoeffSum couplingS deltaQ
64 rfl
65
66/-- Scale-32 Int table cast; kernel-checkable via `KernelCert.explicitZ`. -/
67def explicitM2Coeff (a b c d i j : Fin 4) : ℚ :=
68 explicitM2CoeffZ a b c d i j
69
70/-- Array/Finset m² coefficient equals the Int fold / 256. -/
71theorem m2Coeff_eq_m2Num_div (a b c d i j : Fin 4) :
72 m2Coeff a b c d i j = (m2Num a b c d i j : ℚ) / 256 := by
73 rw [m2Coeff_eq_m2CoeffSum, m2CoeffSum_eq_m2Num_div]
74
75theorem m2Coeff_eq_explicitM2Coeff :
76 ∀ (a b c d i j : Fin 4), m2Coeff a b c d i j = explicitM2Coeff a b c d i j := by
77 intro a b c d i j
78 rw [m2Coeff_eq_m2CoeffSum, explicitM2Coeff, m2CoeffSum_eq_explicitM2CoeffZ]
79
80/-! ## S3. Symmetrized coefficient certificate -/
81
82/-- Closed-form coefficient table: Frobenius + load + trace^2 + trace-quadratic
83pieces of `closedForm`, written per matrix index. -/
84def closedCoeff (a b c d i j : Fin 4) : ℚ :=
85 (if a = c ∧ b = d ∧ i = j then -(1 / 8) else 0) +
86 (if a = c ∧ b = i ∧ d = j then (1 / 4) else 0) +
87 (if a = b ∧ c = d ∧ i = j then (1 / 8) else 0) +
88 (if a = b ∧ c = i ∧ d = j then -(1 / 4) else 0)
89
90/-- Average over the `(a,b)`- and `(c,d)`-flips. -/
91def sym4C (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
92 (a b c d i j : Fin 4) : ℚ :=
93 (C a b c d i j + C b a c d i j + C a b d c i j + C b a d c i j) / 4
94
95/-- Average over the pair exchange `(a,b) ←> (c,d)`. -/
96def sym2exC (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
97 (a b c d i j : Fin 4) : ℚ :=
98 (C a b c d i j + C c d a b i j) / 2
99
100/-- Full bi-quadratic symmetrization (order-8 group generated by the two
101flips and the pair exchange). -/
102def symFull (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
103 (a b c d i j : Fin 4) : ℚ :=
104 sym2exC (sym4C C) a b c d i j
105
106/-- Certificate: the symmetrizations of the explicit m^2 table and of the
107closed-form coefficient table agree pointwise (4096 rational identities). -/
108theorem closedCoeff_eq_closedCoeffZ_pointwise :
109 ∀ a b c d i j : Fin 4,
110 closedCoeff a b c d i j = closedCoeffZ a b c d i j := by
111 intro a b c d i j
112 simpa [closedCoeff] using closedCoeff_eq_closedCoeffZ a b c d i j
113
114private theorem symFull_eq_symFullZ_div
115 (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Int)
116 (D : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
117 (hD : ∀ a b c d i j, D a b c d i j = (C a b c d i j : ℚ) / 32)
118 (a b c d i j : Fin 4) :
119 symFull D a b c d i j = (symFullZ C a b c d i j : ℚ) / 32 := by
120 unfold symFull sym2exC sym4C
121 simp only [hD]
122 exact symFull_scale C a b c d i j
123
124theorem symFull_explicit_eq_symFull_closed :
125 ∀ a b c d i j : Fin 4,
126 symFull explicitM2Coeff a b c d i j = symFull closedCoeff a b c d i j := by
127 intro a b c d i j
128 have hE : ∀ a b c d i j,
129 explicitM2Coeff a b c d i j = (explicitZ a b c d i j : ℚ) / 32 := by
130 intro a b c d i j; rfl
131 have hC : ∀ a b c d i j,
132 closedCoeff a b c d i j = (closedZ a b c d i j : ℚ) / 32 :=
133 closedCoeff_eq_closedCoeffZ_pointwise
134 rw [symFull_eq_symFullZ_div explicitZ explicitM2Coeff hE,
135 symFull_eq_symFullZ_div closedZ closedCoeff hC,
136 symFullZ_rat_explicit_eq_closed]
137
138
139/-! ## S4. ℝ-bridge: bi-quadratic form and sum relabelings -/
140
141noncomputable section
142
143/-- Generic bi-quadratic form: quadratic in `H` entries, quadratic in `k`. -/
144def biquad (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
145 (H : Mat4) (k : Wave4) : ℝ :=
146 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
147 ((C a b c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j
148
149theorem biquad_congr {C1 C2 : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ}
150 (h : ∀ a b c d i j : Fin 4, C1 a b c d i j = C2 a b c d i j)
151 (H : Mat4) (k : Wave4) : biquad C1 H k = biquad C2 H k := by
152 unfold biquad
153 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
154 Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
155 Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
156 rw [h]
157
158private theorem sum2_mul (P : Fin 4 → Fin 4 → ℝ) (X : ℝ) :
159 (∑ a : Fin 4, ∑ b : Fin 4, P a b) * X =
160 ∑ a : Fin 4, ∑ b : Fin 4, P a b * X := by
161 rw [Finset.sum_mul]
162 exact Finset.sum_congr rfl fun a _ => Finset.sum_mul _ _ _
163
164private theorem triple_double_sum_mul (P Q3 R3 : Fin 4 → Fin 4 → ℝ) (c0 : ℝ) :
165 c0 * (∑ a : Fin 4, ∑ b : Fin 4, P a b) * (∑ c : Fin 4, ∑ d : Fin 4, Q3 c d) *
166 (∑ i : Fin 4, ∑ j : Fin 4, R3 i j) =
167 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
168 c0 * P a b * Q3 c d * R3 i j := by
169 have h1 : c0 * (∑ a : Fin 4, ∑ b : Fin 4, P a b) * (∑ c : Fin 4, ∑ d : Fin 4, Q3 c d) *
170 (∑ i : Fin 4, ∑ j : Fin 4, R3 i j) =
171 (∑ a : Fin 4, ∑ b : Fin 4, P a b) *
172 ((∑ c : Fin 4, ∑ d : Fin 4, Q3 c d) *
173 ((∑ i : Fin 4, ∑ j : Fin 4, R3 i j) * c0)) := by ring
174 rw [h1, sum2_mul]
175 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ => ?_
176 have h2 : P a b * ((∑ c : Fin 4, ∑ d : Fin 4, Q3 c d) *
177 ((∑ i : Fin 4, ∑ j : Fin 4, R3 i j) * c0)) =
178 (∑ c : Fin 4, ∑ d : Fin 4, Q3 c d) *
179 ((∑ i : Fin 4, ∑ j : Fin 4, R3 i j) * (c0 * P a b)) := by ring
180 rw [h2, sum2_mul]
181 refine Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ => ?_
182 have h3 : Q3 c d * ((∑ i : Fin 4, ∑ j : Fin 4, R3 i j) * (c0 * P a b)) =
183 (∑ i : Fin 4, ∑ j : Fin 4, R3 i j) * (c0 * P a b * Q3 c d) := by
184 ring
185 rw [h3, sum2_mul]
186 refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
187 ring
188
189private theorem term_expand (H : Mat4) (k : Wave4) (idx : CouplingIdx) :
190 couplingWeightIdx H idx * (-(couplingPhaseIdx k idx) ^ 2 / 2) =
191 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
192 (((-(1 / 4) : ℚ) * couplingS couplingTable[idx] *
193 (couplingTable[idx].De a : ℚ) * (couplingTable[idx].De b : ℚ) *
194 (couplingTable[idx].Dep c : ℚ) * (couplingTable[idx].Dep d : ℚ) *
195 deltaQ couplingTable[idx] i * deltaQ couplingTable[idx] j : ℚ) : ℝ) *
196 H a b * H c d * k i * k j := by
197 unfold couplingWeightIdx couplingPhaseIdx
198 generalize couplingTable[idx] = t
199 have h0 : couplingWeight H t * (-(couplingPhase t k) ^ 2 / 2) =
200 (-(1 / 4) * (t.s : ℝ)) * edgeStrain H t.De * edgeStrain H t.Dep *
201 (couplingPhase t k * couplingPhase t k) := by
202 unfold couplingWeight
203 ring
204 rw [h0]
205 unfold edgeStrain couplingPhase
206 rw [Finset.sum_mul_sum]
207 rw [triple_double_sum_mul]
208 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
209 Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
210 Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
211 simp only [couplingS, deltaQ, Coupling.s, Coupling.delta]
212 push_cast
213 ring
214
215/-- Expansion of the 1208-coupling m^2 sum as a bi-quadratic with the
216`m2Coeff` coefficient table. -/
217theorem exactMidpointBlochM2_eq_biquad (H : Mat4) (k : Wave4) :
218 exactMidpointBlochM2 H k = biquad m2Coeff H k := by
219 unfold exactMidpointBlochM2 biquad
220 refine (Finset.sum_congr rfl fun idx _ => term_expand H k idx).trans ?_
221 rw [Finset.sum_comm]
222 refine Finset.sum_congr rfl fun a _ => ?_
223 rw [Finset.sum_comm]
224 refine Finset.sum_congr rfl fun b _ => ?_
225 rw [Finset.sum_comm]
226 refine Finset.sum_congr rfl fun c _ => ?_
227 rw [Finset.sum_comm]
228 refine Finset.sum_congr rfl fun d _ => ?_
229 rw [Finset.sum_comm]
230 refine Finset.sum_congr rfl fun i _ => ?_
231 rw [Finset.sum_comm]
232 refine Finset.sum_congr rfl fun j _ => ?_
233 have hcast : ((m2Coeff a b c d i j : ℚ) : ℝ) =
234 ∑ idx : CouplingIdx,
235 (((-(1 / 4) : ℚ) * couplingS couplingTable[idx] *
236 (couplingTable[idx].De a : ℚ) * (couplingTable[idx].De b : ℚ) *
237 (couplingTable[idx].Dep c : ℚ) * (couplingTable[idx].Dep d : ℚ) *
238 deltaQ couplingTable[idx] i * deltaQ couplingTable[idx] j : ℚ) : ℝ) := by
239 unfold m2Coeff
240 exact Rat.cast_sum _ _
241 rw [hcast, Finset.sum_mul, Finset.sum_mul, Finset.sum_mul, Finset.sum_mul]
242
243/-! Sum relabeling lemmas (pure index bookkeeping). -/
244
245private theorem sum6_flip_ab (F : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ) :
246 (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
247 F a b c d i j) =
248 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
249 F b a c d i j :=
250 Finset.sum_comm
251
252private theorem sum6_flip_cd (F : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ) :
253 (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
254 F a b c d i j) =
255 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
256 F a b d c i j := by
257 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ => ?_
258 exact Finset.sum_comm
259
260private theorem sum4_exchange (G : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ) :
261 (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, G a b c d) =
262 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, G c d a b := by
263 have h : ∀ P : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ,
264 (∑ x : Fin 4 × Fin 4, ∑ y : Fin 4 × Fin 4, P x.1 x.2 y.1 y.2) =
265 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, P a b c d := by
266 intro P
267 rw [Fintype.sum_prod_type]
268 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ => ?_
269 rw [Fintype.sum_prod_type]
270 have h1 := h G
271 have h2 : (∑ x : Fin 4 × Fin 4, ∑ y : Fin 4 × Fin 4, G y.1 y.2 x.1 x.2) =
272 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, G c d a b :=
273 h fun a b c d => G c d a b
274 rw [← h1, ← h2]
275 exact Finset.sum_comm
276
277private theorem sum6_exchange (F : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ) :
278 (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
279 F a b c d i j) =
280 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
281 F c d a b i j :=
282 sum4_exchange fun a b c d => ∑ i : Fin 4, ∑ j : Fin 4, F a b c d i j
283
284/-! Symmetrization invariance of the bi-quadratic form. -/
285
286theorem biquad_sym4 (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
287 (H : Mat4) (k : Wave4) (hsym : IsSymmetric H) :
288 biquad (sym4C C) H k = biquad C H k := by
289 have hba : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
290 ((C b a c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j) =
291 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
292 ((C a b c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j := by
293 have h1 : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
294 ((C b a c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j) =
295 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
296 ((C a b c d i j : ℚ) : ℝ) * H b a * H c d * k i * k j :=
297 sum6_flip_ab fun x y c d i j => ((C y x c d i j : ℚ) : ℝ) * H x y * H c d * k i * k j
298 rw [h1]
299 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
300 Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
301 Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
302 rw [hsym b a]
303 have hdc : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
304 ((C a b d c i j : ℚ) : ℝ) * H a b * H c d * k i * k j) =
305 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
306 ((C a b c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j := by
307 have h1 : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
308 ((C a b d c i j : ℚ) : ℝ) * H a b * H c d * k i * k j) =
309 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
310 ((C a b c d i j : ℚ) : ℝ) * H a b * H d c * k i * k j :=
311 sum6_flip_cd fun a b x y i j => ((C a b y x i j : ℚ) : ℝ) * H a b * H x y * k i * k j
312 rw [h1]
313 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
314 Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
315 Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
316 rw [hsym d c]
317 have hbadc : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
318 ((C b a d c i j : ℚ) : ℝ) * H a b * H c d * k i * k j) =
319 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
320 ((C a b c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j := by
321 have h1 : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
322 ((C b a d c i j : ℚ) : ℝ) * H a b * H c d * k i * k j) =
323 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
324 ((C a b d c i j : ℚ) : ℝ) * H b a * H c d * k i * k j :=
325 sum6_flip_ab fun x y c d i j => ((C y x d c i j : ℚ) : ℝ) * H x y * H c d * k i * k j
326 have h2 : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
327 ((C a b d c i j : ℚ) : ℝ) * H b a * H c d * k i * k j) =
328 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
329 ((C a b c d i j : ℚ) : ℝ) * H b a * H d c * k i * k j :=
330 sum6_flip_cd fun a b x y i j => ((C a b y x i j : ℚ) : ℝ) * H b a * H x y * k i * k j
331 rw [h1, h2]
332 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
333 Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
334 Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
335 rw [hsym b a, hsym d c]
336 unfold biquad sym4C
337 have expand : ∀ a b c d i j : Fin 4,
338 (((C a b c d i j + C b a c d i j + C a b d c i j + C b a d c i j) / 4 : ℚ) : ℝ) *
339 H a b * H c d * k i * k j =
340 (((C a b c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j +
341 ((C b a c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j +
342 ((C a b d c i j : ℚ) : ℝ) * H a b * H c d * k i * k j +
343 ((C b a d c i j : ℚ) : ℝ) * H a b * H c d * k i * k j) / 4 := by
344 intro a b c d i j
345 push_cast
346 ring
347 simp_rw [expand, ← Finset.sum_div, Finset.sum_add_distrib]
348 rw [hba, hdc, hbadc]
349 ring
350
351theorem biquad_sym2ex (D : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
352 (H : Mat4) (k : Wave4) :
353 biquad (sym2exC D) H k = biquad D H k := by
354 have hex : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
355 ((D c d a b i j : ℚ) : ℝ) * H a b * H c d * k i * k j) =
356 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
357 ((D a b c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j := by
358 have h1 : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
359 ((D a b c d i j : ℚ) : ℝ) * H c d * H a b * k i * k j) =
360 ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4,
361 ((D c d a b i j : ℚ) : ℝ) * H a b * H c d * k i * k j :=
362 sum6_exchange fun a b c d i j => ((D a b c d i j : ℚ) : ℝ) * H c d * H a b * k i * k j
363 rw [← h1]
364 refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
365 Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
366 Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
367 ring
368 unfold biquad sym2exC
369 have expand : ∀ a b c d i j : Fin 4,
370 (((D a b c d i j + D c d a b i j) / 2 : ℚ) : ℝ) * H a b * H c d * k i * k j =
371 (((D a b c d i j : ℚ) : ℝ) * H a b * H c d * k i * k j +
372 ((D c d a b i j : ℚ) : ℝ) * H a b * H c d * k i * k j) / 2 := by
373 intro a b c d i j
374 push_cast
375 ring
376 simp_rw [expand, ← Finset.sum_div, Finset.sum_add_distrib]
377 rw [hex]
378 ring
379
380theorem biquad_symFull (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℚ)
381 (H : Mat4) (k : Wave4) (hsym : IsSymmetric H) :
382 biquad (symFull C) H k = biquad C H k := by
383 have h1 : biquad (symFull C) H k = biquad (sym4C C) H k :=
384 biquad_sym2ex (sym4C C) H k
385 exact h1.trans (biquad_sym4 C H k hsym)
386
387/-! ## S5. Closed form -/
388
389def loadNormSq (H : Mat4) (k : Wave4) : ℝ :=
390 ∑ m : Fin 4, (∑ n : Fin 4, H m n * k n) ^ 2
391
392def quadraticForm (H : Mat4) (k : Wave4) : ℝ :=
393 ∑ i : Fin 4, ∑ j : Fin 4, k i * H i j * k j
394
395def closedForm (H : Mat4) (k : Wave4) : ℝ :=
396 (-(1 / 8) : ℝ) * frobeniusNormSq H * waveNormSq k +
397 (1 / 4 : ℝ) * loadNormSq H k +
398 (1 / 8 : ℝ) * euclideanTrace H *
399 (euclideanTrace H * waveNormSq k - 2 * quadraticForm H k)
400
401/-- The closed-coefficient bi-quadratic reproduces `closedForm` for every `H`
402(not only symmetric ones): each ite piece collapses to its invariant. -/
403theorem biquad_closedCoeff_eq_closedForm (H : Mat4) (k : Wave4) :
404 biquad closedCoeff H k = closedForm H k := by
405 unfold biquad closedCoeff closedForm frobeniusNormSq waveNormSq loadNormSq
406 quadraticForm euclideanTrace
407 simp only [Rat.cast_add, apply_ite ((↑) : ℚ → ℝ), Rat.cast_neg,
408 Rat.cast_div, Rat.cast_one, Rat.cast_ofNat, Rat.cast_zero,
409 add_mul, ite_mul, zero_mul, Finset.sum_add_distrib, ite_and,
410 Finset.sum_ite_irrel, Finset.sum_const_zero, Finset.sum_ite_eq,
411 Finset.mem_univ, if_true]
412 simp only [Fin.sum_univ_four]
413 ring
414
415/-! ## S6. Main chain and TT identity -/
416
417theorem exactMidpointBlochM2_eq_closedForm_of_symmetric
418 (H : Mat4) (k : Wave4) (hsym : IsSymmetric H) :
419 exactMidpointBlochM2 H k = closedForm H k := by
420 calc
421 exactMidpointBlochM2 H k = biquad m2Coeff H k :=
422 exactMidpointBlochM2_eq_biquad H k
423 _ = biquad explicitM2Coeff H k :=
424 biquad_congr m2Coeff_eq_explicitM2Coeff H k
425 _ = biquad (symFull explicitM2Coeff) H k :=
426 (biquad_symFull explicitM2Coeff H k hsym).symm
427 _ = biquad (symFull closedCoeff) H k :=
428 biquad_congr symFull_explicit_eq_symFull_closed H k
429 _ = biquad closedCoeff H k := biquad_symFull closedCoeff H k hsym
430 _ = closedForm H k := biquad_closedCoeff_eq_closedForm H k
431
432theorem closedForm_eq_neg_eighth_of_TT
433 (H : Mat4) (k : Wave4) (hTT : IsTT k H) :
434 closedForm H k = (-(1 / 8) : ℝ) * frobeniusNormSq H * waveNormSq k := by
435 rcases hTT with ⟨_, htr, htrans⟩
436 unfold closedForm
437 have hload : loadNormSq H k = 0 := by
438 unfold loadNormSq
439 refine Finset.sum_eq_zero fun m _ => by simp [htrans m]
440 rw [htr, hload]
441 ring
442
443/-- **Typed blocker `exact_midpoint_m2_tt_identity`, closed.** For TT pairs
444the exact midpoint Bloch m^2 equals `-(1/8) |H|_F^2 |k|^2`. -/
445theorem exactMidpointBlochM2_eq_neg_eighth_frobenius_tt
446 (H : Mat4) (k : Wave4) (hTT : IsTT k H) :
447 exactMidpointBlochM2 H k =
448 (-(1 / 8) : ℝ) * frobeniusNormSq H * waveNormSq k := by
449 rw [exactMidpointBlochM2_eq_closedForm_of_symmetric H k hTT.1,
450 closedForm_eq_neg_eighth_of_TT H k hTT]
451
452
453/-- Unit-Frobenius TT Rayleigh face `-1/8`. -/
454theorem exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT
455 (H : Mat4) (k : Wave4) (hTT : IsTT k H)
456 (hF : frobeniusNormSq H = 1) (hk : waveNormSq k ≠ 0) :
457 exactMidpointBlochM2 H k / waveNormSq k = (-(1 / 8) : ℝ) := by
458 rw [exactMidpointBlochM2_eq_neg_eighth_frobenius_tt H k hTT, hF]
459 field_simp [hk]
460
461/-- Algebraic identity: closed form of a pure gauge pair is identically zero. -/
462theorem closedForm_gaugePart_eq_zero (m v : Wave4) :
463 closedForm (gaugePart m v) m = 0 := by
464 unfold closedForm frobeniusNormSq waveNormSq loadNormSq quadraticForm
465 euclideanTrace gaugePart
466 simp only [Fin.sum_univ_four]
467 ring
468
469/-- Exact midpoint Bloch m² vanishes on pure gauge pairs. -/
470theorem exactMidpointBlochM2_eq_zero_of_gaugePart (m v : Wave4) :
471 exactMidpointBlochM2 (gaugePart m v) m = 0 := by
472 rw [exactMidpointBlochM2_eq_closedForm_of_symmetric
473 (gaugePart m v) m (gaugePart_symmetric m v),
474 closedForm_gaugePart_eq_zero]
475
476/-- Alias kept for packing-route name compatibility. -/
477theorem exactMidpointBlochM2_gaugePart_eq_zero (m v : Wave4) :
478 exactMidpointBlochM2 (gaugePart m v) m = 0 :=
479 exactMidpointBlochM2_eq_zero_of_gaugePart m v
480
481/-- Pure-gauge Rayleigh quotient is zero when the mode is nonzero. -/
482theorem exactMidpointBlochM2_gauge_rayleigh_eq_zero
483 (m v : Wave4) (_hm : waveNormSq m ≠ 0) :
484 exactMidpointBlochM2 (gaugePart m v) m / waveNormSq m = 0 := by
485 rw [exactMidpointBlochM2_eq_zero_of_gaugePart, zero_div]
486
487/-- Packaged TT/gauge m² faces used by residual R3. -/
488theorem exactMidpointBlochM2_faces :
489 (∀ (H : Mat4) (k : Wave4),
490 IsTT k H →
491 frobeniusNormSq H = 1 →
492 waveNormSq k ≠ 0 →
493 exactMidpointBlochM2 H k / waveNormSq k = (-(1 / 8) : ℝ)) ∧
494 (∀ (m v : Wave4),
495 waveNormSq m ≠ 0 →
496 exactMidpointBlochM2 (gaugePart m v) m / waveNormSq m = 0) :=
497 ⟨exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT,
498 exactMidpointBlochM2_gauge_rayleigh_eq_zero⟩
499
500def ExactMidpointM2TTIdentityProved : Bool := true
501theorem exactMidpointM2TTIdentityProved_true :
502 ExactMidpointM2TTIdentityProved = true := rfl
503
504end
505
506end ReggeExactMidpointM2TTIdentity4D
507end Analysis
508end Gravity
509end IndisputableMonolith
510