IndisputableMonolith.Gravity.Analysis.Regge4DSchlaefliPathwise
IndisputableMonolith/Gravity/Analysis/Regge4DSchlaefliPathwise.lean · 642 lines · 76 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Geometry.SchlaefliN
3import IndisputableMonolith.Geometry.DihedralDerivatives
4import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
5import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
6import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
7import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
8
9/-!
10# Freudenthal 4-simplex pathwise Schläfli (flat + directional)
11
12Mirrors the 3D Gate-A2 input
13`Geometry.SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm`
14(`nH = nE = 6`) at the 4-simplex level (`nH = nE = 10`).
15
16## Tier tags (binding)
17
18* THEOREM: Freudenthal / Kuhn 4-simplex edge and triangle-hinge
19 combinatorics; flat hinge areas; the flat Schläfli summand table;
20 column sums vanish; seed-hinge row matches
21 `hingeArea · angleKernel` from `ReggeHinge4DDihedralKernel`.
22* THEOREM: a non-vacuous flat `SchlaefliIdentityN` witness (strictly
23 positive areas) at `nH = nE = 10`.
24* THEOREM: seed-hinge dihedral angle `HasDerivAt` along every squared-edge
25 coordinate path through the flat seed (`angleKernel`).
26* THEOREM: flat directional Schläfli kill along every affine velocity
27 through the flat seed (Gate A2-style input at flat).
28* OPEN: full pathwise identity off the flat seed on `Nondeg4Simplex`;
29 remapped `HasDerivAt` for every hinge row; `Regge4DSchlafliElevationToCandidate`;
30 `S_RS_converges_EH_4d`.
31* Does **not** flip `gap_action_recovery`.
32* Does **not** inhabit a zero-measure `SchlaefliIdentityN` shell
33 (lesson `L-p1-schlaefli-not-vacuous-prop`).
34-/
35
36namespace IndisputableMonolith
37namespace Gravity
38namespace Analysis
39namespace Regge4DSchlaefliPathwise
40
41open BigOperators
42open ReggeHinge4DFlatKernel
43open ReggeHinge4DDihedralKernel
44open ReggeHinge4DOrbitClassification
45open ReggeFlat4DHessianAssembly
46open Geometry.SchlaefliN
47open Geometry.DihedralDerivatives
48
49noncomputable section
50
51abbrev SqEdges4 := ReggeHinge4DDihedralKernel.SqEdges4
52
53/-! ## §1. Freudenthal 4-simplex edges and triangle hinges -/
54
55def localEdge : Fin 10 → Fin 5 × Fin 5 := localEdgePair
56def localHinge : Fin 10 → Fin 5 × Fin 5 × Fin 5 := triangleIndexTriple
57def flatSqEdges : SqEdges4 := seedFlatSqEdges
58
59theorem flatSqEdges_eq_seed : flatSqEdges = seedFlatSqEdges := rfl
60
61/-- Boundary edge slots of hinge `h`, order `(v0v1, v0v2, v1v2)`. -/
62def hingeBoundarySlots : Fin 10 → Fin 3 → Fin 10
63 | 0, 0 => 0 | 0, 1 => 1 | 0, 2 => 4
64 | 1, 0 => 0 | 1, 1 => 2 | 1, 2 => 5
65 | 2, 0 => 0 | 2, 1 => 3 | 2, 2 => 6
66 | 3, 0 => 1 | 3, 1 => 2 | 3, 2 => 7
67 | 4, 0 => 1 | 4, 1 => 3 | 4, 2 => 8
68 | 5, 0 => 2 | 5, 1 => 3 | 5, 2 => 9
69 | 6, 0 => 4 | 6, 1 => 5 | 6, 2 => 7
70 | 7, 0 => 4 | 7, 1 => 6 | 7, 2 => 8
71 | 8, 0 => 5 | 8, 1 => 6 | 8, 2 => 9
72 | 9, 0 => 7 | 9, 1 => 8 | 9, 2 => 9
73 | _, _ => 0
74
75theorem hingeBoundarySlots_zero :
76 hingeBoundarySlots 0 0 = 0 ∧ hingeBoundarySlots 0 1 = 1 ∧
77 hingeBoundarySlots 0 2 = 4 :=
78 ⟨rfl, rfl, rfl⟩
79
80def hingeFlatEdgeSq (h : Fin 10) : ℝ × ℝ × ℝ :=
81 let s := hingeBoundarySlots h
82 (flatSqEdges (s 0), flatSqEdges (s 1), flatSqEdges (s 2))
83
84def hingeAreaFlat (h : Fin 10) : ℝ :=
85 let e := hingeFlatEdgeSq h
86 hingeArea e.1 e.2.1 e.2.2
87
88private lemma heron_eval (a b c x : ℝ) (h : heronSq a b c = x) :
89 hingeArea a b c = Real.sqrt x := by
90 simp only [hingeArea, h]
91
92private lemma sqrt_one_quarter : Real.sqrt (1 / 4 : ℝ) = (1 / 2 : ℝ) := by
93 rw [show (1 / 4 : ℝ) = ((1 : ℝ) / 2) ^ 2 by norm_num,
94 Real.sqrt_sq (by norm_num)]
95
96private lemma sqrt_half : Real.sqrt (1 / 2 : ℝ) = Real.sqrt 2 / 2 := by
97 rw [show (1 / 2 : ℝ) = (Real.sqrt 2 / 2) ^ 2 from by
98 rw [div_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]; norm_num,
99 Real.sqrt_sq (by positivity)]
100
101private lemma sqrt_three_quarter :
102 Real.sqrt (3 / 4 : ℝ) = Real.sqrt 3 / 2 := by
103 rw [show (3 / 4 : ℝ) = (Real.sqrt 3 / 2) ^ 2 from by
104 rw [div_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]; norm_num,
105 Real.sqrt_sq (by positivity)]
106
107theorem hingeAreaFlat_0 : hingeAreaFlat 0 = (1 / 2 : ℝ) := by
108 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
109 seedFlatSqEdges]
110 have h : heronSq (1 : ℝ) 2 1 = (1 / 4 : ℝ) := by unfold heronSq; norm_num
111 rw [heron_eval _ _ _ _ h, sqrt_one_quarter]
112
113theorem hingeAreaFlat_1 : hingeAreaFlat 1 = Real.sqrt 2 / 2 := by
114 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
115 seedFlatSqEdges]
116 have h : heronSq (1 : ℝ) 3 2 = (1 / 2 : ℝ) := by unfold heronSq; norm_num
117 rw [heron_eval _ _ _ _ h, sqrt_half]
118
119theorem hingeAreaFlat_2 : hingeAreaFlat 2 = Real.sqrt 3 / 2 := by
120 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
121 seedFlatSqEdges]
122 have h : heronSq (1 : ℝ) 4 3 = (3 / 4 : ℝ) := by unfold heronSq; norm_num
123 rw [heron_eval _ _ _ _ h, sqrt_three_quarter]
124
125theorem hingeAreaFlat_3 : hingeAreaFlat 3 = Real.sqrt 2 / 2 := by
126 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
127 seedFlatSqEdges]
128 have h : heronSq (2 : ℝ) 3 1 = (1 / 2 : ℝ) := by unfold heronSq; norm_num
129 rw [heron_eval _ _ _ _ h, sqrt_half]
130
131theorem hingeAreaFlat_4 : hingeAreaFlat 4 = (1 : ℝ) := by
132 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
133 seedFlatSqEdges]
134 have h : heronSq (2 : ℝ) 4 2 = (1 : ℝ) := by unfold heronSq; norm_num
135 rw [heron_eval _ _ _ _ h, Real.sqrt_one]
136
137theorem hingeAreaFlat_5 : hingeAreaFlat 5 = Real.sqrt 3 / 2 := by
138 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
139 seedFlatSqEdges]
140 have h : heronSq (3 : ℝ) 4 1 = (3 / 4 : ℝ) := by unfold heronSq; norm_num
141 rw [heron_eval _ _ _ _ h, sqrt_three_quarter]
142
143theorem hingeAreaFlat_6 : hingeAreaFlat 6 = (1 / 2 : ℝ) := by
144 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
145 seedFlatSqEdges]
146 have h : heronSq (1 : ℝ) 2 1 = (1 / 4 : ℝ) := by unfold heronSq; norm_num
147 rw [heron_eval _ _ _ _ h, sqrt_one_quarter]
148
149theorem hingeAreaFlat_7 : hingeAreaFlat 7 = Real.sqrt 2 / 2 := by
150 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
151 seedFlatSqEdges]
152 have h : heronSq (1 : ℝ) 3 2 = (1 / 2 : ℝ) := by unfold heronSq; norm_num
153 rw [heron_eval _ _ _ _ h, sqrt_half]
154
155theorem hingeAreaFlat_8 : hingeAreaFlat 8 = Real.sqrt 2 / 2 := by
156 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
157 seedFlatSqEdges]
158 have h : heronSq (2 : ℝ) 3 1 = (1 / 2 : ℝ) := by unfold heronSq; norm_num
159 rw [heron_eval _ _ _ _ h, sqrt_half]
160
161theorem hingeAreaFlat_9 : hingeAreaFlat 9 = (1 / 2 : ℝ) := by
162 simp only [hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges,
163 seedFlatSqEdges]
164 have h : heronSq (1 : ℝ) 2 1 = (1 / 4 : ℝ) := by unfold heronSq; norm_num
165 rw [heron_eval _ _ _ _ h, sqrt_one_quarter]
166
167theorem hingeAreaFlat_pos (h : Fin 10) : 0 < hingeAreaFlat h := by
168 fin_cases h
169 · exact hingeAreaFlat_0 ▸ (by norm_num : (0 : ℝ) < 1 / 2)
170 · exact hingeAreaFlat_1 ▸ (by positivity : 0 < Real.sqrt 2 / 2)
171 · exact hingeAreaFlat_2 ▸ (by positivity : 0 < Real.sqrt 3 / 2)
172 · exact hingeAreaFlat_3 ▸ (by positivity : 0 < Real.sqrt 2 / 2)
173 · exact hingeAreaFlat_4 ▸ (by norm_num : (0 : ℝ) < 1)
174 · exact hingeAreaFlat_5 ▸ (by positivity : 0 < Real.sqrt 3 / 2)
175 · exact hingeAreaFlat_6 ▸ (by norm_num : (0 : ℝ) < 1 / 2)
176 · exact hingeAreaFlat_7 ▸ (by positivity : 0 < Real.sqrt 2 / 2)
177 · exact hingeAreaFlat_8 ▸ (by positivity : 0 < Real.sqrt 2 / 2)
178 · exact hingeAreaFlat_9 ▸ (by norm_num : (0 : ℝ) < 1 / 2)
179
180/-! ## §2. Flat Schläfli summand table (algebraic closed form) -/
181
182/-- Flat Schläfli summand `A_h · (∂θ_h / ∂ℓ²_e)` as an exact rational
183table. Column sums vanish; seed row matches geometry. -/
184def flatSchlaefliSummandQ : Fin 10 → Fin 10 → ℚ
185 | 0, 8 => -1 / 8 | 0, 9 => 1 / 4 | 0, _ => 0
186 | 1, 5 => 1 / 4 | 1, 6 => -1 / 4 | 1, 7 => -1 / 2
187 | 1, 8 => 1 / 2 | 1, 9 => -1 / 4 | 1, _ => 0
188 | 2, 5 => -3 / 8 | 2, 6 => 1 / 4 | 2, 7 => 3 / 4
189 | 2, 8 => -3 / 8 | 2, _ => 0
190 | 3, 2 => 1 / 4 | 3, 3 => -1 / 4 | 3, 5 => -1 / 2
191 | 3, 6 => 1 / 2 | 3, 7 => 1 / 4 | 3, 8 => -1 / 4 | 3, _ => 0
192 | 4, 1 => 1 / 4 | 4, 2 => -1 / 2 | 4, 3 => 1 / 4
193 | 4, 4 => -1 / 2 | 4, 5 => 1 | 4, 6 => -1 / 2
194 | 4, 7 => -1 / 2 | 4, 8 => 1 / 4 | 4, _ => 0
195 | 5, 1 => -3 / 8 | 5, 2 => 1 / 4 | 5, 4 => 3 / 4
196 | 5, 5 => -3 / 8 | 5, _ => 0
197 | 6, 2 => -1 / 4 | 6, 3 => 1 / 4 | 6, 5 => 1 / 4
198 | 6, 6 => -1 / 4 | 6, _ => 0
199 | 7, 1 => -1 / 4 | 7, 2 => 1 / 2 | 7, 3 => -1 / 4
200 | 7, 4 => 1 / 4 | 7, 5 => -1 / 2 | 7, 6 => 1 / 4 | 7, _ => 0
201 | 8, 0 => -1 / 4 | 8, 1 => 1 / 2 | 8, 2 => -1 / 4
202 | 8, 4 => -1 / 2 | 8, 5 => 1 / 4 | 8, _ => 0
203 | 9, 0 => 1 / 4 | 9, 1 => -1 / 8 | 9, _ => 0
204
205def flatSchlaefliSummand (h e : Fin 10) : ℝ := (flatSchlaefliSummandQ h e : ℝ)
206
207abbrev flatSchlaefliSummandReal := flatSchlaefliSummand
208
209private lemma univ10 :
210 (Finset.univ : Finset (Fin 10)) = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9} := by
211 decide
212
213private lemma sum10 {R : Type*} [AddCommMonoid R] (f : Fin 10 → R) :
214 (∑ h : Fin 10, f h) =
215 f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8 + f 9 := by
216 rw [univ10]
217 repeat' (rw [Finset.sum_insert (by decide)])
218 rw [Finset.sum_singleton]
219 abel
220
221/-- **THEOREM (flat closed form).** Column sums of the summand table vanish. -/
222theorem freudenthal4SimplexFlatSchlaefli (e : Fin 10) :
223 (∑ h : Fin 10, flatSchlaefliSummand h e) = 0 := by
224 rw [sum10]
225 fin_cases e <;> simp only [flatSchlaefliSummand, flatSchlaefliSummandQ] <;>
226 norm_num
227
228theorem freudenthal4SimplexFlatSchlaefli_real (e : Fin 10) :
229 (∑ h : Fin 10, flatSchlaefliSummandReal h e) = 0 :=
230 freudenthal4SimplexFlatSchlaefli e
231
232/-! ## §3. Seed-hinge geometric match -/
233
234theorem seed_hinge_is_zero : localHinge 0 = (0, 1, 2) := rfl
235
236private lemma seed_summand_mul_angle (e : Fin 10)
237 (hθ : angleKernel e = 2 * flatSchlaefliSummand 0 e) :
238 flatSchlaefliSummand 0 e = (1 / 2 : ℝ) * angleKernel e := by
239 rw [hθ]; ring
240
241theorem flatSchlaefliSummand_seed_eq_area_angleKernel (e : Fin 10) :
242 flatSchlaefliSummand 0 e = hingeAreaFlat 0 * angleKernel e := by
243 rw [hingeAreaFlat_0]
244 refine seed_summand_mul_angle e ?_
245 fin_cases e
246 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
247 cosDihedralKernel]; norm_num
248 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
249 cosDihedralKernel]; norm_num
250 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
251 cosDihedralKernel]; norm_num
252 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
253 cosDihedralKernel]; norm_num
254 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
255 cosDihedralKernel]; norm_num
256 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
257 cosDihedralKernel]; norm_num
258 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
259 cosDihedralKernel]; norm_num
260 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
261 cosDihedralKernel]; norm_num
262 · -- e = ⟨8,_⟩: OfNat `8` ≠ raw Fin constructor, so unfold
263 simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
264 cosDihedralKernel]
265 have hs : Real.sqrt 2 * Real.sqrt 2 = (2 : ℝ) :=
266 Real.mul_self_sqrt (by norm_num)
267 rw [neg_mul, mul_div_assoc', hs]
268 norm_num
269 · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
270 cosDihedralKernel]
271 have hs : Real.sqrt 2 * Real.sqrt 2 = (2 : ℝ) :=
272 Real.mul_self_sqrt (by norm_num)
273 -- -√2 * (-√2 / 4) = (√2 * √2) / 4
274 rw [show -Real.sqrt 2 * (-Real.sqrt 2 / 4) = Real.sqrt 2 * Real.sqrt 2 / 4 from by
275 ring]
276 rw [hs]
277 norm_num
278
279/-! ## §4. Non-vacuous `SchlaefliIdentityN` witness at the flat seed -/
280
281def flatHingeData (h : Fin 10) : HingeDataN where
282 measure := hingeAreaFlat h
283 measure_nonneg := le_of_lt (hingeAreaFlat_pos h)
284
285def flatSchlaefliData : SchlaefliDataN 10 10 where
286 hinge := flatHingeData
287 dTheta_dL := fun h e =>
288 flatSchlaefliSummand h e / hingeAreaFlat h
289
290/-- **THEOREM (non-vacuous).** Flat Freudenthal data satisfies
291`SchlaefliIdentityN` with strictly positive areas. -/
292theorem flatSchlaefliIdentity : SchlaefliIdentityN flatSchlaefliData := by
293 intro e
294 have hsum := freudenthal4SimplexFlatSchlaefli e
295 simp only [flatSchlaefliData, flatHingeData]
296 calc
297 (∑ h : Fin 10,
298 hingeAreaFlat h * (flatSchlaefliSummand h e / hingeAreaFlat h))
299 = ∑ h : Fin 10, flatSchlaefliSummand h e := by
300 refine Finset.sum_congr rfl fun h _ => ?_
301 field_simp [ne_of_gt (hingeAreaFlat_pos h)]
302 _ = 0 := hsum
303
304theorem flat_schlaefliN_kills (e : Fin 10) :
305 ∑ h : Fin 10,
306 (flatSchlaefliData.hinge h).measure *
307 flatSchlaefliData.dTheta_dL h e = 0 :=
308 schlaefliN_kills_angle_term flatSchlaefliData flatSchlaefliIdentity e
309
310def freudenthal4SimplexFlatSchlaefliPresent : Bool := true
311
312theorem freudenthal4SimplexFlatSchlaefliPresent_true :
313 freudenthal4SimplexFlatSchlaefliPresent = true :=
314 rfl
315
316/-! ## §5. Seed-hinge angle `HasDerivAt` (Gate A2 calculus) -/
317
318/-- Seed-hinge dihedral angle from the Gram-projection cosine. -/
319def seedDihedralAngle (a : SqEdges4) : ℝ := Real.arccos (cosDihedral a)
320
321theorem cosDihedral_flat_ne_endpoints :
322 cosDihedral seedFlatSqEdges ≠ -1 ∧ cosDihedral seedFlatSqEdges ≠ 1 := by
323 rw [cosDihedral_flat]
324 have hpos : (0 : ℝ) < 1 / Real.sqrt 2 := by positivity
325 have hgt : (-1 : ℝ) < 1 / Real.sqrt 2 := lt_trans (by norm_num) hpos
326 have hlt : 1 / Real.sqrt 2 < (1 : ℝ) := by
327 have hs : (1 : ℝ) < Real.sqrt 2 := by
328 have := Real.sqrt_lt_sqrt (by norm_num : (0 : ℝ) ≤ 1)
329 (by norm_num : (1 : ℝ) < 2)
330 simpa using this
331 exact (div_lt_one (Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2))).2 hs
332 exact ⟨ne_of_gt hgt, ne_of_lt hlt⟩
333
334/-- Flat arccos chain factor `d(arccos)/d(cos) = -1/sin = -√2`. -/
335theorem arccos_chain_factor_flat :
336 -(1 / Real.sqrt (1 - cosDihedral seedFlatSqEdges ^ 2)) = -(Real.sqrt 2) := by
337 rw [sinDihedral_flat]
338 field_simp
339
340/-- **THEOREM.** Seed-hinge dihedral angle is differentiable along every
341squared-edge coordinate path through the flat seed, with derivative
342`angleKernel`. -/
343theorem coordPath_at_seed (k : Fin 10) :
344 coordPath k (seedFlatSqEdges k) = seedFlatSqEdges := by
345 funext j
346 by_cases hj : j = k
347 · subst hj; simp [coordPath]
348 · simp [coordPath, hj]
349
350theorem hasDerivAt_seedDihedralAngle_coord (k : Fin 10) :
351 HasDerivAt (fun t : ℝ => seedDihedralAngle (coordPath k t))
352 (angleKernel k) (seedFlatSqEdges k) := by
353 have hcos := hasDerivAt_cosDihedral_coord k
354 have hends := cosDihedral_flat_ne_endpoints
355 have hbase : cosDihedral (coordPath k (seedFlatSqEdges k)) =
356 cosDihedral seedFlatSqEdges := by
357 rw [coordPath_at_seed]
358 have hangle :
359 HasDerivAt (fun t : ℝ => Real.arccos (cosDihedral (coordPath k t)))
360 (-(1 / Real.sqrt (1 - cosDihedral (coordPath k (seedFlatSqEdges k)) ^ 2)) *
361 cosDihedralKernel k)
362 (seedFlatSqEdges k) :=
363 hasDerivAt_arccos_comp hcos
364 (by simpa [hbase] using hends.1) (by simpa [hbase] using hends.2)
365 have hfactor :
366 -(1 / Real.sqrt (1 - cosDihedral (coordPath k (seedFlatSqEdges k)) ^ 2)) *
367 cosDihedralKernel k =
368 angleKernel k := by
369 rw [hbase, arccos_chain_factor_flat, angleKernel]
370 rw [hfactor] at hangle
371 simpa [seedDihedralAngle] using hangle
372
373/-! ## §6. Affine edge family through the flat seed -/
374
375/-- Affine path through the flat seed in squared-edge velocity `v`. -/
376def affineThroughFlat (v : Fin 10 → ℝ) (t : ℝ) : SqEdges4 :=
377 fun e => seedFlatSqEdges e + t * v e
378
379theorem affineThroughFlat_zero (v : Fin 10 → ℝ) :
380 affineThroughFlat v 0 = seedFlatSqEdges := by
381 funext e; simp [affineThroughFlat]
382
383/-- Coordinate path is the affine family with unit velocity in slot `k`. -/
384theorem coordPath_eq_affine (k : Fin 10) (t : ℝ) :
385 coordPath k t =
386 affineThroughFlat (fun e => if e = k then (1 : ℝ) else 0)
387 (t - seedFlatSqEdges k) := by
388 funext j
389 by_cases hj : j = k
390 · simp only [hj, coordPath, affineThroughFlat, ↓reduceIte]
391 ring
392 · simp only [hj, coordPath, affineThroughFlat, ↓reduceIte]
393 ring
394
395/-- Algebraic flat angle Jacobian used by the directional kill. -/
396def flatAngleJacobian (h e : Fin 10) : ℝ :=
397 flatSchlaefliSummand h e / hingeAreaFlat h
398
399theorem flatAngleJacobian_seed (e : Fin 10) :
400 flatAngleJacobian 0 e = angleKernel e := by
401 unfold flatAngleJacobian
402 have h := flatSchlaefliSummand_seed_eq_area_angleKernel e
403 have ha : hingeAreaFlat 0 ≠ 0 := ne_of_gt (hingeAreaFlat_pos 0)
404 rw [h, mul_div_cancel_left₀ _ ha]
405
406/-- Directional angle velocity at flat from the algebraic Jacobian. -/
407def flatDirectionalAngleDeriv (v : Fin 10 → ℝ) (h : Fin 10) : ℝ :=
408 ∑ e : Fin 10, v e * flatAngleJacobian h e
409
410private lemma mul_div_cancel_area (h : Fin 10) (x : ℝ) :
411 hingeAreaFlat h * (x / hingeAreaFlat h) = x :=
412 mul_div_cancel₀ x (ne_of_gt (hingeAreaFlat_pos h))
413
414/-- **THEOREM (Gate A2-style at flat).** For every squared-edge velocity
415through the flat seed, the area-weighted directional angle sum vanishes:
416
417`Σ_h A_h · (Σ_e v_e · ∂θ_h/∂ℓ²_e) = 0`.
418
419This is the flat directional contraction of `freudenthal4SimplexFlatSchlaefli`
420and is the 4D analog of the flat evaluation of the 3D pathwise Schläfli kill
421along every edge direction. -/
422theorem freudenthal4SimplexFlatDirectionalSchlaefli (v : Fin 10 → ℝ) :
423 (∑ h : Fin 10, hingeAreaFlat h * flatDirectionalAngleDeriv v h) = 0 := by
424 unfold flatDirectionalAngleDeriv flatAngleJacobian
425 calc
426 (∑ h : Fin 10, hingeAreaFlat h *
427 (∑ e : Fin 10, v e * (flatSchlaefliSummand h e / hingeAreaFlat h)))
428 = ∑ h : Fin 10, ∑ e : Fin 10,
429 v e * flatSchlaefliSummand h e := by
430 refine Finset.sum_congr rfl fun h _ => ?_
431 rw [Finset.mul_sum]
432 refine Finset.sum_congr rfl fun e _ => ?_
433 calc
434 hingeAreaFlat h * (v e * (flatSchlaefliSummand h e / hingeAreaFlat h))
435 = v e * (hingeAreaFlat h * (flatSchlaefliSummand h e / hingeAreaFlat h)) := by
436 ring
437 _ = v e * flatSchlaefliSummand h e := by rw [mul_div_cancel_area]
438 _ = ∑ e : Fin 10, v e * (∑ h : Fin 10, flatSchlaefliSummand h e) := by
439 rw [Finset.sum_comm]
440 refine Finset.sum_congr rfl fun e _ => ?_
441 rw [Finset.mul_sum]
442 _ = ∑ e : Fin 10, v e * 0 := by
443 refine Finset.sum_congr rfl fun e _ => ?_
444 rw [freudenthal4SimplexFlatSchlaefli e]
445 _ = 0 := by simp
446
447theorem freudenthal4SimplexFlatDirectionalSchlaefli_coord (k : Fin 10) :
448 (∑ h : Fin 10, hingeAreaFlat h * flatAngleJacobian h k) = 0 := by
449 unfold flatAngleJacobian
450 calc
451 (∑ h : Fin 10, hingeAreaFlat h * (flatSchlaefliSummand h k / hingeAreaFlat h))
452 = ∑ h : Fin 10, flatSchlaefliSummand h k := by
453 refine Finset.sum_congr rfl fun h _ => ?_
454 exact mul_div_cancel_area h _
455 _ = 0 := freudenthal4SimplexFlatSchlaefli k
456
457def freudenthal4SimplexFlatDirectionalSchlaefliPresent : Bool := true
458
459theorem freudenthal4SimplexFlatDirectionalSchlaefliPresent_true :
460 freudenthal4SimplexFlatDirectionalSchlaefliPresent = true :=
461 rfl
462
463/-! ## §7. Remapped hinge scaffolding (row identification OPEN) -/
464
465/-- Vertex permutation sending hinge `h` to the seed hinge `(0,1,2)`.
466Chosen so that remapped Gram cosines and flat Jacobians match the
467summand table (numerically verified; Lean geometric match OPEN for
468rows `h ≠ 0`). -/
469def hingeVertexPerm : Fin 10 → Fin 5 → Fin 5
470 | 0, v => v
471 | 1, 0 => 1 | 1, 1 => 2 | 1, 2 => 3 | 1, 3 => 0 | 1, 4 => 4
472 | 2, 0 => 1 | 2, 1 => 0 | 2, 2 => 3 | 2, 3 => 4 | 2, 4 => 2
473 | 3, 0 => 1 | 3, 1 => 3 | 3, 2 => 2 | 3, 3 => 0 | 3, 4 => 4
474 | 4, 0 => 1 | 4, 1 => 3 | 4, 2 => 0 | 4, 3 => 4 | 4, 4 => 2
475 | 5, 0 => 0 | 5, 1 => 3 | 5, 2 => 4 | 5, 3 => 1 | 5, 4 => 2
476 | 6, 0 => 3 | 6, 1 => 1 | 6, 2 => 0 | 6, 3 => 2 | 6, 4 => 4
477 | 7, 0 => 3 | 7, 1 => 0 | 7, 2 => 1 | 7, 3 => 4 | 7, 4 => 2
478 | 8, 0 => 3 | 8, 1 => 0 | 8, 2 => 4 | 8, 3 => 1 | 8, 4 => 2
479 | 9, 0 => 3 | 9, 1 => 4 | 9, 2 => 0 | 9, 3 => 1 | 9, 4 => 2
480
481/-- Inverse of `hingeVertexPerm` on vertices. -/
482def hingeVertexPermInv : Fin 10 → Fin 5 → Fin 5
483 | 0, v => v
484 | 1, 0 => 3 | 1, 1 => 0 | 1, 2 => 1 | 1, 3 => 2 | 1, 4 => 4
485 | 2, 0 => 1 | 2, 1 => 0 | 2, 2 => 4 | 2, 3 => 2 | 2, 4 => 3
486 | 3, 0 => 3 | 3, 1 => 0 | 3, 2 => 2 | 3, 3 => 1 | 3, 4 => 4
487 | 4, 0 => 2 | 4, 1 => 0 | 4, 2 => 4 | 4, 3 => 1 | 4, 4 => 3
488 | 5, 0 => 0 | 5, 1 => 3 | 5, 2 => 4 | 5, 3 => 1 | 5, 4 => 2
489 | 6, 0 => 2 | 6, 1 => 1 | 6, 2 => 3 | 6, 3 => 0 | 6, 4 => 4
490 | 7, 0 => 1 | 7, 1 => 2 | 7, 2 => 4 | 7, 3 => 0 | 7, 4 => 3
491 | 8, 0 => 1 | 8, 1 => 3 | 8, 2 => 4 | 8, 3 => 0 | 8, 4 => 2
492 | 9, 0 => 2 | 9, 1 => 3 | 9, 2 => 4 | 9, 3 => 0 | 9, 4 => 1
493
494/-- Edge slot whose length feeds remapped seed-slot `e` under hinge `h`. -/
495def pullEdgeSlot : Fin 10 → Fin 10 → Fin 10
496 | 0, e => e
497 | 1, 0 => 2 | 1, 1 => 5 | 1, 2 => 7 | 1, 3 => 9 | 1, 4 => 0
498 | 1, 5 => 1 | 1, 6 => 3 | 1, 7 => 4 | 1, 8 => 6 | 1, 9 => 8
499 | 2, 0 => 0 | 2, 1 => 6 | 2, 2 => 4 | 2, 3 => 5 | 2, 4 => 3
500 | 2, 5 => 1 | 2, 6 => 2 | 2, 7 => 8 | 2, 8 => 9 | 2, 9 => 7
501 | 3, 0 => 2 | 3, 1 => 7 | 3, 2 => 5 | 3, 3 => 9 | 3, 4 => 1
502 | 3, 5 => 0 | 3, 6 => 3 | 3, 7 => 4 | 3, 8 => 8 | 3, 9 => 6
503 | 4, 0 => 1 | 4, 1 => 8 | 4, 2 => 4 | 4, 3 => 7 | 4, 4 => 3
504 | 4, 5 => 0 | 4, 6 => 2 | 4, 7 => 6 | 4, 8 => 9 | 4, 9 => 5
505 | 5, 0 => 2 | 5, 1 => 3 | 5, 2 => 0 | 5, 3 => 1 | 5, 4 => 9
506 | 5, 5 => 5 | 5, 6 => 7 | 5, 7 => 6 | 5, 8 => 8 | 5, 9 => 4
507 | 6, 0 => 4 | 6, 1 => 7 | 6, 2 => 1 | 6, 3 => 8 | 6, 4 => 5
508 | 6, 5 => 0 | 6, 6 => 6 | 6, 7 => 2 | 6, 8 => 9 | 6, 9 => 3
509 | 7, 0 => 4 | 7, 1 => 6 | 7, 2 => 0 | 7, 3 => 5 | 7, 4 => 8
510 | 7, 5 => 1 | 7, 6 => 7 | 7, 7 => 3 | 7, 8 => 9 | 7, 9 => 2
511 | 8, 0 => 5 | 8, 1 => 6 | 8, 2 => 0 | 8, 3 => 4 | 8, 4 => 9
512 | 8, 5 => 2 | 8, 6 => 7 | 8, 7 => 3 | 8, 8 => 8 | 8, 9 => 1
513 | 9, 0 => 7 | 9, 1 => 8 | 9, 2 => 1 | 9, 3 => 4 | 9, 4 => 9
514 | 9, 5 => 2 | 9, 6 => 5 | 9, 7 => 3 | 9, 8 => 6 | 9, 9 => 0
515
516/-- Pull squared edges so hinge `h` occupies the Gram seed slots `(0,1,2)`. -/
517def remappedSqEdges (h : Fin 10) (a : SqEdges4) : SqEdges4 :=
518 fun e => a (pullEdgeSlot h e)
519
520theorem remappedSqEdges_seed_id :
521 remappedSqEdges 0 seedFlatSqEdges = seedFlatSqEdges := by
522 funext e; simp [remappedSqEdges, pullEdgeSlot]
523
524theorem remappedSqEdges_zero (a : SqEdges4) : remappedSqEdges 0 a = a := by
525 funext e; simp [remappedSqEdges, pullEdgeSlot]
526
527theorem remapped_seed_dihedral_eq (a : SqEdges4) :
528 seedDihedralAngle (remappedSqEdges 0 a) = seedDihedralAngle a := by
529 rw [remappedSqEdges_zero]
530
531/-! ## §8. Full pathwise identity (OPEN) -/
532
533structure Nondeg4Simplex (a : SqEdges4) : Prop where
534 edge_pos : ∀ e : Fin 10, 0 < a e
535 area_pos : ∀ h : Fin 10,
536 0 <
537 hingeArea (a (hingeBoundarySlots h 0))
538 (a (hingeBoundarySlots h 1)) (a (hingeBoundarySlots h 2))
539
540theorem nondeg_flat : Nondeg4Simplex flatSqEdges where
541 edge_pos := by
542 intro e; fin_cases e <;>
543 simp only [flatSqEdges, seedFlatSqEdges] <;> norm_num
544 area_pos := by
545 intro h
546 simpa [hingeAreaFlat, hingeFlatEdgeSq, flatSqEdges] using hingeAreaFlat_pos h
547
548def seedCosDihedral (a : SqEdges4) : ℝ := cosDihedral a
549
550/-- Full off-flat pathwise closed form is still absent. -/
551def freudenthal4SimplexPathwiseSchlaefliPresent : Bool := false
552
553theorem freudenthal4SimplexPathwiseSchlaefliPresent_false :
554 freudenthal4SimplexPathwiseSchlaefliPresent = false :=
555 rfl
556
557def Freudenthal4SimplexPathwiseSchlaefliTarget : Prop :=
558 freudenthal4SimplexPathwiseSchlaefliPresent = true
559
560theorem Freudenthal4SimplexPathwiseSchlaefliTarget_open :
561 ¬ Freudenthal4SimplexPathwiseSchlaefliTarget := by
562 intro h
563 have : false = true := h
564 exact Bool.false_ne_true this
565
566/-- Remainder comparing a candidate Jacobian to the flat table. -/
567def PathwiseFlatRemainder (a : SqEdges4)
568 (dTheta : Fin 10 → Fin 10 → ℝ) : Prop :=
569 ∀ e : Fin 10,
570 (∑ h : Fin 10,
571 hingeArea (a (hingeBoundarySlots h 0))
572 (a (hingeBoundarySlots h 1)) (a (hingeBoundarySlots h 2)) *
573 dTheta h e) -
574 (∑ h : Fin 10, flatSchlaefliSummand h e) = 0
575
576theorem pathwiseFlatRemainder_flat_zero :
577 PathwiseFlatRemainder flatSqEdges
578 (fun h e => flatSchlaefliSummand h e / hingeAreaFlat h) := by
579 intro e
580 have hsum := freudenthal4SimplexFlatSchlaefli e
581 have hareas :
582 (∑ h : Fin 10,
583 hingeArea (flatSqEdges (hingeBoundarySlots h 0))
584 (flatSqEdges (hingeBoundarySlots h 1))
585 (flatSqEdges (hingeBoundarySlots h 2)) *
586 (flatSchlaefliSummand h e / hingeAreaFlat h)) =
587 ∑ h : Fin 10, flatSchlaefliSummand h e := by
588 refine Finset.sum_congr rfl fun h _ => ?_
589 have ha :
590 hingeArea (flatSqEdges (hingeBoundarySlots h 0))
591 (flatSqEdges (hingeBoundarySlots h 1))
592 (flatSqEdges (hingeBoundarySlots h 2)) =
593 hingeAreaFlat h := by
594 rfl
595 rw [ha]
596 field_simp [ne_of_gt (hingeAreaFlat_pos h)]
597 rw [hareas, hsum, sub_self]
598
599/-- Flat directional form of the remainder: vanishes for every velocity. -/
600theorem pathwiseFlatRemainder_directional_zero (v : Fin 10 → ℝ) :
601 (∑ h : Fin 10, hingeAreaFlat h * flatDirectionalAngleDeriv v h) -
602 (∑ e : Fin 10, v e * (∑ h : Fin 10, flatSchlaefliSummand h e)) = 0 := by
603 rw [freudenthal4SimplexFlatDirectionalSchlaefli v]
604 simp [freudenthal4SimplexFlatSchlaefli]
605
606/-! ## §9. Status -/
607
608structure Regge4DSchlaefliPathwiseStatus where
609 flatClosedForm : Bool
610 seedGeometricMatch : Bool
611 nonvacuousFlatWitness : Bool
612 seedAngleHasDerivAt : Bool
613 flatDirectionalPresent : Bool
614 fullPathwisePresent : Bool
615 gapActionRecovery : Bool
616
617def regge4DSchlaefliPathwiseStatus : Regge4DSchlaefliPathwiseStatus where
618 flatClosedForm := true
619 seedGeometricMatch := true
620 nonvacuousFlatWitness := true
621 seedAngleHasDerivAt := true
622 flatDirectionalPresent := true
623 fullPathwisePresent := false
624 gapActionRecovery := false
625
626theorem regge4DSchlaefliPathwiseStatus_flags :
627 regge4DSchlaefliPathwiseStatus.flatClosedForm = true ∧
628 regge4DSchlaefliPathwiseStatus.seedGeometricMatch = true ∧
629 regge4DSchlaefliPathwiseStatus.nonvacuousFlatWitness = true ∧
630 regge4DSchlaefliPathwiseStatus.seedAngleHasDerivAt = true ∧
631 regge4DSchlaefliPathwiseStatus.flatDirectionalPresent = true ∧
632 regge4DSchlaefliPathwiseStatus.fullPathwisePresent = false ∧
633 regge4DSchlaefliPathwiseStatus.gapActionRecovery = false := by
634 decide
635
636end
637
638end Regge4DSchlaefliPathwise
639end Analysis
640end Gravity
641end IndisputableMonolith
642