IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DStarKernel22.lean · 650 lines · 76 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
3import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
4import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
5
6/-!
7# Regge 4D full periodic-lattice star deficit class kernel (type (2,2))
8
9QG full-theory campaign, next kernel-checked increment after
10`ReggeHinge4DStarKernel` (type (1,1) seed orbit). Imports the Freudenthal
11incidence layer, the 15-class stencil, and the Gram-projection cosine
12calculus; never redefines their API.
13
14## Tier tags (binding)
15
16* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
17 `admit`, no new axioms, no `native_decide`, no `: True` shells).
18* Scope: the type-(2,2) triangle hinge `{0, e₀+e₁, e₀+e₁+e₂+e₃}`
19 (masks `{0,3,15}`, difference masks `(3,12)`) and its **full**
20 periodic Freudenthal star. Other hinge orbits remain as previously
21 closed or OPEN.
22* This does **not** complete the flat Hessian assembly over all hinges.
23* This does **not** prove `S_RS_converges_EH_4d`.
24* This does **not** flip `gap_action_recovery`.
25* This does **not** reverse-engineer weights from Einstein–Hilbert.
26
27## What is proved (deliverable A)
28
291. **Star enumeration.** Exactly four `(cube translate, Kuhn simplex)`
30 pairs contain the (2,2) hinge; among all 16 axis-aligned unit-cube
31 corners with coordinates in `{-1,0}`, only the origin corner
32 contains the absolute hinge, verified by decidable computation.
332. **Flat cosine multiset.** All four incident simplices have flat
34 cosine `0`, from each simplex's own hinge-ordered Gram vector
35 (local squared lengths `(2,4,1,3,2,1,1,3,1,2)`).
363. **Flatness gate.** Star angle sum equals exactly `2π`
37 (`4 · arccos 0 = 4 · (π/2)`).
384. **Full-star deficit class kernel** on all 15 stencil classes with
39 the closed form recorded below.
405. **Gates:** nonvacuity, swap-`0↔1` and swap-`2↔3` symmetry (both
41 fix the hinge vertex set), uniform-scaling decoy, homothety
42 stationarity.
43
44Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
45-/
46
47namespace IndisputableMonolith
48namespace Gravity
49namespace Analysis
50namespace ReggeHinge4DStarKernel22
51
52open BigOperators
53open ReggeHinge4DFlatKernel
54open ReggeHinge4DDihedralKernel
55open ReggeEdgeStencil4D
56
57noncomputable section
58
59/-! ## §1. Cube translates and star enumeration -/
60
61/-- Absolute (2,2) hinge vertex masks. -/
62def absHingeMasks : Finset ℕ := {0, 3, 15}
63
64/-- Cube corner encoded as a 4-bit mask: bit `i` set means the corner
65has coordinate `-1` on axis `i` (else `0`). -/
66abbrev CubeCorner := Fin 16
67
68/-- Geometric containment: absolute vertex mask `m` lies in the unit
69cube with corner `c` iff every negatively shifted axis has absolute
70coordinate `0`. -/
71def cornerContainsMask (c : CubeCorner) (m : ℕ) : Bool :=
72 decide (∀ i : Fin 4, ¬ Nat.testBit c.val i.val ∨ ¬ Nat.testBit m i.val)
73
74def cornerContainsHinge (c : CubeCorner) : Bool :=
75 decide (∀ m ∈ absHingeMasks, cornerContainsMask c m = true)
76
77/-- Local mask of an absolute vertex inside a containing corner cube
78(XOR with the corner bitmask). -/
79def localMask (c : CubeCorner) (m : ℕ) : ℕ := Nat.xor m c.val
80
81def localHingeMasks (c : CubeCorner) : Finset ℕ :=
82 absHingeMasks.image (localMask c)
83
84def containsHinge (c : CubeCorner) (s : Fin 24) : Bool :=
85 cornerContainsHinge c &&
86 decide (∀ m ∈ localHingeMasks c, ∃ i : Fin 5, vertexMask s i = m)
87
88structure StarMember where
89 cube : CubeCorner
90 simplex : Fin 24
91 deriving DecidableEq, Repr
92
93def starMembers : List StarMember :=
94 [ ⟨0, 0⟩, ⟨0, 1⟩, ⟨0, 6⟩, ⟨0, 7⟩ ]
95
96theorem starMembers_length : starMembers.length = 4 := rfl
97
98theorem starMembers_complete (c : CubeCorner) (s : Fin 24) :
99 containsHinge c s = true ↔ ⟨c, s⟩ ∈ starMembers := by
100 revert c s
101 decide
102
103theorem star_cardinality :
104 (Finset.univ.filter (fun p : CubeCorner × Fin 24 =>
105 containsHinge p.1 p.2 = true)).card = 4 := by
106 decide
107
108theorem only_origin_corner_contains_hinge (c : CubeCorner)
109 (h : cornerContainsHinge c = true) : c = 0 := by
110 revert c
111 decide
112
113/-! ## §2. Flat squared-length orbit representative -/
114
115/-- Hinge-ordered flat squared lengths for each (2,2) star simplex:
116hinge vertices ordered `(0,3,15)`, apexes by increasing simplex index. -/
117def t22FlatSqEdges : SqEdges4
118 | 0 => 2 | 1 => 4 | 2 => 1 | 3 => 3 | 4 => 2
119 | 5 => 1 | 6 => 1 | 7 => 3 | 8 => 1 | 9 => 2
120
121theorem hingeGramDet_t22 : hingeGramDet t22FlatSqEdges = 16 := by
122 norm_num [hingeGramDet, t22FlatSqEdges]
123theorem apexDotNum_t22 : apexDotNum t22FlatSqEdges = 0 := by
124 norm_num [apexDotNum, hingeGramDet, t22FlatSqEdges]
125theorem apex3NormSqNum_t22 : apex3NormSqNum t22FlatSqEdges = 8 := by
126 norm_num [apex3NormSqNum, hingeGramDet, t22FlatSqEdges]
127theorem apex4NormSqNum_t22 : apex4NormSqNum t22FlatSqEdges = 8 := by
128 norm_num [apex4NormSqNum, hingeGramDet, t22FlatSqEdges]
129
130theorem cosDihedral_t22_flat : cosDihedral t22FlatSqEdges = 0 := by
131 rw [cos_numForm _ (by rw [hingeGramDet_t22]; norm_num),
132 apexDotNum_t22, apex3NormSqNum_t22, apex4NormSqNum_t22]
133 norm_num
134
135/-! ## §3. Flatness gate -/
136
137def flatAngleT22 : ℝ := Real.arccos 0
138
139theorem flatAngleT22_eq : flatAngleT22 = Real.pi / 2 := Real.arccos_zero
140
141def starFlatAngleSum : ℝ := 4 * flatAngleT22
142
143theorem star_flat_angle_sum_two_pi : starFlatAngleSum = 2 * Real.pi := by
144 simp only [starFlatAngleSum, flatAngleT22_eq]
145 ring
146
147def starFlatCosines : Fin 4 → ℝ := fun _ => 0
148
149theorem starFlatCosines_match_orbit (m : Fin 4) :
150 starFlatCosines m = cosDihedral t22FlatSqEdges :=
151 cosDihedral_t22_flat.symm
152
153/-! ## §4. Coordinate derivatives (cleared-denominator master lemma) -/
154
155def t22CoordPath (k : Fin 10) (t : ℝ) : SqEdges4 :=
156 fun j => if j = k then t else t22FlatSqEdges j
157
158def t22CosKernel : Fin 10 → ℝ
159 | ⟨0, _⟩ => (-1 / 4 : ℝ)
160 | ⟨1, _⟩ => (-1 / 4 : ℝ)
161 | ⟨2, _⟩ => 0
162 | ⟨3, _⟩ => (1 / 2 : ℝ)
163 | ⟨4, _⟩ => (-1 / 4 : ℝ)
164 | ⟨5, _⟩ => (1 / 2 : ℝ)
165 | ⟨6, _⟩ => (1 / 2 : ℝ)
166 | ⟨7, _⟩ => (1 / 2 : ℝ)
167 | ⟨8, _⟩ => 0
168 | ⟨9, _⟩ => (-1 : ℝ)
169
170private lemma hasDerivAt_quadPoly (a b c t0 : ℝ) :
171 HasDerivAt (fun t : ℝ => a * t ^ 2 + b * t + c) (2 * a * t0 + b) t0 := by
172 have h1 : HasDerivAt (fun t : ℝ => t ^ 2) (2 * t0) t0 := by
173 simpa using hasDerivAt_pow 2 t0
174 have h2 : HasDerivAt (fun t : ℝ => a * t ^ 2) (a * (2 * t0)) t0 :=
175 h1.const_mul a
176 have h3 : HasDerivAt (fun t : ℝ => b * t) b t0 := by
177 simpa using (hasDerivAt_id t0).const_mul b
178 have h4 := (h2.add h3).add_const c
179 convert h4 using 1
180 ring
181
182/-- Master lemma at the (2,2) flat point: `N=0`, `P=Q=8`, so
183`d/dt (N/(2√(PQ))) = N'/16`. -/
184private lemma hasDerivAt_numForm_t22 {N P Q : ℝ → ℝ} {t0 N' P' Q' : ℝ}
185 (hN : HasDerivAt N N' t0) (hP : HasDerivAt P P' t0)
186 (hQ : HasDerivAt Q Q' t0)
187 (hN0 : N t0 = 0) (hP0 : P t0 = 8) (hQ0 : Q t0 = 8) :
188 HasDerivAt (fun t => N t / (2 * Real.sqrt (P t * Q t)))
189 (N' / 16) t0 := by
190 have hPQ : HasDerivAt (fun t => P t * Q t)
191 (P' * Q t0 + P t0 * Q') t0 := hP.mul hQ
192 have hPQ0 : P t0 * Q t0 = 64 := by rw [hP0, hQ0]; norm_num
193 have hPQne : P t0 * Q t0 ≠ 0 := by rw [hPQ0]; norm_num
194 have hsqrt : HasDerivAt (fun t => Real.sqrt (P t * Q t))
195 ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0))) t0 :=
196 hPQ.sqrt hPQne
197 have hden : HasDerivAt (fun t => 2 * Real.sqrt (P t * Q t))
198 (2 * ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0)))) t0 :=
199 hsqrt.const_mul 2
200 have hdenne : 2 * Real.sqrt (P t0 * Q t0) ≠ 0 := by
201 rw [hPQ0]; positivity
202 have hdiv := hN.div hden hdenne
203 convert hdiv using 1
204 have h8 : Real.sqrt (P t0 * Q t0) = 8 := by
205 rw [hPQ0, show (64 : ℝ) = (8 : ℝ) ^ 2 by norm_num,
206 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 8)]
207 rw [h8, hN0]
208 ring
209
210private lemma hasDerivAt_t22_slot (k : Fin 10) (t0 : ℝ)
211 (aN bN cN aP bP cP aQ bQ cQ aD bD cD : ℝ)
212 (hpath : ∀ t : ℝ,
213 apexDotNum (t22CoordPath k t) = aN * t ^ 2 + bN * t + cN
214 ∧ apex3NormSqNum (t22CoordPath k t) = aP * t ^ 2 + bP * t + cP
215 ∧ apex4NormSqNum (t22CoordPath k t) = aQ * t ^ 2 + bQ * t + cQ
216 ∧ hingeGramDet (t22CoordPath k t) = aD * t ^ 2 + bD * t + cD)
217 (hN0 : aN * t0 ^ 2 + bN * t0 + cN = 0)
218 (hP0 : aP * t0 ^ 2 + bP * t0 + cP = 8)
219 (hQ0 : aQ * t0 ^ 2 + bQ * t0 + cQ = 8)
220 (hD0 : 0 < aD * t0 ^ 2 + bD * t0 + cD) :
221 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath k t))
222 ((2 * aN * t0 + bN) / 16) t0 := by
223 have hN := hasDerivAt_quadPoly aN bN cN t0
224 have hP := hasDerivAt_quadPoly aP bP cP t0
225 have hQ := hasDerivAt_quadPoly aQ bQ cQ t0
226 have hmain := hasDerivAt_numForm_t22 hN hP hQ hN0 hP0 hQ0
227 refine hmain.congr_of_eventuallyEq ?_
228 have hDcont : Continuous fun t : ℝ => aD * t ^ 2 + bD * t + cD := by
229 continuity
230 have hDev : ∀ᶠ t in nhds t0, 0 < aD * t ^ 2 + bD * t + cD :=
231 (hDcont.tendsto t0).eventually (eventually_gt_nhds hD0)
232 filter_upwards [hDev] with t ht
233 have hp := hpath t
234 rw [cos_numForm (t22CoordPath k t) (by rw [hp.2.2.2]; exact ht),
235 hp.1, hp.2.1, hp.2.2.1]
236
237private lemma t22_path0_polys : ∀ t : ℝ,
238 apexDotNum (t22CoordPath 0 t) = (-2) * t ^ 2 + (4) * t + (0)
239 ∧ apex3NormSqNum (t22CoordPath 0 t) = (-3) * t ^ 2 + (12) * t + (-4)
240 ∧ apex4NormSqNum (t22CoordPath 0 t) = (-1) * t ^ 2 + (8) * t + (-4)
241 ∧ hingeGramDet (t22CoordPath 0 t) = (-1) * t ^ 2 + (12) * t + (-4) := by
242 intro t
243 refine ⟨?_, ?_, ?_, ?_⟩ <;>
244 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
245 t22CoordPath, t22FlatSqEdges] <;> ring
246
247private lemma t22_path1_polys : ∀ t : ℝ,
248 apexDotNum (t22CoordPath 1 t) = (0) * t ^ 2 + (-4) * t + (16)
249 ∧ apex3NormSqNum (t22CoordPath 1 t) = (-1) * t ^ 2 + (8) * t + (-8)
250 ∧ apex4NormSqNum (t22CoordPath 1 t) = (-1) * t ^ 2 + (8) * t + (-8)
251 ∧ hingeGramDet (t22CoordPath 1 t) = (-1) * t ^ 2 + (8) * t + (0) := by
252 intro t
253 refine ⟨?_, ?_, ?_, ?_⟩ <;>
254 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
255 t22CoordPath, t22FlatSqEdges] <;> ring
256
257private lemma t22_path2_polys : ∀ t : ℝ,
258 apexDotNum (t22CoordPath 2 t) = (0) * t ^ 2 + (0) * t + (0)
259 ∧ apex3NormSqNum (t22CoordPath 2 t) = (-2) * t ^ 2 + (12) * t + (-2)
260 ∧ apex4NormSqNum (t22CoordPath 2 t) = (0) * t ^ 2 + (0) * t + (8)
261 ∧ hingeGramDet (t22CoordPath 2 t) = (0) * t ^ 2 + (0) * t + (16) := by
262 intro t
263 refine ⟨?_, ?_, ?_, ?_⟩ <;>
264 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
265 t22CoordPath, t22FlatSqEdges] <;> ring
266
267private lemma t22_path3_polys : ∀ t : ℝ,
268 apexDotNum (t22CoordPath 3 t) = (0) * t ^ 2 + (8) * t + (-24)
269 ∧ apex3NormSqNum (t22CoordPath 3 t) = (0) * t ^ 2 + (0) * t + (8)
270 ∧ apex4NormSqNum (t22CoordPath 3 t) = (-2) * t ^ 2 + (12) * t + (-10)
271 ∧ hingeGramDet (t22CoordPath 3 t) = (0) * t ^ 2 + (0) * t + (16) := by
272 intro t
273 refine ⟨?_, ?_, ?_, ?_⟩ <;>
274 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
275 t22CoordPath, t22FlatSqEdges] <;> ring
276
277private lemma t22_path4_polys : ∀ t : ℝ,
278 apexDotNum (t22CoordPath 4 t) = (-2) * t ^ 2 + (4) * t + (0)
279 ∧ apex3NormSqNum (t22CoordPath 4 t) = (-1) * t ^ 2 + (8) * t + (-4)
280 ∧ apex4NormSqNum (t22CoordPath 4 t) = (-3) * t ^ 2 + (12) * t + (-4)
281 ∧ hingeGramDet (t22CoordPath 4 t) = (-1) * t ^ 2 + (12) * t + (-4) := by
282 intro t
283 refine ⟨?_, ?_, ?_, ?_⟩ <;>
284 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
285 t22CoordPath, t22FlatSqEdges] <;> ring
286
287private lemma t22_path5_polys : ∀ t : ℝ,
288 apexDotNum (t22CoordPath 5 t) = (0) * t ^ 2 + (8) * t + (-8)
289 ∧ apex3NormSqNum (t22CoordPath 5 t) = (-4) * t ^ 2 + (16) * t + (-4)
290 ∧ apex4NormSqNum (t22CoordPath 5 t) = (0) * t ^ 2 + (0) * t + (8)
291 ∧ hingeGramDet (t22CoordPath 5 t) = (0) * t ^ 2 + (0) * t + (16) := by
292 intro t
293 refine ⟨?_, ?_, ?_, ?_⟩ <;>
294 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
295 t22CoordPath, t22FlatSqEdges] <;> ring
296
297private lemma t22_path6_polys : ∀ t : ℝ,
298 apexDotNum (t22CoordPath 6 t) = (0) * t ^ 2 + (8) * t + (-8)
299 ∧ apex3NormSqNum (t22CoordPath 6 t) = (0) * t ^ 2 + (0) * t + (8)
300 ∧ apex4NormSqNum (t22CoordPath 6 t) = (-4) * t ^ 2 + (16) * t + (-4)
301 ∧ hingeGramDet (t22CoordPath 6 t) = (0) * t ^ 2 + (0) * t + (16) := by
302 intro t
303 refine ⟨?_, ?_, ?_, ?_⟩ <;>
304 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
305 t22CoordPath, t22FlatSqEdges] <;> ring
306
307private lemma t22_path7_polys : ∀ t : ℝ,
308 apexDotNum (t22CoordPath 7 t) = (0) * t ^ 2 + (8) * t + (-24)
309 ∧ apex3NormSqNum (t22CoordPath 7 t) = (-2) * t ^ 2 + (12) * t + (-10)
310 ∧ apex4NormSqNum (t22CoordPath 7 t) = (0) * t ^ 2 + (0) * t + (8)
311 ∧ hingeGramDet (t22CoordPath 7 t) = (0) * t ^ 2 + (0) * t + (16) := by
312 intro t
313 refine ⟨?_, ?_, ?_, ?_⟩ <;>
314 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
315 t22CoordPath, t22FlatSqEdges] <;> ring
316
317private lemma t22_path8_polys : ∀ t : ℝ,
318 apexDotNum (t22CoordPath 8 t) = (0) * t ^ 2 + (0) * t + (0)
319 ∧ apex3NormSqNum (t22CoordPath 8 t) = (0) * t ^ 2 + (0) * t + (8)
320 ∧ apex4NormSqNum (t22CoordPath 8 t) = (-2) * t ^ 2 + (12) * t + (-2)
321 ∧ hingeGramDet (t22CoordPath 8 t) = (0) * t ^ 2 + (0) * t + (16) := by
322 intro t
323 refine ⟨?_, ?_, ?_, ?_⟩ <;>
324 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
325 t22CoordPath, t22FlatSqEdges] <;> ring
326
327private lemma t22_path9_polys : ∀ t : ℝ,
328 apexDotNum (t22CoordPath 9 t) = (0) * t ^ 2 + (-16) * t + (32)
329 ∧ apex3NormSqNum (t22CoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8)
330 ∧ apex4NormSqNum (t22CoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8)
331 ∧ hingeGramDet (t22CoordPath 9 t) = (0) * t ^ 2 + (0) * t + (16) := by
332 intro t
333 refine ⟨?_, ?_, ?_, ?_⟩ <;>
334 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
335 t22CoordPath, t22FlatSqEdges] <;> ring
336
337theorem hasDerivAt_t22_slot0 :
338 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 0 t))
339 ((-1 / 4 : ℝ)) 2 := by
340 have h := hasDerivAt_t22_slot 0 2 (-2) (4) (0) (-3) (12) (-4) (-1) (8) (-4) (-1) (12) (-4) t22_path0_polys
341 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
342 convert h using 1
343 ring
344
345theorem hasDerivAt_t22_slot1 :
346 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 1 t))
347 ((-1 / 4 : ℝ)) 4 := by
348 have h := hasDerivAt_t22_slot 1 4 (0) (-4) (16) (-1) (8) (-8) (-1) (8) (-8) (-1) (8) (0) t22_path1_polys
349 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
350 convert h using 1
351 ring
352
353theorem hasDerivAt_t22_slot2 :
354 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 2 t))
355 (0) 1 := by
356 have h := hasDerivAt_t22_slot 2 1 (0) (0) (0) (-2) (12) (-2) (0) (0) (8) (0) (0) (16) t22_path2_polys
357 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
358 convert h using 1
359 ring
360
361theorem hasDerivAt_t22_slot3 :
362 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 3 t))
363 ((1 / 2 : ℝ)) 3 := by
364 have h := hasDerivAt_t22_slot 3 3 (0) (8) (-24) (0) (0) (8) (-2) (12) (-10) (0) (0) (16) t22_path3_polys
365 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
366 convert h using 1
367 ring
368
369theorem hasDerivAt_t22_slot4 :
370 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 4 t))
371 ((-1 / 4 : ℝ)) 2 := by
372 have h := hasDerivAt_t22_slot 4 2 (-2) (4) (0) (-1) (8) (-4) (-3) (12) (-4) (-1) (12) (-4) t22_path4_polys
373 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
374 convert h using 1
375 ring
376
377theorem hasDerivAt_t22_slot5 :
378 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 5 t))
379 ((1 / 2 : ℝ)) 1 := by
380 have h := hasDerivAt_t22_slot 5 1 (0) (8) (-8) (-4) (16) (-4) (0) (0) (8) (0) (0) (16) t22_path5_polys
381 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
382 convert h using 1
383 ring
384
385theorem hasDerivAt_t22_slot6 :
386 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 6 t))
387 ((1 / 2 : ℝ)) 1 := by
388 have h := hasDerivAt_t22_slot 6 1 (0) (8) (-8) (0) (0) (8) (-4) (16) (-4) (0) (0) (16) t22_path6_polys
389 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
390 convert h using 1
391 ring
392
393theorem hasDerivAt_t22_slot7 :
394 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 7 t))
395 ((1 / 2 : ℝ)) 3 := by
396 have h := hasDerivAt_t22_slot 7 3 (0) (8) (-24) (-2) (12) (-10) (0) (0) (8) (0) (0) (16) t22_path7_polys
397 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
398 convert h using 1
399 ring
400
401theorem hasDerivAt_t22_slot8 :
402 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 8 t))
403 (0) 1 := by
404 have h := hasDerivAt_t22_slot 8 1 (0) (0) (0) (0) (0) (8) (-2) (12) (-2) (0) (0) (16) t22_path8_polys
405 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
406 convert h using 1
407 ring
408
409theorem hasDerivAt_t22_slot9 :
410 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath 9 t))
411 ((-1 : ℝ)) 2 := by
412 have h := hasDerivAt_t22_slot 9 2 (0) (-16) (32) (0) (0) (8) (0) (0) (8) (0) (0) (16) t22_path9_polys
413 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
414 convert h using 1
415 ring
416
417theorem hasDerivAt_t22_coord (k : Fin 10) :
418 HasDerivAt (fun t : ℝ => cosDihedral (t22CoordPath k t))
419 (t22CosKernel k) (t22FlatSqEdges k) := by
420 fin_cases k
421 · exact hasDerivAt_t22_slot0
422 · exact hasDerivAt_t22_slot1
423 · exact hasDerivAt_t22_slot2
424 · exact hasDerivAt_t22_slot3
425 · exact hasDerivAt_t22_slot4
426 · exact hasDerivAt_t22_slot5
427 · exact hasDerivAt_t22_slot6
428 · exact hasDerivAt_t22_slot7
429 · exact hasDerivAt_t22_slot8
430 · exact hasDerivAt_t22_slot9
431
432/-! ## §5. Full-star deficit class kernel -/
433
434/-- Arccos chain factor `d(arccos)/d(cos)` at flat cosine `0`: `-1`. -/
435def chainT22 : ℝ := (-1 : ℝ)
436
437/-- Per-simplex deficit kernel equals `-chain · cosKernel = cosKernel`. -/
438def t22DeficitKernel : Fin 10 → ℝ := t22CosKernel
439
440theorem t22DeficitKernel_eq_chain (k : Fin 10) :
441 t22DeficitKernel k = -chainT22 * t22CosKernel k := by
442 simp [t22DeficitKernel, chainT22]
443
444/-- Hinge-ordered local slot → global edge class, for star members
445indexed in `starMembers` order (simplices `0,1,6,7`). -/
446def starSlotClass : Fin 4 → Fin 10 → Fin 15
447 | 0, 0 => 2 | 0, 1 => 14 | 0, 2 => 0 | 0, 3 => 6 | 0, 4 => 11
448 | 0, 5 => 1 | 0, 6 => 3 | 0, 7 => 13 | 0, 8 => 7 | 0, 9 => 5
449 | 1, 0 => 2 | 1, 1 => 14 | 1, 2 => 0 | 1, 3 => 10 | 1, 4 => 11
450 | 1, 5 => 1 | 1, 6 => 7 | 1, 7 => 13 | 1, 8 => 3 | 1, 9 => 9
451 | 2, 0 => 2 | 2, 1 => 14 | 2, 2 => 1 | 2, 3 => 6 | 2, 4 => 11
452 | 2, 5 => 0 | 2, 6 => 3 | 2, 7 => 12 | 2, 8 => 7 | 2, 9 => 4
453 | 3, 0 => 2 | 3, 1 => 14 | 3, 2 => 1 | 3, 3 => 10 | 3, 4 => 11
454 | 3, 5 => 0 | 3, 6 => 7 | 3, 7 => 12 | 3, 8 => 3 | 3, 9 => 8
455
456def assembleStarMember (m : Fin 4) : Fin 15 → ℝ :=
457 fun d => ∑ e : Fin 10,
458 if starSlotClass m e = d then t22DeficitKernel e else 0
459
460def fullStarClassKernelAssembled : Fin 15 → ℝ :=
461 fun d => ∑ m : Fin 4, assembleStarMember m d
462
463def fullStarClassKernel : Fin 15 → ℝ
464 | ⟨0, _⟩ => (1 : ℝ)
465 | ⟨1, _⟩ => (1 : ℝ)
466 | ⟨2, _⟩ => (-1 : ℝ)
467 | ⟨3, _⟩ => (1 : ℝ)
468 | ⟨4, _⟩ => (-1 : ℝ)
469 | ⟨5, _⟩ => (-1 : ℝ)
470 | ⟨6, _⟩ => (1 : ℝ)
471 | ⟨7, _⟩ => (1 : ℝ)
472 | ⟨8, _⟩ => (-1 : ℝ)
473 | ⟨9, _⟩ => (-1 : ℝ)
474 | ⟨10, _⟩ => (1 : ℝ)
475 | ⟨11, _⟩ => (-1 : ℝ)
476 | ⟨12, _⟩ => (1 : ℝ)
477 | ⟨13, _⟩ => (1 : ℝ)
478 | ⟨14, _⟩ => (-1 : ℝ)
479
480private lemma sum_fin10 (f : Fin 10 → ℝ) :
481 (∑ e : Fin 10, f e) =
482 f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8 + f 9 := by
483 rw [show (Finset.univ : Finset (Fin 10)) =
484 insert (0 : Fin 10) (insert (1 : Fin 10) (insert (2 : Fin 10)
485 (insert (3 : Fin 10) (insert (4 : Fin 10) (insert (5 : Fin 10)
486 (insert (6 : Fin 10) (insert (7 : Fin 10) (insert (8 : Fin 10)
487 (insert (9 : Fin 10) (∅ : Finset (Fin 10))))))))))) from by decide]
488 simp [Finset.sum_insert]
489 ring
490
491private lemma member_eval (m : Fin 4) (d : Fin 15) :
492 assembleStarMember m d =
493 (if starSlotClass m 0 = d then t22DeficitKernel 0 else 0) +
494 (if starSlotClass m 1 = d then t22DeficitKernel 1 else 0) +
495 (if starSlotClass m 2 = d then t22DeficitKernel 2 else 0) +
496 (if starSlotClass m 3 = d then t22DeficitKernel 3 else 0) +
497 (if starSlotClass m 4 = d then t22DeficitKernel 4 else 0) +
498 (if starSlotClass m 5 = d then t22DeficitKernel 5 else 0) +
499 (if starSlotClass m 6 = d then t22DeficitKernel 6 else 0) +
500 (if starSlotClass m 7 = d then t22DeficitKernel 7 else 0) +
501 (if starSlotClass m 8 = d then t22DeficitKernel 8 else 0) +
502 (if starSlotClass m 9 = d then t22DeficitKernel 9 else 0) := by
503 simp only [assembleStarMember]
504 exact sum_fin10 _
505
506private lemma sum4 (f : Fin 4 → ℝ) :
507 (∑ m : Fin 4, f m) = f 0 + f 1 + f 2 + f 3 := by
508 rw [show (Finset.univ : Finset (Fin 4)) =
509 insert (0 : Fin 4) (insert (1 : Fin 4) (insert (2 : Fin 4)
510 (insert (3 : Fin 4) (∅ : Finset (Fin 4))))) from by decide]
511 simp [Finset.sum_insert]
512 ring
513
514theorem fullStarClassKernel_eq (d : Fin 15) :
515 fullStarClassKernelAssembled d = fullStarClassKernel d := by
516 simp only [fullStarClassKernelAssembled]
517 rw [sum4]
518 fin_cases d <;>
519 (simp [member_eval, starSlotClass, t22DeficitKernel, t22CosKernel,
520 fullStarClassKernel] <;> norm_num)
521
522theorem fullStarClassKernel_values :
523 fullStarClassKernel 0 = (1 : ℝ) ∧
524 fullStarClassKernel 1 = (1 : ℝ) ∧
525 fullStarClassKernel 2 = (-1 : ℝ) ∧
526 fullStarClassKernel 3 = (1 : ℝ) ∧
527 fullStarClassKernel 4 = (-1 : ℝ) ∧
528 fullStarClassKernel 5 = (-1 : ℝ) ∧
529 fullStarClassKernel 6 = (1 : ℝ) ∧
530 fullStarClassKernel 7 = (1 : ℝ) ∧
531 fullStarClassKernel 8 = (-1 : ℝ) ∧
532 fullStarClassKernel 9 = (-1 : ℝ) ∧
533 fullStarClassKernel 10 = (1 : ℝ) ∧
534 fullStarClassKernel 11 = (-1 : ℝ) ∧
535 fullStarClassKernel 12 = (1 : ℝ) ∧
536 fullStarClassKernel 13 = (1 : ℝ) ∧
537 fullStarClassKernel 14 = (-1 : ℝ) :=
538 ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
539
540/-! ## §6. Gates -/
541
542def swap01Mask (m : ℕ) : ℕ :=
543 (if Nat.testBit m 0 then 2 else 0) +
544 (if Nat.testBit m 1 then 1 else 0) +
545 (if Nat.testBit m 2 then 4 else 0) +
546 (if Nat.testBit m 3 then 8 else 0)
547
548theorem swap01Mask_bounds (d : Fin 15) :
549 0 < swap01Mask (maskOf d) ∧ swap01Mask (maskOf d) ≤ 15 := by
550 fin_cases d <;> decide
551
552def swap01Class (d : Fin 15) : Fin 15 :=
553 ⟨swap01Mask (maskOf d) - 1, by
554 have h := swap01Mask_bounds d
555 omega⟩
556
557theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 0 ≠ 0 := by
558 norm_num [fullStarClassKernel]
559
560theorem fullStarClassKernel_swap01 (d : Fin 15) :
561 fullStarClassKernel (swap01Class d) = fullStarClassKernel d := by
562 fin_cases d <;> rfl
563
564theorem fullStarClassKernel_swap23 (d : Fin 15) :
565 fullStarClassKernel (swap23Class d) = fullStarClassKernel d := by
566 fin_cases d <;> rfl
567
568def fullStarDirectional (v : Fin 15 → ℝ) : ℝ :=
569 ∑ d : Fin 15, v d * fullStarClassKernel d
570
571private lemma sum15_all (f : Fin 15 → ℝ) :
572 (∑ d : Fin 15, f d) =
573 f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8 + f 9 +
574 f 10 + f 11 + f 12 + f 13 + f 14 := by
575 rw [show (Finset.univ : Finset (Fin 15)) =
576 insert (0 : Fin 15) (insert (1 : Fin 15) (insert (2 : Fin 15)
577 (insert (3 : Fin 15) (insert (4 : Fin 15) (insert (5 : Fin 15)
578 (insert (6 : Fin 15) (insert (7 : Fin 15) (insert (8 : Fin 15)
579 (insert (9 : Fin 15) (insert (10 : Fin 15) (insert (11 : Fin 15)
580 (insert (12 : Fin 15) (insert (13 : Fin 15) (insert (14 : Fin 15)
581 (∅ : Finset (Fin 15)))))))))))))))) from by decide]
582 simp [Finset.sum_insert]
583 ring
584
585theorem fullStar_uniformScale_decoy :
586 fullStarDirectional (fun _ => (1 : ℝ)) = (1 : ℝ) := by
587 simp only [fullStarDirectional]
588 rw [sum15_all]
589 simp [fullStarClassKernel]
590
591theorem fullStar_homothety_stationary :
592 fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
593 simp only [fullStarDirectional]
594 rw [sum15_all]
595 have w0 : classWeightNat 0 = 1 := by decide
596 have w1 : classWeightNat 1 = 1 := by decide
597 have w2 : classWeightNat 2 = 2 := by decide
598 have w3 : classWeightNat 3 = 1 := by decide
599 have w4 : classWeightNat 4 = 2 := by decide
600 have w5 : classWeightNat 5 = 2 := by decide
601 have w6 : classWeightNat 6 = 3 := by decide
602 have w7 : classWeightNat 7 = 1 := by decide
603 have w8 : classWeightNat 8 = 2 := by decide
604 have w9 : classWeightNat 9 = 2 := by decide
605 have w10 : classWeightNat 10 = 3 := by decide
606 have w11 : classWeightNat 11 = 2 := by decide
607 have w12 : classWeightNat 12 = 3 := by decide
608 have w13 : classWeightNat 13 = 3 := by decide
609 have w14 : classWeightNat 14 = 4 := by decide
610 simp [fullStarClassKernel, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9,
611 w10, w11, w12, w13, w14]
612 norm_num
613
614/-! ## §7. Status -/
615
616structure Hinge4DStarKernel22Status where
617 starEnumerationClosed : Bool
618 flatnessGateClosed : Bool
619 fullStarClassKernelClosed : Bool
620 otherHingeOrbitsOpen : Bool
621 flatHessianAssemblyOpen : Bool
622 convergesEH4d : Bool
623 gapActionRecovery : Bool
624
625def hinge4DStarKernel22Status : Hinge4DStarKernel22Status where
626 starEnumerationClosed := true
627 flatnessGateClosed := true
628 fullStarClassKernelClosed := true
629 otherHingeOrbitsOpen := true
630 flatHessianAssemblyOpen := true
631 convergesEH4d := false
632 gapActionRecovery := false
633
634theorem hinge4DStarKernel22Status_flags :
635 hinge4DStarKernel22Status.starEnumerationClosed = true ∧
636 hinge4DStarKernel22Status.flatnessGateClosed = true ∧
637 hinge4DStarKernel22Status.fullStarClassKernelClosed = true ∧
638 hinge4DStarKernel22Status.otherHingeOrbitsOpen = true ∧
639 hinge4DStarKernel22Status.flatHessianAssemblyOpen = true ∧
640 hinge4DStarKernel22Status.convergesEH4d = false ∧
641 hinge4DStarKernel22Status.gapActionRecovery = false := by
642 decide
643
644end
645
646end ReggeHinge4DStarKernel22
647end Analysis
648end Gravity
649end IndisputableMonolith
650