IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DFlatKernel.lean · 423 lines · 48 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
3
4/-!
5# Regge 4D Freudenthal hinge incidence + flat-Hessian assembly skeleton
6
7QG full-theory campaign, next kernel-checked increment after
8`ReggeEdgeStencil4D`. The 15-class stencil is imported, never redefined.
9
10## Tier tags (binding)
11
12* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
13 `admit`, no new axioms, no `native_decide`, no `: True` shells).
14* MODEL: the flat-Hessian assembly formula (definition only; OPEN
15 per-hinge deficit / area kernels are parameters, not evaluated).
16* OPEN: the true per-hinge flat second-variation kernels — the dihedral /
17 Cayley–Menger calculus that supplies numeric class weights.
18* This does **not** complete the flat Hessian of the 4D Regge action.
19* This does **not** prove `S_RS_converges_EH_4d`.
20* This does **not** flip `gap_action_recovery`.
21* This does **not** reverse-engineer weights from Einstein–Hilbert.
22
23## What is proved (honest scope: deliverable B, with A-shaped gates
24on the combinatorial support)
25
261. **Freudenthal / Kuhn 4-cube cell.** Explicit enumeration of the 24
27 monotone 4-simplices (permutations of the four axes) and their
28 five nested vertices / ten edge-class masks (among the 15 of
29 `ReggeEdgeStencil4D`).
302. **Seed hinge orbit.** The triangle with vertices `0`, `e₀`,
31 `e₀+e₁` (masks `0,1,3`). Exactly two of the 24 simplices contain
32 it; they are the permutations that begin `(0,1,…)`.
333. **Incidence multiplicities.** For each of the 15 edge classes, the
34 number of containing seed-simplices in which that class appears as
35 a local edge. Three classes are absent (combinatorial decoys);
36 the three hinge-boundary classes each have multiplicity `2`.
374. **Nonvacuity / symmetry / decoy (combinatorial).** The incidence
38 support is nonempty; it is invariant under the axis swap `2 ↔ 3`
39 that fixes the seed hinge; three explicit classes lie outside the
40 support.
415. **Assembly skeleton (MODEL).** The flat-Hessian class form that
42 contracts OPEN per-hinge area weights against OPEN per-hinge
43 deficit kernels, forced to vanish off the incidence support.
44
45## What remains for the true weights
46
47Lift the 3D Schläfli-reduced chain of `ReggeTTFlatSecondVariation` to
484D: for this seed hinge (then every orbit), express the dihedral angle
49at the triangle in each incident 4-simplex as a Cayley–Menger / cosine
50function of the ten squared edge lengths, differentiate at the flat
51Freudenthal point, and assemble `d²S = Σ_h dA_h · dδ_h` into class
52weights on the 15-stencil. The incidence table here is the
53combinatorial factor those kernels must contract against.
54
55Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
56-/
57
58namespace IndisputableMonolith
59namespace Gravity
60namespace Analysis
61namespace ReggeHinge4DFlatKernel
62
63open BigOperators
64open ReggeEdgeStencil4D
65
66/-! ## §1. Freudenthal / Kuhn 24-simplex cell -/
67
68/-- Lexicographic enumeration of the 24 permutations of `Fin 4`:
69`permAxes s = (σ(0), σ(1), σ(2), σ(3))`. -/
70def permAxes : Fin 24 → Fin 4 × Fin 4 × Fin 4 × Fin 4
71 | 0 => (0, 1, 2, 3)
72 | 1 => (0, 1, 3, 2)
73 | 2 => (0, 2, 1, 3)
74 | 3 => (0, 2, 3, 1)
75 | 4 => (0, 3, 1, 2)
76 | 5 => (0, 3, 2, 1)
77 | 6 => (1, 0, 2, 3)
78 | 7 => (1, 0, 3, 2)
79 | 8 => (1, 2, 0, 3)
80 | 9 => (1, 2, 3, 0)
81 | 10 => (1, 3, 0, 2)
82 | 11 => (1, 3, 2, 0)
83 | 12 => (2, 0, 1, 3)
84 | 13 => (2, 0, 3, 1)
85 | 14 => (2, 1, 0, 3)
86 | 15 => (2, 1, 3, 0)
87 | 16 => (2, 3, 0, 1)
88 | 17 => (2, 3, 1, 0)
89 | 18 => (3, 0, 1, 2)
90 | 19 => (3, 0, 2, 1)
91 | 20 => (3, 1, 0, 2)
92 | 21 => (3, 1, 2, 0)
93 | 22 => (3, 2, 0, 1)
94 | 23 => (3, 2, 1, 0)
95 | ⟨n + 24, h⟩ => absurd h (by omega)
96
97/-- Axis image `σ(i)` for simplex `s`. -/
98def permOf (s : Fin 24) (i : Fin 4) : Fin 4 :=
99 match i, permAxes s with
100 | 0, (a, _, _, _) => a
101 | 1, (_, b, _, _) => b
102 | 2, (_, _, c, _) => c
103 | 3, (_, _, _, d) => d
104
105/-- Bit mask of the standard basis vector `e_i`. -/
106def axisMask (i : Fin 4) : ℕ := 2 ^ i.val
107
108/-- Nested Freudenthal vertex after `k` steps along simplex `s`
109(bit mask in `{0,…,15}`). -/
110def vertexMask (s : Fin 24) : Fin 5 → ℕ
111 | 0 => 0
112 | 1 => axisMask (permOf s 0)
113 | 2 => axisMask (permOf s 0) + axisMask (permOf s 1)
114 | 3 =>
115 axisMask (permOf s 0) + axisMask (permOf s 1) + axisMask (permOf s 2)
116 | 4 => 15
117
118theorem vertexMask_start (s : Fin 24) : vertexMask s 0 = 0 := rfl
119
120theorem vertexMask_end (s : Fin 24) : vertexMask s 4 = 15 := rfl
121
122/-- Local 4-simplex edge slots: the ten pairs among five vertices. -/
123def localEdgePair : Fin 10 → Fin 5 × Fin 5
124 | 0 => (0, 1)
125 | 1 => (0, 2)
126 | 2 => (0, 3)
127 | 3 => (0, 4)
128 | 4 => (1, 2)
129 | 5 => (1, 3)
130 | 6 => (1, 4)
131 | 7 => (2, 3)
132 | 8 => (2, 4)
133 | 9 => (3, 4)
134 | ⟨n + 10, h⟩ => absurd h (by omega)
135
136/-- XOR mask of local edge `e` in simplex `s`. -/
137def localEdgeMask (s : Fin 24) (e : Fin 10) : ℕ :=
138 let p := localEdgePair e
139 Nat.xor (vertexMask s p.1) (vertexMask s p.2)
140
141theorem localEdgeMask_bounds (s : Fin 24) (e : Fin 10) :
142 0 < localEdgeMask s e ∧ localEdgeMask s e ≤ 15 := by
143 fin_cases s <;> fin_cases e <;> decide
144
145/-- Local edge class of slot `e` in simplex `s`. -/
146def localEdgeClass (s : Fin 24) (e : Fin 10) : Fin 15 :=
147 ⟨localEdgeMask s e - 1, by
148 have h := localEdgeMask_bounds s e
149 omega⟩
150
151theorem localEdgeClass_mask (s : Fin 24) (e : Fin 10) :
152 maskOf (localEdgeClass s e) = localEdgeMask s e := by
153 unfold localEdgeClass maskOf
154 have h := (localEdgeMask_bounds s e).1
155 exact Nat.sub_add_cancel h
156
157/-- Whether simplex `s` carries edge class `d` among its ten local edges. -/
158def simplexHasClass (s : Fin 24) (d : Fin 15) : Bool :=
159 decide (∃ e : Fin 10, localEdgeClass s e = d)
160
161theorem permOf_eq_of_eq (s : Fin 24) {i j : Fin 4}
162 (h : permOf s i = permOf s j) : i = j := by
163 fin_cases s <;> fin_cases i <;> fin_cases j <;>
164 first | rfl | exact (nomatch h)
165
166/-! ## §2. Seed hinge orbit `{0, e₀, e₀+e₁}` -/
167
168/-- Whether the five vertices of simplex `s` contain the seed hinge
169masks `{0,1,3}`. -/
170def containsSeedHinge (s : Fin 24) : Bool :=
171 decide (∃ i : Fin 5, vertexMask s i = 1) &&
172 decide (∃ i : Fin 5, vertexMask s i = 3)
173
174/-- THEOREM: the seed hinge sits in simplex `s` iff the permutation
175begins with axes `(0,1)`. -/
176theorem containsSeedHinge_iff (s : Fin 24) :
177 containsSeedHinge s = true ↔ permOf s 0 = 0 ∧ permOf s 1 = 1 := by
178 fin_cases s <;> decide
179
180/-- THEOREM: exactly two of the 24 Freudenthal simplices contain the
181seed hinge. -/
182theorem seedHinge_simplex_count :
183 (Finset.univ.filter (fun s : Fin 24 => containsSeedHinge s = true)).card =
184 2 := by
185 decide
186
187/-- THEOREM: those two simplices are indices `0` and `1`. -/
188theorem seedHinge_simplices :
189 Finset.univ.filter (fun s : Fin 24 => containsSeedHinge s = true) =
190 ({0, 1} : Finset (Fin 24)) := by
191 decide
192
193/-! ## §3. Incidence multiplicities on the 15 edge classes -/
194
195/-- Edge-class set of Freudenthal simplex `0` = perm `(0,1,2,3)`. -/
196def simplex0Classes : Finset (Fin 15) :=
197 {0, 1, 2, 3, 5, 6, 7, 11, 13, 14}
198
199/-- Edge-class set of Freudenthal simplex `1` = perm `(0,1,3,2)`. -/
200def simplex1Classes : Finset (Fin 15) :=
201 {0, 1, 2, 3, 7, 9, 10, 11, 13, 14}
202
203/-- THEOREM: the table for simplex `0` matches the computed local edges. -/
204theorem simplex0Classes_correct (e : Fin 10) :
205 localEdgeClass 0 e ∈ simplex0Classes := by
206 fin_cases e <;> decide
207
208/-- THEOREM: the table for simplex `1` matches the computed local edges. -/
209theorem simplex1Classes_correct (e : Fin 10) :
210 localEdgeClass 1 e ∈ simplex1Classes := by
211 fin_cases e <;> decide
212
213/-- THEOREM: every class in the simplex-`0` table is realized by some slot. -/
214theorem simplex0Classes_complete (d : Fin 15) (hd : d ∈ simplex0Classes) :
215 simplexHasClass 0 d = true := by
216 revert hd
217 fin_cases d <;> decide
218
219/-- THEOREM: every class in the simplex-`1` table is realized by some slot. -/
220theorem simplex1Classes_complete (d : Fin 15) (hd : d ∈ simplex1Classes) :
221 simplexHasClass 1 d = true := by
222 revert hd
223 fin_cases d <;> decide
224
225/-- Combinatorial incidence: how many seed-containing simplices carry class `d`. -/
226def seedHingeIncidenceNat (d : Fin 15) : ℕ :=
227 (if d ∈ simplex0Classes then 1 else 0) +
228 (if d ∈ simplex1Classes then 1 else 0)
229
230/-- Closed-form incidence values. -/
231theorem seedHingeIncidenceNat_values :
232 seedHingeIncidenceNat ⟨0, by decide⟩ = 2 ∧
233 seedHingeIncidenceNat ⟨1, by decide⟩ = 2 ∧
234 seedHingeIncidenceNat ⟨2, by decide⟩ = 2 ∧
235 seedHingeIncidenceNat ⟨3, by decide⟩ = 2 ∧
236 seedHingeIncidenceNat ⟨4, by decide⟩ = 0 ∧
237 seedHingeIncidenceNat ⟨5, by decide⟩ = 1 ∧
238 seedHingeIncidenceNat ⟨6, by decide⟩ = 1 ∧
239 seedHingeIncidenceNat ⟨7, by decide⟩ = 2 ∧
240 seedHingeIncidenceNat ⟨8, by decide⟩ = 0 ∧
241 seedHingeIncidenceNat ⟨9, by decide⟩ = 1 ∧
242 seedHingeIncidenceNat ⟨10, by decide⟩ = 1 ∧
243 seedHingeIncidenceNat ⟨11, by decide⟩ = 2 ∧
244 seedHingeIncidenceNat ⟨12, by decide⟩ = 0 ∧
245 seedHingeIncidenceNat ⟨13, by decide⟩ = 2 ∧
246 seedHingeIncidenceNat ⟨14, by decide⟩ = 2 := by
247 decide
248
249/-- Total incidence mass on the seed hinge (= 2 simplices × 10 edges). -/
250theorem sum_seedHingeIncidenceNat :
251 (∑ d : Fin 15, seedHingeIncidenceNat d) = 20 := by
252 unfold seedHingeIncidenceNat simplex0Classes simplex1Classes
253 decide
254
255/-! ## §4. Nonvacuity, symmetry, decoy (combinatorial A-shaped gates) -/
256
257/-- THEOREM (nonvacuity): class `0` (hinge-boundary edge `e₀`) has
258multiplicity `2`. -/
259theorem seedHingeIncidence_nonvacuous :
260 seedHingeIncidenceNat (0 : Fin 15) = 2 ∧
261 seedHingeIncidenceNat (0 : Fin 15) ≠ 0 := by
262 decide
263
264/-- Bit-mask image under the axis swap `2 ↔ 3`. -/
265def swap23Mask (m : ℕ) : ℕ :=
266 (if Nat.testBit m 0 then 1 else 0) +
267 (if Nat.testBit m 1 then 2 else 0) +
268 (if Nat.testBit m 2 then 8 else 0) +
269 (if Nat.testBit m 3 then 4 else 0)
270
271theorem swap23Mask_bounds (d : Fin 15) :
272 0 < swap23Mask (maskOf d) ∧ swap23Mask (maskOf d) ≤ 15 := by
273 fin_cases d <;> decide
274
275/-- Class image under axis swap `2 ↔ 3`. -/
276def swap23Class (d : Fin 15) : Fin 15 :=
277 ⟨swap23Mask (maskOf d) - 1, by
278 have h := swap23Mask_bounds d
279 omega⟩
280
281/-- THEOREM (symmetry): seed-hinge incidence is invariant under the
282lattice symmetry that swaps axes `2` and `3` and fixes the hinge. -/
283theorem seedHingeIncidence_swap23 (d : Fin 15) :
284 seedHingeIncidenceNat (swap23Class d) = seedHingeIncidenceNat d := by
285 fin_cases d <;> decide
286
287/-- Combinatorial decoy classes: masks `5,9,13` (classes `4,8,12`). -/
288def decoyClass4 : Fin 15 := ⟨4, by decide⟩
289def decoyClass8 : Fin 15 := ⟨8, by decide⟩
290def decoyClass12 : Fin 15 := ⟨12, by decide⟩
291
292/-- THEOREM (decoy): three explicit edge classes have zero seed-hinge
293incidence. -/
294theorem seedHingeIncidence_decoy_zero :
295 seedHingeIncidenceNat decoyClass4 = 0 ∧
296 seedHingeIncidenceNat decoyClass8 = 0 ∧
297 seedHingeIncidenceNat decoyClass12 = 0 := by
298 decide
299
300/-- Hinge-boundary edge classes of the seed triangle. -/
301def hingeBoundaryClass : Fin 3 → Fin 15
302 | 0 => 0
303 | 1 => 1
304 | 2 => 2
305
306/-- THEOREM: every seed-hinge boundary class has positive incidence. -/
307theorem hingeBoundary_incidence_pos (i : Fin 3) :
308 0 < seedHingeIncidenceNat (hingeBoundaryClass i) := by
309 fin_cases i <;> decide
310
311/-! ## §5. Full-cell edge-class inventory (sanity) -/
312
313/-- Whether class `d` appears in simplex `s` (Nat indicator). -/
314def classInSimplexNat (s : Fin 24) (d : Fin 15) : ℕ :=
315 if simplexHasClass s d then 1 else 0
316
317/-- Every Freudenthal 4-simplex carries exactly ten edge classes. -/
318theorem simplex_class_count (s : Fin 24) :
319 (∑ d : Fin 15, classInSimplexNat s d) = 10 := by
320 fin_cases s <;> decide
321
322/-- The 24-simplex cell covers every one of the 15 nonzero 0/1 classes. -/
323theorem cell_covers_all_classes (d : Fin 15) :
324 ∃ s : Fin 24, simplexHasClass s d = true := by
325 fin_cases d <;> decide
326
327/-! ## §6. Flat-Hessian assembly skeleton (MODEL; kernels OPEN) -/
328
329/-- MODEL: flat second-variation class form for one hinge orbit,
330`Σ_{e,f} Aweight_e · Kdeficit_{e f} · c_e · c_f`.
331
332This is the 4D skeleton of the 3D Schläfli-reduced contraction
333`−Σ_τ Σ_f L' · θ'` in `ReggeTTFlatSecondVariation`: here `Aweight`
334plays the role of the area / hinge-volume first derivative and
335`Kdeficit` the outer product of deficit gradients. Both maps are OPEN. -/
336def flatHessianOrbitForm
337 (Aweight : Fin 15 → ℝ)
338 (Kdeficit : Fin 15 → Fin 15 → ℝ)
339 (c : Fin 15 → ℝ) : ℝ :=
340 ∑ e : Fin 15, ∑ f : Fin 15, Aweight e * Kdeficit e f * c e * c f
341
342/-- MODEL: cell-local seed-orbit contribution with incidence cutoff
343hard-wired so off-support classes cannot contribute. -/
344def seedOrbitAssembly
345 (Aweight : Fin 15 → ℝ)
346 (Kdeficit : Fin 15 → Fin 15 → ℝ)
347 (c : Fin 15 → ℝ) : ℝ :=
348 flatHessianOrbitForm
349 (fun e => (seedHingeIncidenceNat e : ℝ) * Aweight e)
350 (fun e f =>
351 if seedHingeIncidenceNat e = 0 ∨ seedHingeIncidenceNat f = 0 then 0
352 else Kdeficit e f)
353 c
354
355/-- THEOREM: a decoy-only bump in the area weight is annihilated by the
356incidence cutoff. -/
357theorem seedOrbitAssembly_decoy_area
358 (Aweight : Fin 15 → ℝ) (Kdeficit : Fin 15 → Fin 15 → ℝ)
359 (c : Fin 15 → ℝ) :
360 seedOrbitAssembly
361 (fun e => if e = decoyClass4 then (1 : ℝ) else Aweight e)
362 Kdeficit c =
363 seedOrbitAssembly Aweight Kdeficit c := by
364 unfold seedOrbitAssembly flatHessianOrbitForm
365 have hzN : seedHingeIncidenceNat decoyClass4 = 0 := by decide
366 have hz : (seedHingeIncidenceNat decoyClass4 : ℝ) = 0 := by
367 exact_mod_cast hzN
368 refine Finset.sum_congr rfl fun e _ => ?_
369 refine Finset.sum_congr rfl fun f _ => ?_
370 by_cases he : e = decoyClass4
371 · subst he
372 simp only [hz, zero_mul]
373 · simp [he]
374
375/-- Support projection onto positive-incidence classes. -/
376def supportProject (c : Fin 15 → ℝ) : Fin 15 → ℝ :=
377 fun d => if seedHingeIncidenceNat d = 0 then 0 else c d
378
379/-- THEOREM: assembly depends on `c` only through supported classes
380(incidence cutoff already zeros off-support deficit slots). -/
381theorem seedOrbitAssembly_support_projection
382 (Aweight : Fin 15 → ℝ)
383 (Kdeficit : Fin 15 → Fin 15 → ℝ)
384 (c : Fin 15 → ℝ) :
385 seedOrbitAssembly Aweight Kdeficit c =
386 seedOrbitAssembly Aweight Kdeficit (supportProject c) := by
387 unfold seedOrbitAssembly flatHessianOrbitForm supportProject
388 refine Finset.sum_congr rfl fun e _ => ?_
389 refine Finset.sum_congr rfl fun f _ => ?_
390 by_cases he : seedHingeIncidenceNat e = 0
391 · simp [he]
392 · by_cases hf : seedHingeIncidenceNat f = 0
393 · simp [he, hf]
394 · simp [he, hf]
395
396/-- Status record: combinatorial layer closed; true kernels OPEN. -/
397structure Hinge4DFlatKernelStatus where
398 freudenthal24Enumerated : Bool
399 seedHingeIncidenceClosed : Bool
400 trueDeficitKernelOpen : Bool
401 convergesEH4d : Bool
402 gapActionRecovery : Bool
403
404def hinge4DFlatKernelStatus : Hinge4DFlatKernelStatus where
405 freudenthal24Enumerated := true
406 seedHingeIncidenceClosed := true
407 trueDeficitKernelOpen := true
408 convergesEH4d := false
409 gapActionRecovery := false
410
411theorem hinge4DFlatKernelStatus_flags :
412 hinge4DFlatKernelStatus.freudenthal24Enumerated = true ∧
413 hinge4DFlatKernelStatus.seedHingeIncidenceClosed = true ∧
414 hinge4DFlatKernelStatus.trueDeficitKernelOpen = true ∧
415 hinge4DFlatKernelStatus.convergesEH4d = false ∧
416 hinge4DFlatKernelStatus.gapActionRecovery = false := by
417 decide
418
419end ReggeHinge4DFlatKernel
420end Analysis
421end Gravity
422end IndisputableMonolith
423