IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DDihedralKernel.lean · 748 lines · 87 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
3import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
4
5/-!
6# Regge 4D seed-hinge dihedral cosine kernel at flat
7
8QG full-theory campaign, next kernel-checked increment after
9`ReggeHinge4DFlatKernel`. Imports the Freudenthal incidence layer and
10the 15-class stencil; never redefines their API.
11
12## Tier tags (binding)
13
14* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
15 `admit`, no new axioms, no `native_decide`, no `: True` shells).
16* Scope: the seed triangle hinge `{0, e₀, e₀+e₁}` inside its **two**
17 seed-cell Freudenthal 4-simplices only (the permutations beginning
18 `(0,1,…)`; both share the same local squared-edge vector, proved
19 against the incidence layer's `localEdgeMask`). The full lattice
20 orbit sum over all hinges is OPEN.
21* This does **not** complete the flat Hessian of the 4D Regge action.
22* This does **not** prove `S_RS_converges_EH_4d`.
23* This does **not** flip `gap_action_recovery`.
24* This does **not** reverse-engineer weights from Einstein–Hilbert.
25
26## What is proved (deliverable A)
27
281. **Gram-projection cosine.** `cosDihedral` of the seed-hinge dihedral
29 angle as an explicit function of the ten local squared edge lengths
30 (inner product / norms of the two apex vectors projected orthogonal
31 to the hinge plane, in cleared-denominator Gram form).
322. **Flat value.** `cosDihedral = 1/√2` at the flat Freudenthal point
33 (equivalently `cos² = 1/2`, `sin = 1/√2`); transcendental-free
34 arithmetic throughout (`sin² = 1 − cos²`).
353. **All ten coordinate derivatives** (`HasDerivAt`, deliverable A):
36 slot 8 ↦ `√2/8`, slot 9 ↦ `-√2/4`, slots 0–7 ↦ `0`, packaged as
37 `cosDihedralKernel` with the master theorem
38 `hasDerivAt_cosDihedral_coord`.
394. **Angle and two-simplex partial deficit kernels.** Via the arccos
40 chain factor `-1/sin = -√2` at flat: local angle kernel
41 `(slot 8, slot 9) ↦ (-1/4, 1/2)`; assembled on the 15 edge classes
42 through each seed simplex's `localEdgeClass` table, the two-simplex
43 partial deficit gradient `∂(2π - θ₀ - θ₁)/∂ℓ²` is supported on
44 classes `(3, 7, 11)` with values `(-1/2, -1/2, +1/2)`.
455. **Nonvacuity, symmetry, decoy.** Slot-9 kernel nonzero; the class
46 kernel is invariant under the hinge-fixing axis swap `2 ↔ 3`;
47 uniform squared-length scaling gives `-√2/8 ≠ 0` (computed, not
48 assumed), while the true homothety direction gives `0` exactly as
49 scale invariance demands.
50
51Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
52-/
53
54namespace IndisputableMonolith
55namespace Gravity
56namespace Analysis
57namespace ReggeHinge4DDihedralKernel
58
59open BigOperators
60open ReggeHinge4DFlatKernel
61open ReggeEdgeStencil4D
62
63noncomputable section
64
65/-! ## §1. Local squared edges of the seed simplices -/
66
67abbrev SqEdges4 := Fin 10 → ℝ
68
69/-- Flat Freudenthal squared lengths shared by both seed simplices,
70in the local slot order `localEdgePair` of the incidence layer. -/
71def seedFlatSqEdges : SqEdges4
72 | 0 => 1 | 1 => 2 | 2 => 3 | 3 => 4 | 4 => 1
73 | 5 => 2 | 6 => 3 | 7 => 1 | 8 => 2 | 9 => 1
74
75@[simp] lemma seedFlat_0 : seedFlatSqEdges 0 = 1 := rfl
76@[simp] lemma seedFlat_1 : seedFlatSqEdges 1 = 2 := rfl
77@[simp] lemma seedFlat_2 : seedFlatSqEdges 2 = 3 := rfl
78@[simp] lemma seedFlat_3 : seedFlatSqEdges 3 = 4 := rfl
79@[simp] lemma seedFlat_4 : seedFlatSqEdges 4 = 1 := rfl
80@[simp] lemma seedFlat_5 : seedFlatSqEdges 5 = 2 := rfl
81@[simp] lemma seedFlat_6 : seedFlatSqEdges 6 = 3 := rfl
82@[simp] lemma seedFlat_7 : seedFlatSqEdges 7 = 1 := rfl
83@[simp] lemma seedFlat_8 : seedFlatSqEdges 8 = 2 := rfl
84@[simp] lemma seedFlat_9 : seedFlatSqEdges 9 = 1 := rfl
85
86/-- ℕ mirror of the flat squared lengths (for kernel-decidable
87comparison with the incidence layer's masks). -/
88def seedFlatMaskNat : Fin 10 → ℕ
89 | 0 => 1 | 1 => 2 | 2 => 3 | 3 => 4 | 4 => 1
90 | 5 => 2 | 6 => 3 | 7 => 1 | 8 => 2 | 9 => 1
91
92lemma seedFlat_eq_cast (e : Fin 10) :
93 seedFlatSqEdges e = (seedFlatMaskNat e : ℝ) := by
94 fin_cases e <;> norm_num [seedFlatSqEdges, seedFlatMaskNat]
95
96/-- Bit weight of a 4-axis mask: unit Freudenthal steps flip one axis
97each, so the flat squared edge length is the number of set bits of the
98incidence layer's XOR mask. -/
99def maskWeight (m : ℕ) : ℕ :=
100 (if m.testBit 0 then 1 else 0) + (if m.testBit 1 then 1 else 0)
101 + (if m.testBit 2 then 1 else 0) + (if m.testBit 3 then 1 else 0)
102
103/-- THEOREM: the flat local squared lengths agree with the bit weights
104of the incidence layer's edge masks for seed simplex `0`. -/
105theorem seedFlatSqEdges_simplex0 (e : Fin 10) :
106 seedFlatSqEdges e = (maskWeight (localEdgeMask 0 e) : ℝ) := by
107 have h : ∀ e : Fin 10,
108 seedFlatMaskNat e = maskWeight (localEdgeMask 0 e) := by decide
109 rw [seedFlat_eq_cast, h e]
110
111/-- THEOREM: same agreement for seed simplex `1`. -/
112theorem seedFlatSqEdges_simplex1 (e : Fin 10) :
113 seedFlatSqEdges e = (maskWeight (localEdgeMask 1 e) : ℝ) := by
114 have h : ∀ e : Fin 10,
115 seedFlatMaskNat e = maskWeight (localEdgeMask 1 e) := by decide
116 rw [seedFlat_eq_cast, h e]
117
118/-! ## §2. Gram-projection cosine -/
119
120/-- `4⟨a,a⟩⟨b,b⟩ − (2⟨a,b⟩)²` for the hinge edge-vectors from vertex 0
121(`4·` the squared hinge area factor). -/
122def hingeGramDet (a : SqEdges4) : ℝ :=
123 4 * a 0 * a 1 - (a 0 + a 1 - a 4) ^ 2
124
125/-- Numerator of `⟨c',d'⟩ · hingeGramDet` (apex projections orthogonal
126to the hinge plane). -/
127def apexDotNum (a : SqEdges4) : ℝ :=
128 let den := hingeGramDet a
129 (-2) * a 0 * (a 1 + a 2 - a 7) * (a 1 + a 3 - a 8)
130 + (-2) * a 1 * (a 0 + a 2 - a 5) * (a 0 + a 3 - a 6)
131 + den * (a 2 + a 3 - a 9)
132 + (a 0 + a 1 - a 4) * (a 0 + a 2 - a 5) * (a 1 + a 3 - a 8)
133 + (a 0 + a 1 - a 4) * (a 0 + a 3 - a 6) * (a 1 + a 2 - a 7)
134
135/-- Numerator of `|c'|² · hingeGramDet`. -/
136def apex3NormSqNum (a : SqEdges4) : ℝ :=
137 let den := hingeGramDet a
138 (-a 0) * (a 1 + a 2 - a 7) ^ 2 + (-a 1) * (a 0 + a 2 - a 5) ^ 2
139 + a 2 * den
140 + (a 0 + a 1 - a 4) * (a 0 + a 2 - a 5) * (a 1 + a 2 - a 7)
141
142/-- Numerator of `|d'|² · hingeGramDet`. -/
143def apex4NormSqNum (a : SqEdges4) : ℝ :=
144 let den := hingeGramDet a
145 (-a 0) * (a 1 + a 3 - a 8) ^ 2 + (-a 1) * (a 0 + a 3 - a 6) ^ 2
146 + a 3 * den
147 + (a 0 + a 1 - a 4) * (a 0 + a 3 - a 6) * (a 1 + a 3 - a 8)
148
149def apexDot (a : SqEdges4) : ℝ := apexDotNum a / (2 * hingeGramDet a)
150def apex3NormSq (a : SqEdges4) : ℝ := apex3NormSqNum a / hingeGramDet a
151def apex4NormSq (a : SqEdges4) : ℝ := apex4NormSqNum a / hingeGramDet a
152
153/-- Cosine of the seed-hinge dihedral angle inside one 4-simplex. -/
154def cosDihedral (a : SqEdges4) : ℝ :=
155 apexDot a / Real.sqrt (apex3NormSq a * apex4NormSq a)
156
157/-- THEOREM: cleared-denominator form of the cosine wherever the hinge
158Gram determinant is positive. -/
159theorem cos_numForm (a : SqEdges4) (hden : 0 < hingeGramDet a) :
160 cosDihedral a =
161 apexDotNum a /
162 (2 * Real.sqrt (apex3NormSqNum a * apex4NormSqNum a)) := by
163 have hden' : hingeGramDet a ≠ 0 := ne_of_gt hden
164 simp only [cosDihedral, apexDot, apex3NormSq, apex4NormSq]
165 rw [show apex3NormSqNum a / hingeGramDet a *
166 (apex4NormSqNum a / hingeGramDet a)
167 = apex3NormSqNum a * apex4NormSqNum a / (hingeGramDet a) ^ 2 from by
168 rw [div_mul_div_comm, pow_two]]
169 rw [Real.sqrt_div' (apex3NormSqNum a * apex4NormSqNum a)
170 (sq_nonneg (hingeGramDet a))]
171 rw [Real.sqrt_sq hden.le]
172 by_cases hPQ : Real.sqrt (apex3NormSqNum a * apex4NormSqNum a) = 0
173 · rw [hPQ]
174 simp
175 · field_simp
176
177/-! ## §3. Flat evaluation -/
178
179theorem hingeGramDet_flat : hingeGramDet seedFlatSqEdges = 4 := by
180 norm_num [hingeGramDet]
181
182theorem apexDotNum_flat : apexDotNum seedFlatSqEdges = 8 := by
183 norm_num [apexDotNum, hingeGramDet]
184
185theorem apex3NormSqNum_flat : apex3NormSqNum seedFlatSqEdges = 4 := by
186 norm_num [apex3NormSqNum, hingeGramDet]
187
188theorem apex4NormSqNum_flat : apex4NormSqNum seedFlatSqEdges = 8 := by
189 norm_num [apex4NormSqNum, hingeGramDet]
190
191/-- THEOREM: flat cosine equals `1/√2`. -/
192theorem cosDihedral_flat :
193 cosDihedral seedFlatSqEdges = 1 / Real.sqrt 2 := by
194 rw [cos_numForm _ (by rw [hingeGramDet_flat]; norm_num),
195 apexDotNum_flat, apex3NormSqNum_flat, apex4NormSqNum_flat]
196 rw [show (4 : ℝ) * 8 = 32 by norm_num,
197 show (32 : ℝ) = 4 ^ 2 * 2 by norm_num,
198 Real.sqrt_mul (by positivity : (0 : ℝ) ≤ 4 ^ 2) 2,
199 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
200 rw [div_eq_div_iff (by positivity)
201 (ne_of_gt (Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)))]
202 ring
203
204/-- THEOREM: flat cosine squared is `1/2` (transcendental-free form). -/
205theorem cosDihedral_flat_sq :
206 cosDihedral seedFlatSqEdges ^ 2 = (1 / 2 : ℝ) := by
207 rw [cosDihedral_flat, div_pow, one_pow,
208 Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
209
210theorem cosDihedral_flat_pos : 0 < cosDihedral seedFlatSqEdges := by
211 rw [cosDihedral_flat]; positivity
212
213/-- THEOREM: flat sine from `sin² = 1 − cos²`, positive branch. -/
214theorem sinDihedral_flat :
215 Real.sqrt (1 - cosDihedral seedFlatSqEdges ^ 2) = 1 / Real.sqrt 2 := by
216 rw [cosDihedral_flat_sq, show (1 : ℝ) - 1 / 2 = 1 / 2 from by norm_num,
217 Real.sqrt_div (by norm_num : (0 : ℝ) ≤ 1) 2, Real.sqrt_one]
218
219/-! ## §4. Kernel table -/
220
221/-- Flat cosine derivatives with respect to the ten local squared
222lengths (all THEOREM via `hasDerivAt_cosDihedral_coord`). -/
223def cosDihedralKernel : Fin 10 → ℝ
224 | ⟨8, _⟩ => Real.sqrt 2 / 8
225 | ⟨9, _⟩ => -(Real.sqrt 2) / 4
226 | _ => 0
227
228lemma cosDihedralKernel_eight : cosDihedralKernel 8 = Real.sqrt 2 / 8 := rfl
229lemma cosDihedralKernel_nine : cosDihedralKernel 9 = -(Real.sqrt 2) / 4 := rfl
230
231lemma cosDihedralKernel_le_seven (k : Fin 10) (hk : k.val ≤ 7) :
232 cosDihedralKernel k = 0 := by
233 fin_cases k <;> first | rfl | exact absurd hk (by decide)
234
235/-- One-parameter path varying local slot `k` about the flat point. -/
236def coordPath (k : Fin 10) (t : ℝ) : SqEdges4 :=
237 fun j => if j = k then t else seedFlatSqEdges j
238
239/-! ## §5. Generic derivative machinery
240
241Every slot restriction of `cosDihedral` is `N(t) / (2√(P(t)·Q(t)))`
242for quadratics `N, P, Q` with flat values `(8, 4, 8)`; the flat
243derivative is `√2·(2N' − 2P' − Q')/32`. One lemma serves all ten
244slots. -/
245
246private lemma hasDerivAt_quadPoly (a b c t0 : ℝ) :
247 HasDerivAt (fun t : ℝ => a * t ^ 2 + b * t + c) (2 * a * t0 + b) t0 := by
248 have h1 : HasDerivAt (fun t : ℝ => t ^ 2) (2 * t0) t0 := by
249 simpa using hasDerivAt_pow 2 t0
250 have h2 : HasDerivAt (fun t : ℝ => a * t ^ 2) (a * (2 * t0)) t0 :=
251 h1.const_mul a
252 have h3 : HasDerivAt (fun t : ℝ => b * t) b t0 := by
253 simpa using (hasDerivAt_id t0).const_mul b
254 have h4 := (h2.add h3).add_const c
255 convert h4 using 1
256 ring
257
258private lemma hasDerivAt_numForm {N P Q : ℝ → ℝ} {t0 N' P' Q' : ℝ}
259 (hN : HasDerivAt N N' t0) (hP : HasDerivAt P P' t0)
260 (hQ : HasDerivAt Q Q' t0)
261 (hN0 : N t0 = 8) (hP0 : P t0 = 4) (hQ0 : Q t0 = 8) :
262 HasDerivAt (fun t => N t / (2 * Real.sqrt (P t * Q t)))
263 (Real.sqrt 2 * (2 * N' - 2 * P' - Q') / 32) t0 := by
264 have hs2 : Real.sqrt 2 * Real.sqrt 2 = 2 :=
265 Real.mul_self_sqrt (by norm_num)
266 have hPQ : HasDerivAt (fun t => P t * Q t)
267 (P' * Q t0 + P t0 * Q') t0 := hP.mul hQ
268 have hPQ0 : P t0 * Q t0 = 32 := by rw [hP0, hQ0]; norm_num
269 have hPQne : P t0 * Q t0 ≠ 0 := by rw [hPQ0]; norm_num
270 have hsqrt : HasDerivAt (fun t => Real.sqrt (P t * Q t))
271 ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0))) t0 :=
272 hPQ.sqrt hPQne
273 have hden : HasDerivAt (fun t => 2 * Real.sqrt (P t * Q t))
274 (2 * ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0)))) t0 :=
275 hsqrt.const_mul 2
276 have hdenne : 2 * Real.sqrt (P t0 * Q t0) ≠ 0 := by
277 rw [hPQ0]
278 positivity
279 have hdiv := hN.div hden hdenne
280 convert hdiv using 1
281 have h32 : Real.sqrt (P t0 * Q t0) = 4 * Real.sqrt 2 := by
282 rw [hPQ0, show (32 : ℝ) = 4 ^ 2 * 2 by norm_num,
283 Real.sqrt_mul (by positivity : (0 : ℝ) ≤ 4 ^ 2) 2,
284 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
285 rw [h32, hN0, hP0, hQ0]
286 have hpow : (2 * (4 * Real.sqrt 2)) ^ 2 = 128 := by
287 rw [show (2 * (4 * Real.sqrt 2)) ^ 2
288 = 64 * (Real.sqrt 2 * Real.sqrt 2) from by ring, hs2]
289 norm_num
290 rw [hpow]
291 have hdiv2 : ∀ X : ℝ,
292 X / (2 * (4 * Real.sqrt 2)) = X * Real.sqrt 2 / 16 := by
293 intro X
294 rw [div_eq_div_iff (by positivity) (by norm_num : (16 : ℝ) ≠ 0)]
295 rw [show X * Real.sqrt 2 * (2 * (4 * Real.sqrt 2))
296 = X * 8 * (Real.sqrt 2 * Real.sqrt 2) from by ring, hs2]
297 ring
298 rw [hdiv2]
299 ring
300
301private lemma hasDerivAt_slot (k : Fin 10) (t0 : ℝ)
302 (aN bN cN aP bP cP aQ bQ cQ aD bD cD : ℝ)
303 (hpath : ∀ t : ℝ,
304 apexDotNum (coordPath k t) = aN * t ^ 2 + bN * t + cN
305 ∧ apex3NormSqNum (coordPath k t) = aP * t ^ 2 + bP * t + cP
306 ∧ apex4NormSqNum (coordPath k t) = aQ * t ^ 2 + bQ * t + cQ
307 ∧ hingeGramDet (coordPath k t) = aD * t ^ 2 + bD * t + cD)
308 (hN0 : aN * t0 ^ 2 + bN * t0 + cN = 8)
309 (hP0 : aP * t0 ^ 2 + bP * t0 + cP = 4)
310 (hQ0 : aQ * t0 ^ 2 + bQ * t0 + cQ = 8)
311 (hD0 : 0 < aD * t0 ^ 2 + bD * t0 + cD) :
312 HasDerivAt (fun t : ℝ => cosDihedral (coordPath k t))
313 (Real.sqrt 2 * (2 * (2 * aN * t0 + bN) - 2 * (2 * aP * t0 + bP)
314 - (2 * aQ * t0 + bQ)) / 32) t0 := by
315 have hN := hasDerivAt_quadPoly aN bN cN t0
316 have hP := hasDerivAt_quadPoly aP bP cP t0
317 have hQ := hasDerivAt_quadPoly aQ bQ cQ t0
318 have hmain := hasDerivAt_numForm hN hP hQ hN0 hP0 hQ0
319 refine hmain.congr_of_eventuallyEq ?_
320 have hDcont : Continuous fun t : ℝ => aD * t ^ 2 + bD * t + cD := by
321 continuity
322 have hDev : ∀ᶠ t in nhds t0, 0 < aD * t ^ 2 + bD * t + cD :=
323 (hDcont.tendsto t0).eventually (eventually_gt_nhds hD0)
324 filter_upwards [hDev] with t ht
325 have hp := hpath t
326 rw [cos_numForm (coordPath k t) (by rw [hp.2.2.2]; exact ht),
327 hp.1, hp.2.1, hp.2.2.1]
328
329/-! ## §6. Per-slot path polynomials (verified against the Gram form) -/
330
331private lemma path0_polys : ∀ t : ℝ,
332 apexDotNum (coordPath 0 t) = (-2) * t ^ 2 + 12 * t + (-2)
333 ∧ apex3NormSqNum (coordPath 0 t) = (-1) * t ^ 2 + 6 * t + (-1)
334 ∧ apex4NormSqNum (coordPath 0 t) = (-2) * t ^ 2 + 12 * t + (-2)
335 ∧ hingeGramDet (coordPath 0 t) = (-1) * t ^ 2 + 6 * t + (-1) := by
336 intro t
337 refine ⟨?_, ?_, ?_, ?_⟩ <;>
338 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
339 coordPath] <;> ring
340
341private lemma path1_polys : ∀ t : ℝ,
342 apexDotNum (coordPath 1 t) = (-4) * t ^ 2 + 16 * t + (-8)
343 ∧ apex3NormSqNum (coordPath 1 t) = (-2) * t ^ 2 + 8 * t + (-4)
344 ∧ apex4NormSqNum (coordPath 1 t) = (-3) * t ^ 2 + 12 * t + (-4)
345 ∧ hingeGramDet (coordPath 1 t) = (-1) * t ^ 2 + 4 * t + 0 := by
346 intro t
347 refine ⟨?_, ?_, ?_, ?_⟩ <;>
348 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
349 coordPath] <;> ring
350
351private lemma path2_polys : ∀ t : ℝ,
352 apexDotNum (coordPath 2 t) = 0 * t ^ 2 + 0 * t + 8
353 ∧ apex3NormSqNum (coordPath 2 t) = (-1) * t ^ 2 + 6 * t + (-5)
354 ∧ apex4NormSqNum (coordPath 2 t) = 0 * t ^ 2 + 0 * t + 8
355 ∧ hingeGramDet (coordPath 2 t) = 0 * t ^ 2 + 0 * t + 4 := by
356 intro t
357 refine ⟨?_, ?_, ?_, ?_⟩ <;>
358 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
359 coordPath] <;> ring
360
361private lemma path3_polys : ∀ t : ℝ,
362 apexDotNum (coordPath 3 t) = 0 * t ^ 2 + 0 * t + 8
363 ∧ apex3NormSqNum (coordPath 3 t) = 0 * t ^ 2 + 0 * t + 4
364 ∧ apex4NormSqNum (coordPath 3 t) = (-1) * t ^ 2 + 8 * t + (-8)
365 ∧ hingeGramDet (coordPath 3 t) = 0 * t ^ 2 + 0 * t + 4 := by
366 intro t
367 refine ⟨?_, ?_, ?_, ?_⟩ <;>
368 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
369 coordPath] <;> ring
370
371private lemma path4_polys : ∀ t : ℝ,
372 apexDotNum (coordPath 4 t) = (-6) * t ^ 2 + 20 * t + (-6)
373 ∧ apex3NormSqNum (coordPath 4 t) = (-3) * t ^ 2 + 10 * t + (-3)
374 ∧ apex4NormSqNum (coordPath 4 t) = (-4) * t ^ 2 + 16 * t + (-4)
375 ∧ hingeGramDet (coordPath 4 t) = (-1) * t ^ 2 + 6 * t + (-1) := by
376 intro t
377 refine ⟨?_, ?_, ?_, ?_⟩ <;>
378 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
379 coordPath] <;> ring
380
381private lemma path5_polys : ∀ t : ℝ,
382 apexDotNum (coordPath 5 t) = 0 * t ^ 2 + 0 * t + 8
383 ∧ apex3NormSqNum (coordPath 5 t) = (-2) * t ^ 2 + 8 * t + (-4)
384 ∧ apex4NormSqNum (coordPath 5 t) = 0 * t ^ 2 + 0 * t + 8
385 ∧ hingeGramDet (coordPath 5 t) = 0 * t ^ 2 + 0 * t + 4 := by
386 intro t
387 refine ⟨?_, ?_, ?_, ?_⟩ <;>
388 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
389 coordPath] <;> ring
390
391private lemma path6_polys : ∀ t : ℝ,
392 apexDotNum (coordPath 6 t) = 0 * t ^ 2 + 0 * t + 8
393 ∧ apex3NormSqNum (coordPath 6 t) = 0 * t ^ 2 + 0 * t + 4
394 ∧ apex4NormSqNum (coordPath 6 t) = (-2) * t ^ 2 + 12 * t + (-10)
395 ∧ hingeGramDet (coordPath 6 t) = 0 * t ^ 2 + 0 * t + 4 := by
396 intro t
397 refine ⟨?_, ?_, ?_, ?_⟩ <;>
398 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
399 coordPath] <;> ring
400
401private lemma path7_polys : ∀ t : ℝ,
402 apexDotNum (coordPath 7 t) = 0 * t ^ 2 + 4 * t + 4
403 ∧ apex3NormSqNum (coordPath 7 t) = (-1) * t ^ 2 + 6 * t + (-1)
404 ∧ apex4NormSqNum (coordPath 7 t) = 0 * t ^ 2 + 0 * t + 8
405 ∧ hingeGramDet (coordPath 7 t) = 0 * t ^ 2 + 0 * t + 4 := by
406 intro t
407 refine ⟨?_, ?_, ?_, ?_⟩ <;>
408 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
409 coordPath] <;> ring
410
411private lemma path8_polys : ∀ t : ℝ,
412 apexDotNum (coordPath 8 t) = 0 * t ^ 2 + 4 * t + 0
413 ∧ apex3NormSqNum (coordPath 8 t) = 0 * t ^ 2 + 0 * t + 4
414 ∧ apex4NormSqNum (coordPath 8 t) = (-1) * t ^ 2 + 8 * t + (-4)
415 ∧ hingeGramDet (coordPath 8 t) = 0 * t ^ 2 + 0 * t + 4 := by
416 intro t
417 refine ⟨?_, ?_, ?_, ?_⟩ <;>
418 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
419 coordPath] <;> ring
420
421private lemma path9_polys : ∀ t : ℝ,
422 apexDotNum (coordPath 9 t) = 0 * t ^ 2 + (-4) * t + 12
423 ∧ apex3NormSqNum (coordPath 9 t) = 0 * t ^ 2 + 0 * t + 4
424 ∧ apex4NormSqNum (coordPath 9 t) = 0 * t ^ 2 + 0 * t + 8
425 ∧ hingeGramDet (coordPath 9 t) = 0 * t ^ 2 + 0 * t + 4 := by
426 intro t
427 refine ⟨?_, ?_, ?_, ?_⟩ <;>
428 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
429 coordPath] <;> ring
430
431/-! ## §7. The ten coordinate derivatives (deliverable A) -/
432
433theorem hasDerivAt_cosDihedral_slot0 :
434 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 0 t)) 0 1 := by
435 have h := hasDerivAt_slot 0 1 (-2) 12 (-2) (-1) 6 (-1) (-2) 12 (-2)
436 (-1) 6 (-1) path0_polys (by norm_num) (by norm_num) (by norm_num)
437 (by norm_num)
438 convert h using 1
439 ring
440
441theorem hasDerivAt_cosDihedral_slot1 :
442 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 1 t)) 0 2 := by
443 have h := hasDerivAt_slot 1 2 (-4) 16 (-8) (-2) 8 (-4) (-3) 12 (-4)
444 (-1) 4 0 path1_polys (by norm_num) (by norm_num) (by norm_num)
445 (by norm_num)
446 convert h using 1
447 ring
448
449theorem hasDerivAt_cosDihedral_slot2 :
450 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 2 t)) 0 3 := by
451 have h := hasDerivAt_slot 2 3 0 0 8 (-1) 6 (-5) 0 0 8 0 0 4
452 path2_polys (by norm_num) (by norm_num) (by norm_num) (by norm_num)
453 convert h using 1
454 ring
455
456theorem hasDerivAt_cosDihedral_slot3 :
457 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 3 t)) 0 4 := by
458 have h := hasDerivAt_slot 3 4 0 0 8 0 0 4 (-1) 8 (-8) 0 0 4
459 path3_polys (by norm_num) (by norm_num) (by norm_num) (by norm_num)
460 convert h using 1
461 ring
462
463theorem hasDerivAt_cosDihedral_slot4 :
464 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 4 t)) 0 1 := by
465 have h := hasDerivAt_slot 4 1 (-6) 20 (-6) (-3) 10 (-3) (-4) 16 (-4)
466 (-1) 6 (-1) path4_polys (by norm_num) (by norm_num) (by norm_num)
467 (by norm_num)
468 convert h using 1
469 ring
470
471theorem hasDerivAt_cosDihedral_slot5 :
472 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 5 t)) 0 2 := by
473 have h := hasDerivAt_slot 5 2 0 0 8 (-2) 8 (-4) 0 0 8 0 0 4
474 path5_polys (by norm_num) (by norm_num) (by norm_num) (by norm_num)
475 convert h using 1
476 ring
477
478theorem hasDerivAt_cosDihedral_slot6 :
479 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 6 t)) 0 3 := by
480 have h := hasDerivAt_slot 6 3 0 0 8 0 0 4 (-2) 12 (-10) 0 0 4
481 path6_polys (by norm_num) (by norm_num) (by norm_num) (by norm_num)
482 convert h using 1
483 ring
484
485theorem hasDerivAt_cosDihedral_slot7 :
486 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 7 t)) 0 1 := by
487 have h := hasDerivAt_slot 7 1 0 4 4 (-1) 6 (-1) 0 0 8 0 0 4
488 path7_polys (by norm_num) (by norm_num) (by norm_num) (by norm_num)
489 convert h using 1
490 ring
491
492theorem hasDerivAt_cosDihedral_slot8 :
493 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 8 t))
494 (Real.sqrt 2 / 8) 2 := by
495 have h := hasDerivAt_slot 8 2 0 4 0 0 0 4 (-1) 8 (-4) 0 0 4
496 path8_polys (by norm_num) (by norm_num) (by norm_num) (by norm_num)
497 convert h using 1
498 ring
499
500theorem hasDerivAt_cosDihedral_slot9 :
501 HasDerivAt (fun t : ℝ => cosDihedral (coordPath 9 t))
502 (-(Real.sqrt 2) / 4) 1 := by
503 have h := hasDerivAt_slot 9 1 0 (-4) 12 0 0 4 0 0 8 0 0 4
504 path9_polys (by norm_num) (by norm_num) (by norm_num) (by norm_num)
505 convert h using 1
506 ring
507
508/-- THEOREM (deliverable A): every local squared-length direction has an
509explicit flat cosine derivative given by `cosDihedralKernel`. -/
510theorem hasDerivAt_cosDihedral_coord (k : Fin 10) :
511 HasDerivAt (fun t : ℝ => cosDihedral (coordPath k t))
512 (cosDihedralKernel k) (seedFlatSqEdges k) := by
513 fin_cases k
514 · exact hasDerivAt_cosDihedral_slot0
515 · exact hasDerivAt_cosDihedral_slot1
516 · exact hasDerivAt_cosDihedral_slot2
517 · exact hasDerivAt_cosDihedral_slot3
518 · exact hasDerivAt_cosDihedral_slot4
519 · exact hasDerivAt_cosDihedral_slot5
520 · exact hasDerivAt_cosDihedral_slot6
521 · exact hasDerivAt_cosDihedral_slot7
522 · exact hasDerivAt_cosDihedral_slot8
523 · exact hasDerivAt_cosDihedral_slot9
524
525/-! ## §8. Angle and two-simplex partial-deficit class kernels -/
526
527/-- Angle kernel `θ' = -(1/sin θ)·cos'` with flat `1/sin = √2`. -/
528def angleKernel (k : Fin 10) : ℝ := -(Real.sqrt 2) * cosDihedralKernel k
529
530/-- One seed simplex's contribution to the deficit gradient
531(`δ = 2π − Σθ`, so per-simplex `-θ'`). -/
532def singleSimplexDeficitKernel (k : Fin 10) : ℝ := -angleKernel k
533
534theorem angleKernel_eight : angleKernel 8 = (-1 / 4 : ℝ) := by
535 simp only [angleKernel, cosDihedralKernel_eight]
536 rw [show -(Real.sqrt 2) * (Real.sqrt 2 / 8)
537 = -((Real.sqrt 2 * Real.sqrt 2) / 8) from by ring,
538 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
539 norm_num
540
541theorem angleKernel_nine : angleKernel 9 = (1 / 2 : ℝ) := by
542 simp only [angleKernel, cosDihedralKernel_nine]
543 rw [show -(Real.sqrt 2) * (-(Real.sqrt 2) / 4)
544 = (Real.sqrt 2 * Real.sqrt 2) / 4 from by ring,
545 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
546 norm_num
547
548theorem singleSimplexDeficitKernel_eight :
549 singleSimplexDeficitKernel 8 = (1 / 4 : ℝ) := by
550 simp only [singleSimplexDeficitKernel]
551 rw [angleKernel_eight]
552 norm_num
553
554theorem singleSimplexDeficitKernel_nine :
555 singleSimplexDeficitKernel 9 = (-1 / 2 : ℝ) := by
556 simp only [singleSimplexDeficitKernel]
557 rw [angleKernel_nine]
558 norm_num
559
560theorem singleSimplexDeficitKernel_le_seven (k : Fin 10) (hk : k.val ≤ 7) :
561 singleSimplexDeficitKernel k = 0 := by
562 simp [singleSimplexDeficitKernel, angleKernel,
563 cosDihedralKernel_le_seven k hk]
564
565/-- Sum over `Fin 10` of a function supported on slots 8 and 9. -/
566private lemma sum_fin10_split (f : Fin 10 → ℝ)
567 (hz : ∀ e : Fin 10, e.val ≤ 7 → f e = 0) :
568 (∑ e : Fin 10, f e) = f 8 + f 9 := by
569 have hmem : ∀ e : Fin 10,
570 e ∈ ({0, 1, 2, 3, 4, 5, 6, 7} : Finset (Fin 10)) → e.val ≤ 7 := by
571 decide
572 rw [show (Finset.univ : Finset (Fin 10))
573 = insert 8 (insert 9 ({0, 1, 2, 3, 4, 5, 6, 7} : Finset (Fin 10)))
574 from by decide]
575 rw [Finset.sum_insert (by decide), Finset.sum_insert (by decide),
576 Finset.sum_eq_zero (fun e he => hz e (hmem e he))]
577 ring
578
579/-- Assemble a local Fin-10 kernel onto the 15 edge classes through one
580simplex's local edge table. -/
581def assembleClassKernel (s : Fin 24) (localK : Fin 10 → ℝ) : Fin 15 → ℝ :=
582 fun d => ∑ e : Fin 10, if localEdgeClass s e = d then localK e else 0
583
584/-- Two-simplex partial deficit class kernel
585`∂(2π − θ₀ − θ₁)/∂ℓ²_class` at flat. -/
586def partialDeficitClassKernel : Fin 15 → ℝ :=
587 fun d =>
588 assembleClassKernel 0 singleSimplexDeficitKernel d +
589 assembleClassKernel 1 singleSimplexDeficitKernel d
590
591/-- THEOREM: the assembly reduces to the two active local slots. -/
592theorem assembleClassKernel_eval (s : Fin 24) (d : Fin 15) :
593 assembleClassKernel s singleSimplexDeficitKernel d =
594 (if localEdgeClass s 8 = d then singleSimplexDeficitKernel 8 else 0)
595 + (if localEdgeClass s 9 = d then singleSimplexDeficitKernel 9
596 else 0) := by
597 unfold assembleClassKernel
598 exact sum_fin10_split _
599 (fun e he => by rw [singleSimplexDeficitKernel_le_seven e he, ite_self])
600
601theorem partialDeficitClassKernel_three :
602 partialDeficitClassKernel 3 = (-1 / 2 : ℝ) := by
603 simp only [partialDeficitClassKernel]
604 rw [assembleClassKernel_eval, assembleClassKernel_eval]
605 rw [if_neg (by decide : ¬ localEdgeClass 0 8 = 3),
606 if_neg (by decide : ¬ localEdgeClass 0 9 = 3),
607 if_neg (by decide : ¬ localEdgeClass 1 8 = 3),
608 if_pos (by decide : localEdgeClass 1 9 = 3),
609 singleSimplexDeficitKernel_nine]
610 norm_num
611
612theorem partialDeficitClassKernel_seven :
613 partialDeficitClassKernel 7 = (-1 / 2 : ℝ) := by
614 simp only [partialDeficitClassKernel]
615 rw [assembleClassKernel_eval, assembleClassKernel_eval]
616 rw [if_neg (by decide : ¬ localEdgeClass 0 8 = 7),
617 if_pos (by decide : localEdgeClass 0 9 = 7),
618 if_neg (by decide : ¬ localEdgeClass 1 8 = 7),
619 if_neg (by decide : ¬ localEdgeClass 1 9 = 7),
620 singleSimplexDeficitKernel_nine]
621 norm_num
622
623theorem partialDeficitClassKernel_eleven :
624 partialDeficitClassKernel 11 = (1 / 2 : ℝ) := by
625 simp only [partialDeficitClassKernel]
626 rw [assembleClassKernel_eval, assembleClassKernel_eval]
627 rw [if_pos (by decide : localEdgeClass 0 8 = 11),
628 if_neg (by decide : ¬ localEdgeClass 0 9 = 11),
629 if_pos (by decide : localEdgeClass 1 8 = 11),
630 if_neg (by decide : ¬ localEdgeClass 1 9 = 11),
631 singleSimplexDeficitKernel_eight]
632 norm_num
633
634/-- THEOREM: the partial deficit kernel vanishes off classes 3, 7, 11. -/
635theorem partialDeficitClassKernel_zero_off (d : Fin 15)
636 (h3 : d ≠ 3) (h7 : d ≠ 7) (h11 : d ≠ 11) :
637 partialDeficitClassKernel d = 0 := by
638 simp only [partialDeficitClassKernel]
639 rw [assembleClassKernel_eval, assembleClassKernel_eval]
640 rw [show localEdgeClass 0 8 = 11 from by decide,
641 show localEdgeClass 0 9 = 7 from by decide,
642 show localEdgeClass 1 8 = 11 from by decide,
643 show localEdgeClass 1 9 = 3 from by decide]
644 rw [if_neg (show ¬((11 : Fin 15) = d) from fun h => h11 h.symm),
645 if_neg (show ¬((7 : Fin 15) = d) from fun h => h7 h.symm),
646 if_neg (show ¬((3 : Fin 15) = d) from fun h => h3 h.symm)]
647 norm_num
648
649theorem partialDeficitClassKernel_values :
650 partialDeficitClassKernel 3 = (-1 / 2 : ℝ) ∧
651 partialDeficitClassKernel 7 = (-1 / 2 : ℝ) ∧
652 partialDeficitClassKernel 11 = (1 / 2 : ℝ) :=
653 ⟨partialDeficitClassKernel_three, partialDeficitClassKernel_seven,
654 partialDeficitClassKernel_eleven⟩
655
656/-! ## §9. Nonvacuity, symmetry, decoy -/
657
658/-- THEOREM (nonvacuity): the slot-9 cosine kernel is nonzero. -/
659theorem cosDihedralKernel_nonvacuous : cosDihedralKernel 9 ≠ 0 := by
660 rw [cosDihedralKernel_nine]
661 have h2 : (0 : ℝ) < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num)
662 intro h
663 linarith
664
665/-- Directional cosine derivative along a local direction `v`. -/
666def cosDirectional (v : Fin 10 → ℝ) : ℝ :=
667 ∑ k : Fin 10, v k * cosDihedralKernel k
668
669/-- THEOREM (decoy, computed honestly): uniform scaling of the squared
670lengths is NOT stationary; the value is `-√2/8`. -/
671theorem cosDihedral_uniformScale_decoy :
672 cosDirectional (fun _ => (1 : ℝ)) = -(Real.sqrt 2) / 8 := by
673 simp only [cosDirectional]
674 rw [sum_fin10_split _
675 (fun e he => by rw [cosDihedralKernel_le_seven e he, mul_zero])]
676 rw [cosDihedralKernel_eight, cosDihedralKernel_nine]
677 ring
678
679/-- THEOREM: the true homothety direction (scaling every flat squared
680length by the same factor) is stationary, as scale invariance of the
681angle demands. -/
682theorem cosDihedral_homothety_stationary :
683 cosDirectional seedFlatSqEdges = 0 := by
684 simp only [cosDirectional]
685 rw [sum_fin10_split _
686 (fun e he => by rw [cosDihedralKernel_le_seven e he, mul_zero])]
687 rw [cosDihedralKernel_eight, cosDihedralKernel_nine, seedFlat_8,
688 seedFlat_9]
689 ring
690
691/-- THEOREM (symmetry): the partial deficit class kernel is invariant
692under the hinge-fixing axis swap `2 ↔ 3` of the incidence layer. -/
693theorem partialDeficitClassKernel_swap23 (d : Fin 15) :
694 partialDeficitClassKernel (swap23Class d) =
695 partialDeficitClassKernel d := by
696 have hinv : ∀ x : Fin 15, swap23Class (swap23Class x) = x := by decide
697 have hs3 : swap23Class 3 = 7 := by decide
698 have hs7 : swap23Class 7 = 3 := by decide
699 have hs11 : swap23Class 11 = 11 := by decide
700 by_cases h3 : d = 3
701 · subst h3
702 rw [hs3, partialDeficitClassKernel_seven, partialDeficitClassKernel_three]
703 by_cases h7 : d = 7
704 · subst h7
705 rw [hs7, partialDeficitClassKernel_three, partialDeficitClassKernel_seven]
706 by_cases h11 : d = 11
707 · subst h11
708 rw [hs11]
709 have g3 : swap23Class d ≠ 3 := fun h => h7 (by rw [← hinv d, h, hs3])
710 have g7 : swap23Class d ≠ 7 := fun h => h3 (by rw [← hinv d, h, hs7])
711 have g11 : swap23Class d ≠ 11 := fun h => h11 (by rw [← hinv d, h, hs11])
712 rw [partialDeficitClassKernel_zero_off _ g3 g7 g11,
713 partialDeficitClassKernel_zero_off _ h3 h7 h11]
714
715/-! ## §10. Status -/
716
717structure Hinge4DDihedralKernelStatus where
718 seedCosineFlatClosed : Bool
719 tenCoordDerivativesClosed : Bool
720 twoSimplexPartialDeficitClosed : Bool
721 fullLatticeOrbitOpen : Bool
722 convergesEH4d : Bool
723 gapActionRecovery : Bool
724
725def hinge4DDihedralKernelStatus : Hinge4DDihedralKernelStatus where
726 seedCosineFlatClosed := true
727 tenCoordDerivativesClosed := true
728 twoSimplexPartialDeficitClosed := true
729 fullLatticeOrbitOpen := true
730 convergesEH4d := false
731 gapActionRecovery := false
732
733theorem hinge4DDihedralKernelStatus_flags :
734 hinge4DDihedralKernelStatus.seedCosineFlatClosed = true ∧
735 hinge4DDihedralKernelStatus.tenCoordDerivativesClosed = true ∧
736 hinge4DDihedralKernelStatus.twoSimplexPartialDeficitClosed = true ∧
737 hinge4DDihedralKernelStatus.fullLatticeOrbitOpen = true ∧
738 hinge4DDihedralKernelStatus.convergesEH4d = false ∧
739 hinge4DDihedralKernelStatus.gapActionRecovery = false := by
740 decide
741
742end
743
744end ReggeHinge4DDihedralKernel
745end Analysis
746end Gravity
747end IndisputableMonolith
748