IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DStarKernel13.lean · 794 lines · 90 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 type-(1,3) periodic-lattice star deficit class kernel
8
9QG full-theory campaign, next kernel-checked increment after
10`ReggeHinge4DStarKernel` (type `(1,1)` seed orbit) and
11`ReggeHinge4DOrbitClassification`. Imports the Freudenthal incidence
12layer, the 15-class stencil, and the Gram-projection cosine calculus;
13never redefines their API.
14
15## Tier tags (binding)
16
17* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
18 `admit`, no new axioms, no `native_decide`, no `: True` shells).
19* Scope: the type-`(1,3)` triangle hinge with absolute masks
20 `{0, e₀, e₀+e₁+e₂+e₃}` = `{0,1,15}` (difference masks `(1,14)`,
21 local flat squared lengths `(1,3,4)`) and its **full** periodic
22 Freudenthal star. The complementary type `(3,1)` is related by
23 mask complement in the classification layer; transport of this
24 kernel to `(3,1)` is **OPEN**.
25* This does **not** complete the flat Hessian assembly over all hinges.
26* This does **not** prove `S_RS_converges_EH_4d`.
27* This does **not** flip `gap_action_recovery`.
28* This does **not** reverse-engineer weights from Einstein–Hilbert.
29
30## What is proved (deliverable A)
31
321. **Star enumeration.** Exactly six Kuhn simplices in the origin unit
33 cube contain the hinge; among cube translates in `{-1,0,1}⁴` only
34 the origin contains it (decidable search).
352. **Flat cosine multiset.** All six simplices have flat cosine `1/2`,
36 from the shared Gram vector of local squared lengths.
373. **Flatness gate.** Star angle sum equals exactly `2π`
38 (`6 · arccos(1/2) = 6 · (π/3)`).
394. **All ten coordinate derivatives** via the cleared-denominator
40 master lemma at flat values `(N,P,Q) = (8,8,8)`.
415. **Full-star deficit class kernel** on classes
42 `(1,3,5,7,9,11,13)` with values
43 `(-√3,-√3,+√3,-√3,+√3,+√3,-√3)`.
446. **Gates:** nonvacuity, hinge-fixing transposition `1↔2` of axes
45 `{1,2,3}`, uniform-scaling decoy, homothety stationarity exactly `0`.
46
47Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
48-/
49
50namespace IndisputableMonolith
51namespace Gravity
52namespace Analysis
53namespace ReggeHinge4DStarKernel13
54
55open BigOperators
56open ReggeHinge4DFlatKernel
57open ReggeHinge4DDihedralKernel
58open ReggeEdgeStencil4D
59
60noncomputable section
61
62/-! ## §1. Cube translates and star enumeration -/
63
64/-- Candidate unit-cube origins with each coordinate in `{-1,0,1}`,
65encoded as `Fin 3` values `0,1,2`. A vertex with absolute coordinate
66`v ∈ {0,1}` lies in the cube of origin-index `o` iff
67`o ≤ v+1 ≤ o+1` (equivalently the shifted interval test). -/
68abbrev CubeOffset := Fin 3 × Fin 3 × Fin 3 × Fin 3
69
70def offsetAxis : CubeOffset → Fin 4 → Fin 3
71 | c, 0 => c.1
72 | c, 1 => c.2.1
73 | c, 2 => c.2.2.1
74 | c, 3 => c.2.2.2
75
76/-- Absolute hinge vertex coordinates in `{0,1}⁴`. -/
77def absHingeCoord : Fin 3 → Fin 4 → Fin 2
78 | 0, _ => 0
79 | 1, 0 => 1
80 | 1, _ => 0
81 | 2, _ => 1
82
83def axisFits (o : Fin 3) (v : Fin 2) : Bool :=
84 decide (o.val ≤ v.val + 1 ∧ v.val + 1 ≤ o.val + 1)
85
86def vertexInCube (c : CubeOffset) (k : Fin 3) : Bool :=
87 decide (∀ i : Fin 4, axisFits (offsetAxis c i) (absHingeCoord k i) = true)
88
89def cubeContainsHinge (c : CubeOffset) : Bool :=
90 decide (∀ k : Fin 3, vertexInCube c k = true)
91
92def originOffset : CubeOffset :=
93 (⟨1, by decide⟩, ⟨1, by decide⟩, ⟨1, by decide⟩, ⟨1, by decide⟩)
94
95theorem cubeContainsHinge_origin : cubeContainsHinge originOffset = true := by
96 decide
97
98theorem star_cube_cardinality :
99 (Finset.univ.filter (fun c : CubeOffset =>
100 cubeContainsHinge c = true)).card = 1 := by
101 decide
102
103theorem only_origin_contains_hinge :
104 (Finset.univ.filter (fun c : CubeOffset =>
105 cubeContainsHinge c = true)) = {originOffset} := by
106 decide
107
108/-- Local masks of the type-`(1,3)` hinge in the origin cube. -/
109def localHingeMasks : Finset ℕ := {0, 1, 15}
110
111
112def containsHinge (s : Fin 24) : Bool :=
113 decide (∀ m ∈ localHingeMasks, ∃ i : Fin 5, vertexMask s i = m)
114
115def starMembers : List (Fin 24) := [0, 1, 2, 3, 4, 5]
116
117theorem starMembers_length : starMembers.length = 6 := rfl
118
119theorem starMembers_complete (s : Fin 24) :
120 containsHinge s = true ↔ s ∈ starMembers := by
121 fin_cases s <;> decide
122
123theorem star_cardinality :
124 (Finset.univ.filter (fun s : Fin 24 => containsHinge s = true)).card =
125 6 := by
126 decide
127
128/-! ## §2. Flat squared-length representative (hinge ordered `0,1,15`) -/
129
130/-- Flat local squared edges for every star member after reordering the
131five vertices so the hinge occupies slots `(0,1,2)` and the two apexes
132follow Freudenthal chain order. -/
133def t13FlatSqEdges : SqEdges4
134 | 0 => 1 | 1 => 4 | 2 => 2 | 3 => 3 | 4 => 3
135 | 5 => 1 | 6 => 2 | 7 => 2 | 8 => 1 | 9 => 1
136
137theorem hingeGramDet_t13 : hingeGramDet t13FlatSqEdges = 12 := by
138 norm_num [hingeGramDet, t13FlatSqEdges]
139theorem apexDotNum_t13 : apexDotNum t13FlatSqEdges = 8 := by
140 norm_num [apexDotNum, hingeGramDet, t13FlatSqEdges]
141theorem apex3NormSqNum_t13 : apex3NormSqNum t13FlatSqEdges = 8 := by
142 norm_num [apex3NormSqNum, hingeGramDet, t13FlatSqEdges]
143theorem apex4NormSqNum_t13 : apex4NormSqNum t13FlatSqEdges = 8 := by
144 norm_num [apex4NormSqNum, hingeGramDet, t13FlatSqEdges]
145
146theorem cosDihedral_t13_flat :
147 cosDihedral t13FlatSqEdges = (1 / 2 : ℝ) := by
148 rw [cos_numForm _ (by rw [hingeGramDet_t13]; norm_num),
149 apexDotNum_t13, apex3NormSqNum_t13, apex4NormSqNum_t13]
150 rw [show (8 : ℝ) * 8 = 64 by norm_num,
151 show Real.sqrt (64 : ℝ) = 8 by
152 rw [show (64 : ℝ) = (8 : ℝ) ^ 2 by norm_num,
153 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 8)]]
154 norm_num
155
156/-! ## §3. Flatness gate -/
157
158theorem arccos_one_half : Real.arccos (1 / 2 : ℝ) = Real.pi / 3 := by
159 have hcos : Real.cos (Real.pi / 3) = (1 / 2 : ℝ) := Real.cos_pi_div_three
160 rw [← hcos, Real.arccos_cos (by positivity) (by
161 have : (0 : ℝ) < Real.pi := Real.pi_pos
162 linarith [show Real.pi / 3 ≤ Real.pi from by linarith])]
163
164def flatAngleT13 : ℝ := Real.arccos (1 / 2 : ℝ)
165
166theorem flatAngleT13_eq : flatAngleT13 = Real.pi / 3 := arccos_one_half
167
168def starFlatAngleSum : ℝ := 6 * flatAngleT13
169
170theorem star_flat_angle_sum_two_pi : starFlatAngleSum = 2 * Real.pi := by
171 simp only [starFlatAngleSum, flatAngleT13_eq]
172 ring
173
174def starFlatCosines : Fin 6 → ℝ := fun _ => (1 / 2 : ℝ)
175
176theorem starFlatCosines_match :
177 ∀ m : Fin 6, starFlatCosines m = cosDihedral t13FlatSqEdges := by
178 intro m
179 simp [starFlatCosines, cosDihedral_t13_flat]
180
181/-! ## §4. Coordinate derivatives (master lemma at `(N,P,Q)=(8,8,8)`) -/
182
183def t13CoordPath (k : Fin 10) (t : ℝ) : SqEdges4 :=
184 fun j => if j = k then t else t13FlatSqEdges j
185
186def t13CosKernel : Fin 10 → ℝ
187 | ⟨4, _⟩ => (-1 / 4 : ℝ)
188 | ⟨6, _⟩ => (3 / 8 : ℝ)
189 | ⟨7, _⟩ => (3 / 8 : ℝ)
190 | ⟨9, _⟩ => (-3 / 4 : ℝ)
191 | _ => 0
192
193private lemma hasDerivAt_quadPoly (a b c t0 : ℝ) :
194 HasDerivAt (fun t : ℝ => a * t ^ 2 + b * t + c) (2 * a * t0 + b) t0 := by
195 have h1 : HasDerivAt (fun t : ℝ => t ^ 2) (2 * t0) t0 := by
196 simpa using hasDerivAt_pow 2 t0
197 have h2 : HasDerivAt (fun t : ℝ => a * t ^ 2) (a * (2 * t0)) t0 :=
198 h1.const_mul a
199 have h3 : HasDerivAt (fun t : ℝ => b * t) b t0 := by
200 simpa using (hasDerivAt_id t0).const_mul b
201 have h4 := (h2.add h3).add_const c
202 convert h4 using 1
203 ring
204
205/-- Cleared-denominator master derivative at flat `(N,P,Q)=(8,8,8)`. -/
206private lemma hasDerivAt_numForm_t13 {N P Q : ℝ → ℝ} {t0 N' P' Q' : ℝ}
207 (hN : HasDerivAt N N' t0) (hP : HasDerivAt P P' t0)
208 (hQ : HasDerivAt Q Q' t0)
209 (hN0 : N t0 = 8) (hP0 : P t0 = 8) (hQ0 : Q t0 = 8) :
210 HasDerivAt (fun t => N t / (2 * Real.sqrt (P t * Q t)))
211 ((2 * N' - P' - Q') / 32) t0 := by
212 have hPQ : HasDerivAt (fun t => P t * Q t)
213 (P' * Q t0 + P t0 * Q') t0 := hP.mul hQ
214 have hPQ0 : P t0 * Q t0 = 64 := by rw [hP0, hQ0]; norm_num
215 have hPQne : P t0 * Q t0 ≠ 0 := by rw [hPQ0]; norm_num
216 have hsqrt : HasDerivAt (fun t => Real.sqrt (P t * Q t))
217 ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0))) t0 :=
218 hPQ.sqrt hPQne
219 have hden : HasDerivAt (fun t => 2 * Real.sqrt (P t * Q t))
220 (2 * ((P' * Q t0 + P t0 * Q') / (2 * Real.sqrt (P t0 * Q t0)))) t0 :=
221 hsqrt.const_mul 2
222 have hdenne : 2 * Real.sqrt (P t0 * Q t0) ≠ 0 := by
223 rw [hPQ0]; positivity
224 have hdiv := hN.div hden hdenne
225 convert hdiv using 1
226 have h8 : Real.sqrt (P t0 * Q t0) = 8 := by
227 rw [hPQ0, show (64 : ℝ) = (8 : ℝ) ^ 2 by norm_num,
228 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 8)]
229 rw [h8, hN0, hP0, hQ0]
230 ring
231
232private lemma hasDerivAt_t13_slot (k : Fin 10) (t0 : ℝ)
233 (aN bN cN aP bP cP aQ bQ cQ aD bD cD : ℝ)
234 (hpath : ∀ t : ℝ,
235 apexDotNum (t13CoordPath k t) = aN * t ^ 2 + bN * t + cN
236 ∧ apex3NormSqNum (t13CoordPath k t) = aP * t ^ 2 + bP * t + cP
237 ∧ apex4NormSqNum (t13CoordPath k t) = aQ * t ^ 2 + bQ * t + cQ
238 ∧ hingeGramDet (t13CoordPath k t) = aD * t ^ 2 + bD * t + cD)
239 (hN0 : aN * t0 ^ 2 + bN * t0 + cN = 8)
240 (hP0 : aP * t0 ^ 2 + bP * t0 + cP = 8)
241 (hQ0 : aQ * t0 ^ 2 + bQ * t0 + cQ = 8)
242 (hD0 : 0 < aD * t0 ^ 2 + bD * t0 + cD) :
243 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath k t))
244 ((2 * (2 * aN * t0 + bN) - (2 * aP * t0 + bP)
245 - (2 * aQ * t0 + bQ)) / 32) t0 := by
246 have hN := hasDerivAt_quadPoly aN bN cN t0
247 have hP := hasDerivAt_quadPoly aP bP cP t0
248 have hQ := hasDerivAt_quadPoly aQ bQ cQ t0
249 have hmain := hasDerivAt_numForm_t13 hN hP hQ hN0 hP0 hQ0
250 refine hmain.congr_of_eventuallyEq ?_
251 have hDcont : Continuous fun t : ℝ => aD * t ^ 2 + bD * t + cD := by
252 continuity
253 have hDev : ∀ᶠ t in nhds t0, 0 < aD * t ^ 2 + bD * t + cD :=
254 (hDcont.tendsto t0).eventually (eventually_gt_nhds hD0)
255 filter_upwards [hDev] with t ht
256 have hp := hpath t
257 rw [cos_numForm (t13CoordPath k t) (by rw [hp.2.2.2]; exact ht),
258 hp.1, hp.2.1, hp.2.2.1]
259
260private lemma t13_path0_polys : ∀ t : ℝ,
261 apexDotNum (t13CoordPath 0 t) = (-2) * t ^ 2 + (12) * t + (-2)
262 ∧ apex3NormSqNum (t13CoordPath 0 t) = (-2) * t ^ 2 + (12) * t + (-2)
263 ∧ apex4NormSqNum (t13CoordPath 0 t) = (-1) * t ^ 2 + (10) * t + (-1)
264 ∧ hingeGramDet (t13CoordPath 0 t) = (-1) * t ^ 2 + (14) * t + (-1) := by
265 intro t
266 refine ⟨?_, ?_, ?_, ?_⟩ <;>
267 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
268 t13CoordPath, t13FlatSqEdges] <;> ring
269
270private lemma t13_path1_polys : ∀ t : ℝ,
271 apexDotNum (t13CoordPath 1 t) = (-2) * t ^ 2 + (16) * t + (-24)
272 ∧ apex3NormSqNum (t13CoordPath 1 t) = (-1) * t ^ 2 + (8) * t + (-8)
273 ∧ apex4NormSqNum (t13CoordPath 1 t) = (-2) * t ^ 2 + (16) * t + (-24)
274 ∧ hingeGramDet (t13CoordPath 1 t) = (-1) * t ^ 2 + (8) * t + (-4) := by
275 intro t
276 refine ⟨?_, ?_, ?_, ?_⟩ <;>
277 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
278 t13CoordPath, t13FlatSqEdges] <;> ring
279
280private lemma t13_path2_polys : ∀ t : ℝ,
281 apexDotNum (t13CoordPath 2 t) = (0) * t ^ 2 + (0) * t + (8)
282 ∧ apex3NormSqNum (t13CoordPath 2 t) = (-3) * t ^ 2 + (12) * t + (-4)
283 ∧ apex4NormSqNum (t13CoordPath 2 t) = (0) * t ^ 2 + (0) * t + (8)
284 ∧ hingeGramDet (t13CoordPath 2 t) = (0) * t ^ 2 + (0) * t + (12) := by
285 intro t
286 refine ⟨?_, ?_, ?_, ?_⟩ <;>
287 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
288 t13CoordPath, t13FlatSqEdges] <;> ring
289
290private lemma t13_path3_polys : ∀ t : ℝ,
291 apexDotNum (t13CoordPath 3 t) = (0) * t ^ 2 + (0) * t + (8)
292 ∧ apex3NormSqNum (t13CoordPath 3 t) = (0) * t ^ 2 + (0) * t + (8)
293 ∧ apex4NormSqNum (t13CoordPath 3 t) = (-3) * t ^ 2 + (18) * t + (-19)
294 ∧ hingeGramDet (t13CoordPath 3 t) = (0) * t ^ 2 + (0) * t + (12) := by
295 intro t
296 refine ⟨?_, ?_, ?_, ?_⟩ <;>
297 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
298 t13CoordPath, t13FlatSqEdges] <;> ring
299
300private lemma t13_path4_polys : ∀ t : ℝ,
301 apexDotNum (t13CoordPath 4 t) = (-4) * t ^ 2 + (20) * t + (-16)
302 ∧ apex3NormSqNum (t13CoordPath 4 t) = (-2) * t ^ 2 + (12) * t + (-10)
303 ∧ apex4NormSqNum (t13CoordPath 4 t) = (-3) * t ^ 2 + (18) * t + (-19)
304 ∧ hingeGramDet (t13CoordPath 4 t) = (-1) * t ^ 2 + (10) * t + (-9) := by
305 intro t
306 refine ⟨?_, ?_, ?_, ?_⟩ <;>
307 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
308 t13CoordPath, t13FlatSqEdges] <;> ring
309
310private lemma t13_path5_polys : ∀ t : ℝ,
311 apexDotNum (t13CoordPath 5 t) = (0) * t ^ 2 + (4) * t + (4)
312 ∧ apex3NormSqNum (t13CoordPath 5 t) = (-4) * t ^ 2 + (16) * t + (-4)
313 ∧ apex4NormSqNum (t13CoordPath 5 t) = (0) * t ^ 2 + (0) * t + (8)
314 ∧ hingeGramDet (t13CoordPath 5 t) = (0) * t ^ 2 + (0) * t + (12) := by
315 intro t
316 refine ⟨?_, ?_, ?_, ?_⟩ <;>
317 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
318 t13CoordPath, t13FlatSqEdges] <;> ring
319
320private lemma t13_path6_polys : ∀ t : ℝ,
321 apexDotNum (t13CoordPath 6 t) = (0) * t ^ 2 + (8) * t + (-8)
322 ∧ apex3NormSqNum (t13CoordPath 6 t) = (0) * t ^ 2 + (0) * t + (8)
323 ∧ apex4NormSqNum (t13CoordPath 6 t) = (-4) * t ^ 2 + (20) * t + (-16)
324 ∧ hingeGramDet (t13CoordPath 6 t) = (0) * t ^ 2 + (0) * t + (12) := by
325 intro t
326 refine ⟨?_, ?_, ?_, ?_⟩ <;>
327 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
328 t13CoordPath, t13FlatSqEdges] <;> ring
329
330private lemma t13_path7_polys : ∀ t : ℝ,
331 apexDotNum (t13CoordPath 7 t) = (0) * t ^ 2 + (8) * t + (-8)
332 ∧ apex3NormSqNum (t13CoordPath 7 t) = (-1) * t ^ 2 + (8) * t + (-4)
333 ∧ apex4NormSqNum (t13CoordPath 7 t) = (0) * t ^ 2 + (0) * t + (8)
334 ∧ hingeGramDet (t13CoordPath 7 t) = (0) * t ^ 2 + (0) * t + (12) := by
335 intro t
336 refine ⟨?_, ?_, ?_, ?_⟩ <;>
337 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
338 t13CoordPath, t13FlatSqEdges] <;> ring
339
340private lemma t13_path8_polys : ∀ t : ℝ,
341 apexDotNum (t13CoordPath 8 t) = (0) * t ^ 2 + (4) * t + (4)
342 ∧ apex3NormSqNum (t13CoordPath 8 t) = (0) * t ^ 2 + (0) * t + (8)
343 ∧ apex4NormSqNum (t13CoordPath 8 t) = (-1) * t ^ 2 + (10) * t + (-1)
344 ∧ hingeGramDet (t13CoordPath 8 t) = (0) * t ^ 2 + (0) * t + (12) := by
345 intro t
346 refine ⟨?_, ?_, ?_, ?_⟩ <;>
347 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
348 t13CoordPath, t13FlatSqEdges] <;> ring
349
350private lemma t13_path9_polys : ∀ t : ℝ,
351 apexDotNum (t13CoordPath 9 t) = (0) * t ^ 2 + (-12) * t + (20)
352 ∧ apex3NormSqNum (t13CoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8)
353 ∧ apex4NormSqNum (t13CoordPath 9 t) = (0) * t ^ 2 + (0) * t + (8)
354 ∧ hingeGramDet (t13CoordPath 9 t) = (0) * t ^ 2 + (0) * t + (12) := by
355 intro t
356 refine ⟨?_, ?_, ?_, ?_⟩ <;>
357 simp [apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet,
358 t13CoordPath, t13FlatSqEdges] <;> ring
359
360theorem hasDerivAt_t13_slot0 :
361 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 0 t)) 0 1 := by
362 have h := hasDerivAt_t13_slot 0 1 (-2) (12) (-2) (-2) (12) (-2)
363 (-1) (10) (-1) (-1) (14) (-1) t13_path0_polys
364 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
365 convert h using 1
366 ring
367
368theorem hasDerivAt_t13_slot1 :
369 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 1 t)) 0 4 := by
370 have h := hasDerivAt_t13_slot 1 4 (-2) (16) (-24) (-1) (8) (-8)
371 (-2) (16) (-24) (-1) (8) (-4) t13_path1_polys
372 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
373 convert h using 1
374 ring
375
376theorem hasDerivAt_t13_slot2 :
377 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 2 t)) 0 2 := by
378 have h := hasDerivAt_t13_slot 2 2 (0) (0) (8) (-3) (12) (-4)
379 (0) (0) (8) (0) (0) (12) t13_path2_polys
380 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
381 convert h using 1
382 ring
383
384theorem hasDerivAt_t13_slot3 :
385 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 3 t)) 0 3 := by
386 have h := hasDerivAt_t13_slot 3 3 (0) (0) (8) (0) (0) (8)
387 (-3) (18) (-19) (0) (0) (12) t13_path3_polys
388 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
389 convert h using 1
390 ring
391
392theorem hasDerivAt_t13_slot4 :
393 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 4 t))
394 ((-1 / 4 : ℝ)) 3 := by
395 have h := hasDerivAt_t13_slot 4 3 (-4) (20) (-16) (-2) (12) (-10)
396 (-3) (18) (-19) (-1) (10) (-9) t13_path4_polys
397 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
398 convert h using 1
399 ring
400
401theorem hasDerivAt_t13_slot5 :
402 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 5 t)) 0 1 := by
403 have h := hasDerivAt_t13_slot 5 1 (0) (4) (4) (-4) (16) (-4)
404 (0) (0) (8) (0) (0) (12) t13_path5_polys
405 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
406 convert h using 1
407 ring
408
409theorem hasDerivAt_t13_slot6 :
410 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 6 t))
411 ((3 / 8 : ℝ)) 2 := by
412 have h := hasDerivAt_t13_slot 6 2 (0) (8) (-8) (0) (0) (8)
413 (-4) (20) (-16) (0) (0) (12) t13_path6_polys
414 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
415 convert h using 1
416 ring
417
418theorem hasDerivAt_t13_slot7 :
419 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 7 t))
420 ((3 / 8 : ℝ)) 2 := by
421 have h := hasDerivAt_t13_slot 7 2 (0) (8) (-8) (-1) (8) (-4)
422 (0) (0) (8) (0) (0) (12) t13_path7_polys
423 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
424 convert h using 1
425 ring
426
427theorem hasDerivAt_t13_slot8 :
428 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 8 t)) 0 1 := by
429 have h := hasDerivAt_t13_slot 8 1 (0) (4) (4) (0) (0) (8)
430 (-1) (10) (-1) (0) (0) (12) t13_path8_polys
431 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
432 convert h using 1
433 ring
434
435theorem hasDerivAt_t13_slot9 :
436 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath 9 t))
437 ((-3 / 4 : ℝ)) 1 := by
438 have h := hasDerivAt_t13_slot 9 1 (0) (-12) (20) (0) (0) (8)
439 (0) (0) (8) (0) (0) (12) t13_path9_polys
440 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
441 convert h using 1
442 ring
443
444theorem hasDerivAt_t13_coord (k : Fin 10) :
445 HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath k t))
446 (t13CosKernel k) (t13FlatSqEdges k) := by
447 fin_cases k
448 · exact hasDerivAt_t13_slot0
449 · exact hasDerivAt_t13_slot1
450 · exact hasDerivAt_t13_slot2
451 · exact hasDerivAt_t13_slot3
452 · exact hasDerivAt_t13_slot4
453 · exact hasDerivAt_t13_slot5
454 · exact hasDerivAt_t13_slot6
455 · exact hasDerivAt_t13_slot7
456 · exact hasDerivAt_t13_slot8
457 · exact hasDerivAt_t13_slot9
458
459/-! ## §5. Deficit kernels and class assembly -/
460
461/-- Chain factor `-1/sin` at flat cosine `1/2` (`sin = √3/2`). -/
462def chainT13 : ℝ := - (2 / Real.sqrt 3)
463
464theorem chainT13_eq : chainT13 = - (2 * Real.sqrt 3 / 3) := by
465 have hs : Real.sqrt 3 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
466 simp only [chainT13]
467 field_simp [hs]
468 rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
469
470def t13DeficitKernel : Fin 10 → ℝ
471 | ⟨4, _⟩ => - (Real.sqrt 3) / 6
472 | ⟨6, _⟩ => Real.sqrt 3 / 4
473 | ⟨7, _⟩ => Real.sqrt 3 / 4
474 | ⟨9, _⟩ => - (Real.sqrt 3) / 2
475 | _ => 0
476
477theorem t13DeficitKernel_eq_chain (k : Fin 10) :
478 t13DeficitKernel k = -chainT13 * t13CosKernel k := by
479 have hs : Real.sqrt 3 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
480 have hs3 : Real.sqrt 3 ^ 2 = (3 : ℝ) :=
481 Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)
482 fin_cases k <;>
483 (simp only [t13DeficitKernel, chainT13, t13CosKernel]
484 try field_simp [hs]
485 try simp [hs3]
486 try ring)
487
488/-- Local-slot → 15-class map for each of the six star members, after
489reordering vertices so the hinge is `(0,1,15)` and apexes follow the
490Freudenthal chain. -/
491def starSlotClass : Fin 6 → Fin 10 → Fin 15
492 | 0, 0 => 0 | 0, 1 => 14 | 0, 2 => 2 | 0, 3 => 6 | 0, 4 => 13
493 | 0, 5 => 1 | 0, 6 => 5 | 0, 7 => 11 | 0, 8 => 7 | 0, 9 => 3
494 | 1, 0 => 0 | 1, 1 => 14 | 1, 2 => 2 | 1, 3 => 10 | 1, 4 => 13
495 | 1, 5 => 1 | 1, 6 => 9 | 1, 7 => 11 | 1, 8 => 3 | 1, 9 => 7
496 | 2, 0 => 0 | 2, 1 => 14 | 2, 2 => 4 | 2, 3 => 6 | 2, 4 => 13
497 | 2, 5 => 3 | 2, 6 => 5 | 2, 7 => 9 | 2, 8 => 7 | 2, 9 => 1
498 | 3, 0 => 0 | 3, 1 => 14 | 3, 2 => 4 | 3, 3 => 12 | 3, 4 => 13
499 | 3, 5 => 3 | 3, 6 => 11 | 3, 7 => 9 | 3, 8 => 1 | 3, 9 => 7
500 | 4, 0 => 0 | 4, 1 => 14 | 4, 2 => 8 | 4, 3 => 10 | 4, 4 => 13
501 | 4, 5 => 7 | 4, 6 => 9 | 4, 7 => 5 | 4, 8 => 3 | 4, 9 => 1
502 | 5, 0 => 0 | 5, 1 => 14 | 5, 2 => 8 | 5, 3 => 12 | 5, 4 => 13
503 | 5, 5 => 7 | 5, 6 => 11 | 5, 7 => 5 | 5, 8 => 1 | 5, 9 => 3
504
505def assembleStarMember (m : Fin 6) : Fin 15 → ℝ :=
506 fun d => ∑ e : Fin 10,
507 if starSlotClass m e = d then t13DeficitKernel e else 0
508
509def fullStarClassKernelAssembled : Fin 15 → ℝ :=
510 fun d => ∑ m : Fin 6, assembleStarMember m d
511
512def fullStarClassKernel : Fin 15 → ℝ
513 | ⟨1, _⟩ => - Real.sqrt 3
514 | ⟨3, _⟩ => - Real.sqrt 3
515 | ⟨5, _⟩ => Real.sqrt 3
516 | ⟨7, _⟩ => - Real.sqrt 3
517 | ⟨9, _⟩ => Real.sqrt 3
518 | ⟨11, _⟩ => Real.sqrt 3
519 | ⟨13, _⟩ => - Real.sqrt 3
520 | _ => 0
521
522private lemma sum_support4_4679 (f : Fin 10 → ℝ)
523 (hz : ∀ e : Fin 10, e ≠ 4 → e ≠ 6 → e ≠ 7 → e ≠ 9 → f e = 0) :
524 (∑ e : Fin 10, f e) = f 4 + f 6 + f 7 + f 9 := by
525 rw [show (Finset.univ : Finset (Fin 10)) =
526 insert (4 : Fin 10) (insert (6 : Fin 10)
527 (insert (7 : Fin 10) (insert (9 : Fin 10)
528 ({0, 1, 2, 3, 5, 8} : Finset (Fin 10))))) from by decide]
529 rw [Finset.sum_insert (by decide), Finset.sum_insert (by decide),
530 Finset.sum_insert (by decide), Finset.sum_insert (by decide),
531 Finset.sum_eq_zero (fun e he => by
532 fin_cases e <;> simp at he ⊢ <;>
533 exact hz _ (by decide) (by decide) (by decide) (by decide))]
534 abel
535
536private lemma deficit_zero_off (e : Fin 10)
537 (h4 : e ≠ 4) (h6 : e ≠ 6) (h7 : e ≠ 7) (h9 : e ≠ 9) :
538 t13DeficitKernel e = 0 := by
539 fin_cases e <;> first | rfl | contradiction
540
541private lemma member_eval (m : Fin 6) (d : Fin 15) :
542 assembleStarMember m d =
543 (if starSlotClass m 4 = d then t13DeficitKernel 4 else 0) +
544 (if starSlotClass m 6 = d then t13DeficitKernel 6 else 0) +
545 (if starSlotClass m 7 = d then t13DeficitKernel 7 else 0) +
546 (if starSlotClass m 9 = d then t13DeficitKernel 9 else 0) := by
547 simp only [assembleStarMember]
548 exact sum_support4_4679 (fun e =>
549 if starSlotClass m e = d then t13DeficitKernel e else 0)
550 (fun e h4 h6 h7 h9 => by simp [deficit_zero_off e h4 h6 h7 h9])
551
552private lemma sum6 (f : Fin 6 → ℝ) :
553 (∑ m : Fin 6, f m) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 := by
554 rw [show (Finset.univ : Finset (Fin 6)) =
555 insert (0 : Fin 6) (insert (1 : Fin 6) (insert (2 : Fin 6)
556 (insert (3 : Fin 6) (insert (4 : Fin 6) (insert (5 : Fin 6)
557 (∅ : Finset (Fin 6))))))) from by decide]
558 simp [Finset.sum_insert]
559 ring
560
561private lemma member0_closed (d : Fin 15) :
562 assembleStarMember 0 d =
563 (if d = 13 then - (Real.sqrt 3) / 6 else 0) +
564 (if d = 5 then Real.sqrt 3 / 4 else 0) +
565 (if d = 11 then Real.sqrt 3 / 4 else 0) +
566 (if d = 3 then - (Real.sqrt 3) / 2 else 0) := by
567 rw [member_eval]
568 simp only [starSlotClass, t13DeficitKernel]
569 aesop
570
571private lemma member1_closed (d : Fin 15) :
572 assembleStarMember 1 d =
573 (if d = 13 then - (Real.sqrt 3) / 6 else 0) +
574 (if d = 9 then Real.sqrt 3 / 4 else 0) +
575 (if d = 11 then Real.sqrt 3 / 4 else 0) +
576 (if d = 7 then - (Real.sqrt 3) / 2 else 0) := by
577 rw [member_eval]
578 simp only [starSlotClass, t13DeficitKernel]
579 aesop
580
581private lemma member2_closed (d : Fin 15) :
582 assembleStarMember 2 d =
583 (if d = 13 then - (Real.sqrt 3) / 6 else 0) +
584 (if d = 5 then Real.sqrt 3 / 4 else 0) +
585 (if d = 9 then Real.sqrt 3 / 4 else 0) +
586 (if d = 1 then - (Real.sqrt 3) / 2 else 0) := by
587 rw [member_eval]
588 simp only [starSlotClass, t13DeficitKernel]
589 aesop
590
591private lemma member3_closed (d : Fin 15) :
592 assembleStarMember 3 d =
593 (if d = 13 then - (Real.sqrt 3) / 6 else 0) +
594 (if d = 11 then Real.sqrt 3 / 4 else 0) +
595 (if d = 9 then Real.sqrt 3 / 4 else 0) +
596 (if d = 7 then - (Real.sqrt 3) / 2 else 0) := by
597 rw [member_eval]
598 simp only [starSlotClass, t13DeficitKernel]
599 aesop
600
601private lemma member4_closed (d : Fin 15) :
602 assembleStarMember 4 d =
603 (if d = 13 then - (Real.sqrt 3) / 6 else 0) +
604 (if d = 9 then Real.sqrt 3 / 4 else 0) +
605 (if d = 5 then Real.sqrt 3 / 4 else 0) +
606 (if d = 1 then - (Real.sqrt 3) / 2 else 0) := by
607 rw [member_eval]
608 simp only [starSlotClass, t13DeficitKernel]
609 aesop
610
611private lemma member5_closed (d : Fin 15) :
612 assembleStarMember 5 d =
613 (if d = 13 then - (Real.sqrt 3) / 6 else 0) +
614 (if d = 11 then Real.sqrt 3 / 4 else 0) +
615 (if d = 5 then Real.sqrt 3 / 4 else 0) +
616 (if d = 3 then - (Real.sqrt 3) / 2 else 0) := by
617 rw [member_eval]
618 simp only [starSlotClass, t13DeficitKernel]
619 aesop
620
621theorem fullStarClassKernel_eq (d : Fin 15) :
622 fullStarClassKernelAssembled d = fullStarClassKernel d := by
623 simp only [fullStarClassKernelAssembled]
624 rw [sum6, member0_closed, member1_closed, member2_closed,
625 member3_closed, member4_closed, member5_closed]
626 fin_cases d <;> simp [fullStarClassKernel] <;> ring
627
628
629theorem fullStarClassKernel_values :
630 fullStarClassKernel 1 = - Real.sqrt 3 ∧
631 fullStarClassKernel 3 = - Real.sqrt 3 ∧
632 fullStarClassKernel 5 = Real.sqrt 3 ∧
633 fullStarClassKernel 7 = - Real.sqrt 3 ∧
634 fullStarClassKernel 9 = Real.sqrt 3 ∧
635 fullStarClassKernel 11 = Real.sqrt 3 ∧
636 fullStarClassKernel 13 = - Real.sqrt 3 :=
637 ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
638
639theorem fullStarClassKernel_zero_off (d : Fin 15)
640 (h1 : d ≠ 1) (h3 : d ≠ 3) (h5 : d ≠ 5) (h7 : d ≠ 7)
641 (h9 : d ≠ 9) (h11 : d ≠ 11) (h13 : d ≠ 13) :
642 fullStarClassKernel d = 0 := by
643 fin_cases d <;> first | rfl | contradiction
644
645/-! ## §6. Gates -/
646
647theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 5 ≠ 0 := by
648 change Real.sqrt 3 ≠ 0
649 exact Real.sqrt_ne_zero'.mpr (by norm_num : (0 : ℝ) < 3)
650
651/-- Axis swap `1 ↔ 2` (bits 1 and 2); an S₃ generator fixing the hinge
652vertex set `{0,1,15}`. -/
653def swap12Mask (m : ℕ) : ℕ :=
654 (if Nat.testBit m 0 then 1 else 0) +
655 (if Nat.testBit m 1 then 4 else 0) +
656 (if Nat.testBit m 2 then 2 else 0) +
657 (if Nat.testBit m 3 then 8 else 0)
658
659theorem swap12Mask_bounds (d : Fin 15) :
660 0 < swap12Mask (maskOf d) ∧ swap12Mask (maskOf d) ≤ 15 := by
661 fin_cases d <;> decide
662
663def swap12Class (d : Fin 15) : Fin 15 :=
664 ⟨swap12Mask (maskOf d) - 1, by
665 have h := swap12Mask_bounds d
666 omega⟩
667
668/-- Explicit table for `swap12Class` (kernel-decidable). -/
669def swap12ClassTable : Fin 15 → Fin 15
670 | 0 => 0 | 1 => 3 | 2 => 4 | 3 => 1 | 4 => 2
671 | 5 => 5 | 6 => 6 | 7 => 7 | 8 => 8 | 9 => 11
672 | 10 => 12 | 11 => 9 | 12 => 10 | 13 => 13 | 14 => 14
673
674theorem swap12Class_eq_table (d : Fin 15) :
675 swap12Class d = swap12ClassTable d := by
676 fin_cases d <;> decide
677
678theorem fullStarClassKernel_swap12 (d : Fin 15) :
679 fullStarClassKernel (swap12Class d) = fullStarClassKernel d := by
680 rw [swap12Class_eq_table]
681 fin_cases d <;> simp [fullStarClassKernel, swap12ClassTable]
682
683def fullStarDirectional (v : Fin 15 → ℝ) : ℝ :=
684 ∑ d : Fin 15, v d * fullStarClassKernel d
685
686private lemma sum15_support (f : Fin 15 → ℝ)
687 (hz : ∀ d : Fin 15, d ≠ 1 → d ≠ 3 → d ≠ 5 → d ≠ 7 → d ≠ 9 → d ≠ 11 →
688 d ≠ 13 → f d = 0) :
689 (∑ d : Fin 15, f d) =
690 f 1 + f 3 + f 5 + f 7 + f 9 + f 11 + f 13 := by
691 classical
692 have hrest :
693 ∑ d ∈ ({0, 2, 4, 6, 8, 10, 12, 14} : Finset (Fin 15)), f d = 0 := by
694 refine Finset.sum_eq_zero ?_
695 intro d hd
696 have : d = 0 ∨ d = 2 ∨ d = 4 ∨ d = 6 ∨ d = 8 ∨ d = 10 ∨ d = 12 ∨
697 d = 14 := by
698 fin_cases d <;> simp at hd ⊢
699 rcases this with (rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl) <;>
700 exact hz _ (by decide) (by decide) (by decide) (by decide)
701 (by decide) (by decide) (by decide)
702 rw [show (Finset.univ : Finset (Fin 15)) =
703 insert (1 : Fin 15) (insert (3 : Fin 15) (insert (5 : Fin 15)
704 (insert (7 : Fin 15) (insert (9 : Fin 15) (insert (11 : Fin 15)
705 (insert (13 : Fin 15)
706 ({0, 2, 4, 6, 8, 10, 12, 14} : Finset (Fin 15))))))))
707 from by decide]
708 simp [Finset.sum_insert, hrest]
709 ring
710
711theorem fullStar_uniformScale_decoy :
712 fullStarDirectional (fun _ => (1 : ℝ)) = - Real.sqrt 3 := by
713 simp only [fullStarDirectional]
714 rw [sum15_support _ (fun d h1 h3 h5 h7 h9 h11 h13 => by
715 rw [fullStarClassKernel_zero_off d h1 h3 h5 h7 h9 h11 h13, mul_zero])]
716 simp [fullStarClassKernel]
717
718theorem fullStar_homothety_stationary :
719 fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
720 simp only [fullStarDirectional]
721 rw [sum15_support _ (fun d h1 h3 h5 h7 h9 h11 h13 => by
722 rw [fullStarClassKernel_zero_off d h1 h3 h5 h7 h9 h11 h13, mul_zero])]
723 have w1 : classWeightNat 1 = 1 := by decide
724 have w3 : classWeightNat 3 = 1 := by decide
725 have w5 : classWeightNat 5 = 2 := by decide
726 have w7 : classWeightNat 7 = 1 := by decide
727 have w9 : classWeightNat 9 = 2 := by decide
728 have w11 : classWeightNat 11 = 2 := by decide
729 have w13 : classWeightNat 13 = 3 := by decide
730 simp [fullStarClassKernel, w1, w3, w5, w7, w9, w11, w13]
731 ring
732
733/-! ## §7. Status -/
734
735structure Hinge4DStarKernel13Status where
736 starEnumerationClosed : Bool
737 flatnessGateClosed : Bool
738 fullStarClassKernelClosed : Bool
739 type31TransportOpen : Bool
740 flatHessianAssemblyOpen : Bool
741 convergesEH4d : Bool
742 gapActionRecovery : Bool
743
744def hinge4DStarKernel13Status : Hinge4DStarKernel13Status where
745 starEnumerationClosed := true
746 flatnessGateClosed := true
747 fullStarClassKernelClosed := true
748 type31TransportOpen := true
749 flatHessianAssemblyOpen := true
750 convergesEH4d := false
751 gapActionRecovery := false
752
753theorem hinge4DStarKernel13Status_flags :
754 hinge4DStarKernel13Status.starEnumerationClosed = true ∧
755 hinge4DStarKernel13Status.flatnessGateClosed = true ∧
756 hinge4DStarKernel13Status.fullStarClassKernelClosed = true ∧
757 hinge4DStarKernel13Status.type31TransportOpen = true ∧
758 hinge4DStarKernel13Status.flatHessianAssemblyOpen = true ∧
759 hinge4DStarKernel13Status.convergesEH4d = false ∧
760 hinge4DStarKernel13Status.gapActionRecovery = false := by
761 decide
762
763/-! ## §8. Axiom audit (embedded; shared `.lake` symlink emits no olean) -/
764
765#print axioms cubeContainsHinge_origin
766#print axioms star_cube_cardinality
767#print axioms only_origin_contains_hinge
768#print axioms starMembers_length
769#print axioms starMembers_complete
770#print axioms star_cardinality
771#print axioms cosDihedral_t13_flat
772#print axioms arccos_one_half
773#print axioms star_flat_angle_sum_two_pi
774#print axioms starFlatCosines_match
775#print axioms hasDerivAt_t13_coord
776#print axioms chainT13_eq
777#print axioms t13DeficitKernel_eq_chain
778#print axioms swap12Class_eq_table
779#print axioms fullStarClassKernel_eq
780#print axioms fullStarClassKernel_values
781#print axioms fullStarClassKernel_zero_off
782#print axioms fullStarClassKernel_nonvacuous
783#print axioms fullStarClassKernel_swap12
784#print axioms fullStar_uniformScale_decoy
785#print axioms fullStar_homothety_stationary
786#print axioms hinge4DStarKernel13Status_flags
787
788end
789
790end ReggeHinge4DStarKernel13
791end Analysis
792end Gravity
793end IndisputableMonolith
794