IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
IndisputableMonolith/Gravity/Analysis/ReggeEdgeStencil4D.lean · 449 lines · 57 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4D
3
4/-!
5# Regge edge stencil (4D): Freudenthal 4-cube classes + provisional finite quadratic
6
7QG full-theory campaign, next kernel-checked increment after
8`ReggeEdgeTTAttachment4D`: the 4D analogue of the 3D chain's finite TT
9edge-class packaging (`polEdgeCoeff` / hinge-diagonal block ingredients in
10`ReggeTTSymbolPreflight` and `ReggeTTHingeAwareZeroMode`).
11
12## Tier tags (binding)
13
14* THEOREM: every named result in this file (kernel-checked; no `sorry`,
15 no `admit`, no new axioms, no `native_decide`, no `: True` shells).
16* OPEN: the class weights of the true 4D Regge Hessian at flat. The
17 provisional aggregate below uses weight `1` on every nonzero 0/1
18 displacement class. Deriving the correct 4D Regge weights (the 4D
19 lift of the 3D hinge factor `-1/(4 ℓ² √ℓ²)` contracted with deficit
20 incidence) is **not** done here and must not be reverse-engineered
21 from the Einstein-Hilbert answer.
22* This does **not** prove `S_RS_converges_EH_4d`.
23* This does **not** prove the ledger name `edge_tt_decomposition` in full.
24* This does **not** flip `gap_action_recovery`.
25
26## What is proved (honest scope)
27
281. **15 Freudenthal-style edge classes.** Nonzero displacement vectors in
29 `{0,1}⁴`, indexed by `Fin 15` via bit masks `d.val + 1`.
302. **Plane-wave midpoint loading.** Per class, squared-length coefficient
31 `classCoeff H d = Dᵀ H D` (same convention as 3D `polEdgeCoeff` /
32 4D `edgeLoad`) times `cos(m·x + m·D/2)`.
333. **Provisional finite quadratic aggregate.**
34 `finiteTTQuadratic H = Σ_d (classCoeff H d)²` with all-ones weights
35 (OPEN for true Regge weights). Exact polarization identity in `H`.
364. **Gauge entry (exact, non-fake).** Pure gauge loads by
37 `classCoeff (gaugePart m v) d = 2 (m·D)(v·D)`, so the provisional
38 aggregate on pure gauge is `Σ_d 4 (m·D)² (v·D)²`, which is **not**
39 identically zero. Exact gauge invariance of this provisional
40 aggregate therefore fails; the identity that holds is recorded, and
41 an explicit TT + gauge counterexample is given.
425. **Nonvacuity + decoys.** The aggregate is `8` on `axisTTPlus`;
43 pure-gauge and pure-trace inputs evaluate to the distinct predicted
44 values `32` and `80`.
45
46Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
47-/
48
49namespace IndisputableMonolith
50namespace Gravity
51namespace Analysis
52namespace ReggeEdgeStencil4D
53
54open Matrix BigOperators
55open EdgeTTDecomposition4D
56open ReggeEdgeTTAttachment4D
57
58noncomputable section
59
60/-! ## §1. Fifteen nonzero 0/1 displacement classes of the 4-cube -/
61
62/-- Bit-mask of class `d`: the integer `d.val + 1 ∈ {1,…,15}`. -/
63def maskOf (d : Fin 15) : ℕ := d.val + 1
64
65/-- Whether coordinate `i` is set in the 0/1 displacement of class `d`. -/
66def classBit (d : Fin 15) (i : Fin 4) : Bool :=
67 Nat.testBit (maskOf d) i.val
68
69/-- Displacement vector of class `d` (entries in `{0,1}`). -/
70def classDisp (d : Fin 15) : Fin 4 → ℝ :=
71 fun i => if classBit d i then (1 : ℝ) else 0
72
73/-- Flat squared length of class `d` (Hamming weight of the mask). -/
74def classDispSq (d : Fin 15) : ℝ :=
75 ∑ i : Fin 4, classDisp d i * classDisp d i
76
77/-- Nat Hamming weight of the class mask (bits 0..3). -/
78def classWeightNat (d : Fin 15) : ℕ :=
79 (if classBit d 0 then 1 else 0) +
80 (if classBit d 1 then 1 else 0) +
81 (if classBit d 2 then 1 else 0) +
82 (if classBit d 3 then 1 else 0)
83
84theorem classWeightNat_pos (d : Fin 15) : 0 < classWeightNat d := by
85 fin_cases d <;> decide
86
87theorem classDisp_ne_zero (d : Fin 15) : classDisp d ≠ 0 := by
88 intro h
89 have hw := classWeightNat_pos d
90 have hbits :
91 classWeightNat d =
92 (if classBit d 0 then 1 else 0) +
93 (if classBit d 1 then 1 else 0) +
94 (if classBit d 2 then 1 else 0) +
95 (if classBit d 3 then 1 else 0) := rfl
96 have hz : ∀ i : Fin 4, classDisp d i = 0 := by
97 intro i; simp [h]
98 have hb0 : classBit d 0 = false := by
99 have := hz 0; simp [classDisp] at this; exact this
100 have hb1 : classBit d 1 = false := by
101 have := hz 1; simp [classDisp] at this; exact this
102 have hb2 : classBit d 2 = false := by
103 have := hz 2; simp [classDisp] at this; exact this
104 have hb3 : classBit d 3 = false := by
105 have := hz 3; simp [classDisp] at this; exact this
106 simp [hbits, hb0, hb1, hb2, hb3] at hw
107
108theorem classDispSq_eq_weight (d : Fin 15) :
109 classDispSq d = (classWeightNat d : ℝ) := by
110 unfold classDispSq classDisp classWeightNat
111 simp [Fin.sum_univ_four]
112 cases classBit d 0 <;> cases classBit d 1 <;>
113 cases classBit d 2 <;> cases classBit d 3 <;> norm_num
114
115/-! ## §2. Class coefficients and midpoint plane-wave perturbations -/
116
117/-- Edge-class coefficient: `c_d(H) = Dᵀ H D` (3D `polEdgeCoeff` convention). -/
118def classCoeff (H : Mat4) (d : Fin 15) : ℝ :=
119 edgeLoad H (classDisp d)
120
121/-- Midpoint Bloch phase of class `d` based at covering coordinate `x`:
122`m · (x + D/2)`. -/
123def classMidpointPhase (m x : Fin 4 → ℝ) (d : Fin 15) : ℝ :=
124 (∑ i : Fin 4, m i * x i) + (∑ i : Fin 4, m i * classDisp d i) / 2
125
126/-- Plane-wave squared-length perturbation of class `d`:
127`c_d(H) · cos(m·x + m·D/2)`. -/
128def planeWaveClassPert (H : Mat4) (m x : Fin 4 → ℝ) (d : Fin 15) : ℝ :=
129 classCoeff H d * Real.cos (classMidpointPhase m x d)
130
131theorem classCoeff_add (A B : Mat4) (d : Fin 15) :
132 classCoeff (A + B) d = classCoeff A d + classCoeff B d := by
133 unfold classCoeff; exact edgeLoad_add A B _
134
135theorem classCoeff_smul (c : ℝ) (H : Mat4) (d : Fin 15) :
136 classCoeff (c • H) d = c * classCoeff H d := by
137 unfold classCoeff; exact edgeLoad_smul c H _
138
139theorem classCoeff_neg (H : Mat4) (d : Fin 15) :
140 classCoeff (-H) d = -classCoeff H d := by
141 unfold classCoeff; exact edgeLoad_neg H _
142
143theorem classCoeff_sub (A B : Mat4) (d : Fin 15) :
144 classCoeff (A - B) d = classCoeff A d - classCoeff B d := by
145 unfold classCoeff; exact edgeLoad_sub A B _
146
147theorem planeWaveClassPert_add (A B : Mat4) (m x : Fin 4 → ℝ) (d : Fin 15) :
148 planeWaveClassPert (A + B) m x d =
149 planeWaveClassPert A m x d + planeWaveClassPert B m x d := by
150 unfold planeWaveClassPert
151 rw [classCoeff_add, add_mul]
152
153theorem planeWaveClassPert_smul (c : ℝ) (H : Mat4) (m x : Fin 4 → ℝ)
154 (d : Fin 15) :
155 planeWaveClassPert (c • H) m x d = c * planeWaveClassPert H m x d := by
156 unfold planeWaveClassPert
157 rw [classCoeff_smul, mul_assoc]
158
159/-! ## §3. Provisional finite quadratic aggregate (weight 1; OPEN) -/
160
161/-- Symmetric bilinear polarization of the provisional aggregate. -/
162def finiteTTBilinear (A B : Mat4) : ℝ :=
163 ∑ d : Fin 15, classCoeff A d * classCoeff B d
164
165/-- Provisional finite TT quadratic form on edge classes:
166`Q(H) = Σ_d w_d c_d(H)²` with provisional weights `w_d = 1` for every
167nonzero 0/1 class. **OPEN:** replace `w_d` by the true 4D Regge
168flat-Hessian class weights when derived; do not fit them to EH. -/
169def finiteTTQuadratic (H : Mat4) : ℝ :=
170 ∑ d : Fin 15, classCoeff H d ^ 2
171
172theorem finiteTTQuadratic_eq_bilinear (H : Mat4) :
173 finiteTTQuadratic H = finiteTTBilinear H H := by
174 unfold finiteTTQuadratic finiteTTBilinear
175 refine Finset.sum_congr rfl fun d _ => by ring
176
177theorem finiteTTBilinear_symm (A B : Mat4) :
178 finiteTTBilinear A B = finiteTTBilinear B A := by
179 unfold finiteTTBilinear
180 refine Finset.sum_congr rfl fun d _ => mul_comm _ _
181
182theorem finiteTTBilinear_add_left (A₁ A₂ B : Mat4) :
183 finiteTTBilinear (A₁ + A₂) B =
184 finiteTTBilinear A₁ B + finiteTTBilinear A₂ B := by
185 unfold finiteTTBilinear
186 simp_rw [classCoeff_add, add_mul, Finset.sum_add_distrib]
187
188theorem finiteTTBilinear_smul_left (c : ℝ) (A B : Mat4) :
189 finiteTTBilinear (c • A) B = c * finiteTTBilinear A B := by
190 unfold finiteTTBilinear
191 simp_rw [classCoeff_smul, mul_assoc, ← Finset.mul_sum]
192
193/-- Exact quadratic expansion / polarization identity. -/
194theorem finiteTTQuadratic_add (A B : Mat4) :
195 finiteTTQuadratic (A + B) =
196 finiteTTQuadratic A + finiteTTQuadratic B + 2 * finiteTTBilinear A B := by
197 unfold finiteTTQuadratic finiteTTBilinear
198 have h :
199 ∀ d : Fin 15,
200 classCoeff (A + B) d ^ 2 =
201 classCoeff A d ^ 2 + classCoeff B d ^ 2 +
202 2 * (classCoeff A d * classCoeff B d) := by
203 intro d
204 rw [classCoeff_add]
205 ring
206 simp_rw [h, Finset.sum_add_distrib, Finset.mul_sum]
207
208theorem finiteTTQuadratic_smul (c : ℝ) (H : Mat4) :
209 finiteTTQuadratic (c • H) = c ^ 2 * finiteTTQuadratic H := by
210 unfold finiteTTQuadratic
211 simp_rw [classCoeff_smul]
212 -- (c * a)^2 = c^2 * a^2
213 have h : ∀ d : Fin 15, (c * classCoeff H d) ^ 2 = c ^ 2 * classCoeff H d ^ 2 := by
214 intro d; ring
215 simp_rw [h, ← Finset.mul_sum]
216
217theorem finiteTTQuadratic_neg (H : Mat4) :
218 finiteTTQuadratic (-H) = finiteTTQuadratic H := by
219 have h := finiteTTQuadratic_smul (-1) H
220 simpa [neg_one_smul] using h
221
222/-! ## §4. Gauge entry at the exact finite-difference level -/
223
224theorem classCoeff_gaugePart (m v : Fin 4 → ℝ) (d : Fin 15) :
225 classCoeff (gaugePart m v) d =
226 2 * (∑ i : Fin 4, m i * classDisp d i) *
227 (∑ j : Fin 4, v j * classDisp d j) := by
228 unfold classCoeff
229 exact edgeLoad_gaugePart m v _
230
231/-- Exact pure-gauge evaluation of the provisional aggregate.
232This is **not** identically zero, so the provisional weight-1 aggregate
233is **not** gauge-invariant. -/
234theorem finiteTTQuadratic_gaugePart (m v : Fin 4 → ℝ) :
235 finiteTTQuadratic (gaugePart m v) =
236 ∑ d : Fin 15,
237 4 * (∑ i : Fin 4, m i * classDisp d i) ^ 2 *
238 (∑ j : Fin 4, v j * classDisp d j) ^ 2 := by
239 unfold finiteTTQuadratic
240 refine Finset.sum_congr rfl fun d _ => ?_
241 rw [classCoeff_gaugePart]
242 ring
243
244/-- Explicit pure-gauge witness vector along axis 0. -/
245def axisGaugeVector : Fin 4 → ℝ
246 | 0 => 1
247 | 1 => 0
248 | 2 => 0
249 | 3 => 0
250
251theorem classCoeff_gaugePart_axis (d : Fin 15) :
252 classCoeff (gaugePart axisWave axisGaugeVector) d =
253 2 * (if classBit d 0 then (1 : ℝ) else 0) := by
254 rw [classCoeff_gaugePart]
255 have hm :
256 (∑ i : Fin 4, axisWave i * classDisp d i) =
257 if classBit d 0 then (1 : ℝ) else 0 := by
258 simp [axisWave, classDisp, Fin.sum_univ_four]
259 have hv :
260 (∑ j : Fin 4, axisGaugeVector j * classDisp d j) =
261 if classBit d 0 then (1 : ℝ) else 0 := by
262 simp [axisGaugeVector, classDisp, Fin.sum_univ_four]
263 rw [hm, hv]
264 cases classBit d 0 <;> norm_num
265
266/-- Nat indicator: class has bit 0 set. -/
267def hasBit0 (d : Fin 15) : ℕ := if classBit d 0 then 1 else 0
268
269theorem sum_hasBit0 : (∑ d : Fin 15, hasBit0 d) = 8 := by
270 unfold hasBit0 classBit maskOf
271 decide
272
273theorem finiteTTQuadratic_gaugePart_axisWave :
274 finiteTTQuadratic (gaugePart axisWave axisGaugeVector) = 32 := by
275 unfold finiteTTQuadratic
276 have hterm :
277 ∀ d : Fin 15,
278 classCoeff (gaugePart axisWave axisGaugeVector) d ^ 2 =
279 (4 : ℝ) * (hasBit0 d : ℝ) := by
280 intro d
281 rw [classCoeff_gaugePart_axis]
282 unfold hasBit0
283 cases classBit d 0 <;> norm_num
284 simp_rw [hterm, ← Finset.mul_sum, ← Nat.cast_sum, sum_hasBit0]
285 norm_num
286
287theorem finiteTTQuadratic_gaugePart_axisWave_ne_zero :
288 finiteTTQuadratic (gaugePart axisWave axisGaugeVector) ≠ 0 := by
289 rw [finiteTTQuadratic_gaugePart_axisWave]
290 norm_num
291
292/-! ## §5. Axis-TTPlus coefficients and nonvacuity -/
293
294theorem classCoeff_axisTTPlus (d : Fin 15) :
295 classCoeff axisTTPlus d =
296 (if classBit d 2 then (1 : ℝ) else 0) -
297 if classBit d 3 then (1 : ℝ) else 0 := by
298 unfold classCoeff edgeLoad axisTTPlus classDisp
299 simp [Fin.sum_univ_four]
300 split_ifs <;> ring
301
302/-- Cross polarization class coefficient: `Dᵀ H_× D = 2 D₂ D₃`. -/
303theorem classCoeff_axisTTCross (d : Fin 15) :
304 classCoeff axisTTCross d =
305 2 * (if classBit d 2 then (1 : ℝ) else 0) *
306 (if classBit d 3 then (1 : ℝ) else 0) := by
307 unfold classCoeff edgeLoad axisTTCross classDisp
308 simp [Fin.sum_univ_four]
309 split_ifs <;> ring
310
311/-- Nat square of the plus-class coefficient (0 or 1). -/
312def axisTTPlusSqNat (d : Fin 15) : ℕ :=
313 if classBit d 2 ≠ classBit d 3 then 1 else 0
314
315theorem classCoeff_axisTTPlus_sq (d : Fin 15) :
316 classCoeff axisTTPlus d ^ 2 = (axisTTPlusSqNat d : ℝ) := by
317 rw [classCoeff_axisTTPlus]
318 unfold axisTTPlusSqNat
319 cases classBit d 2 <;> cases classBit d 3 <;> norm_num
320
321theorem sum_axisTTPlusSqNat : (∑ d : Fin 15, axisTTPlusSqNat d) = 8 := by
322 unfold axisTTPlusSqNat classBit maskOf
323 decide
324
325theorem finiteTTQuadratic_axisTTPlus : finiteTTQuadratic axisTTPlus = 8 := by
326 unfold finiteTTQuadratic
327 simp_rw [classCoeff_axisTTPlus_sq, ← Nat.cast_sum, sum_axisTTPlusSqNat]
328 norm_num
329
330theorem finiteTTQuadratic_axisTTPlus_ne_zero :
331 finiteTTQuadratic axisTTPlus ≠ 0 := by
332 rw [finiteTTQuadratic_axisTTPlus]
333 norm_num
334
335theorem finiteTTQuadratic_axisTTPlus_isTT_seed :
336 IsTT axisWave axisTTPlus ∧ finiteTTQuadratic axisTTPlus ≠ 0 :=
337 ⟨axisTTPlus_isTT, finiteTTQuadratic_axisTTPlus_ne_zero⟩
338
339/-! ## §6. Gauge non-invariance on a TT seed -/
340
341/-- Cross-term Nat contribution `c₊(d) · (c_g(d)/2)` equals 0 in the sum
342(the signed products cancel). -/
343def crossNat (d : Fin 15) : ℤ :=
344 let cPlus : ℤ :=
345 (if classBit d 2 then (1 : ℤ) else 0) - if classBit d 3 then 1 else 0
346 let cG : ℤ := if classBit d 0 then 1 else 0
347 cPlus * cG
348
349theorem sum_crossNat : (∑ d : Fin 15, crossNat d) = 0 := by
350 unfold crossNat classBit maskOf
351 decide
352
353theorem finiteTTBilinear_axisTTPlus_gauge :
354 finiteTTBilinear axisTTPlus (gaugePart axisWave axisGaugeVector) = 0 := by
355 unfold finiteTTBilinear
356 have hterm :
357 ∀ d : Fin 15,
358 classCoeff axisTTPlus d *
359 classCoeff (gaugePart axisWave axisGaugeVector) d =
360 (2 : ℝ) * (crossNat d : ℝ) := by
361 intro d
362 rw [classCoeff_axisTTPlus, classCoeff_gaugePart_axis]
363 unfold crossNat
364 cases classBit d 0 <;> cases classBit d 2 <;>
365 cases classBit d 3 <;> norm_num
366 simp_rw [hterm, ← Finset.mul_sum, ← Int.cast_sum, sum_crossNat]
367 norm_num
368
369/-- THEOREM: provisional aggregate fails exact gauge invariance on a TT seed.
370`axisTTPlus` is TT for `axisWave`, yet adding the pure axis gauge changes `Q`. -/
371theorem finiteTTQuadratic_not_gauge_invariant_on_axisTTPlus :
372 finiteTTQuadratic (axisTTPlus + gaugePart axisWave axisGaugeVector) ≠
373 finiteTTQuadratic axisTTPlus := by
374 rw [finiteTTQuadratic_add, finiteTTBilinear_axisTTPlus_gauge,
375 finiteTTQuadratic_gaugePart_axisWave]
376 rw [finiteTTQuadratic_axisTTPlus]
377 norm_num
378
379/-! ## §7. Decoys: pure gauge and pure trace -/
380
381/-- Pure-gauge decoy. -/
382def decoyGauge : Mat4 := gaugePart axisWave axisGaugeVector
383
384theorem finiteTTQuadratic_decoyGauge : finiteTTQuadratic decoyGauge = 32 := by
385 unfold decoyGauge
386 exact finiteTTQuadratic_gaugePart_axisWave
387
388/-- Pure-trace decoy: the Euclidean identity (not TT). -/
389def decoyTrace : Mat4 := 1
390
391theorem classCoeff_decoyTrace (d : Fin 15) :
392 classCoeff decoyTrace d = classDispSq d := by
393 unfold classCoeff decoyTrace classDispSq edgeLoad
394 -- Dᵀ I D = |D|²
395 simp [one_apply, Fin.sum_univ_four, classDisp]
396
397theorem classCoeff_decoyTrace_sq (d : Fin 15) :
398 classCoeff decoyTrace d ^ 2 = (classWeightNat d : ℝ) ^ 2 := by
399 rw [classCoeff_decoyTrace, classDispSq_eq_weight]
400
401theorem sum_weightSqNat : (∑ d : Fin 15, classWeightNat d ^ 2) = 80 := by
402 unfold classWeightNat classBit maskOf
403 decide
404
405theorem finiteTTQuadratic_decoyTrace : finiteTTQuadratic decoyTrace = 80 := by
406 unfold finiteTTQuadratic
407 simp_rw [classCoeff_decoyTrace_sq]
408 -- Σ (n : ℝ)^2 = Σ (n^2 : ℝ)
409 have h : ∀ d : Fin 15, ((classWeightNat d : ℝ) ^ 2) = ((classWeightNat d ^ 2 : ℕ) : ℝ) := by
410 intro d; norm_cast
411 simp_rw [h, ← Nat.cast_sum, sum_weightSqNat]
412 norm_num
413
414theorem decoy_values_distinct :
415 finiteTTQuadratic decoyGauge ≠ finiteTTQuadratic decoyTrace ∧
416 finiteTTQuadratic decoyGauge ≠ finiteTTQuadratic axisTTPlus ∧
417 finiteTTQuadratic decoyTrace ≠ finiteTTQuadratic axisTTPlus := by
418 rw [finiteTTQuadratic_decoyGauge, finiteTTQuadratic_decoyTrace,
419 finiteTTQuadratic_axisTTPlus]
420 norm_num
421
422/-! ## §8. Axis class recovers the attachment layer -/
423
424theorem classDisp_axis0 : classDisp (0 : Fin 15) = axisDisp 0 := by
425 funext i
426 fin_cases i <;> simp [classDisp, classBit, maskOf, axisDisp, Nat.testBit]
427
428theorem classCoeff_axis0 (H : Mat4) :
429 classCoeff H (0 : Fin 15) = edgeLoad H (axisDisp 0) := by
430 unfold classCoeff
431 rw [classDisp_axis0]
432
433theorem planeWaveClassPert_axis0 (H : Mat4) (m x : Fin 4 → ℝ) :
434 planeWaveClassPert H m x (0 : Fin 15) =
435 planeWaveAxisEdgePert H m x 0 := by
436 unfold planeWaveClassPert planeWaveAxisEdgePert classCoeff classMidpointPhase
437 axisMidpointPhase
438 rw [classDisp_axis0]
439 have hdot : (∑ i : Fin 4, m i * axisDisp 0 i) = m 0 := by
440 unfold axisDisp; simp [Finset.sum_ite_eq']
441 rw [hdot]
442
443end
444
445end ReggeEdgeStencil4D
446end Analysis
447end Gravity
448end IndisputableMonolith
449