IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity
IndisputableMonolith/Gravity/SevenGaps/HKTKineticNormalizedRigidity.lean · 1210 lines · 85 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill
2import IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE
3import Mathlib.Analysis.Calculus.ContDiff.Basic
4import Mathlib.Analysis.Calculus.Deriv.Basic
5import Mathlib.Analysis.Calculus.Deriv.Prod
6import Mathlib.Analysis.Calculus.FDeriv.Comp
7import Mathlib.Analysis.Calculus.FDeriv.Prod
8import Mathlib.Analysis.Calculus.MeanValue
9/-!
10# Wave C4/C5 gap5: mod-vacuum kill + kinetic-normalized rigidity terminal
11
12Binding: `D-qg-hkt-modvacuum-verdict-20260723` (Codex cross-family, 2026-07-23);
13C5 upgrade: `D-gap5-acceptance-adjudication-20260723`.
14
15Part 1: `¬ HKTRigidityModVacuumStatementN2` via variable-kinetic CanonicalMom
16inhabitant. Part 2: `KineticNormalizedCanonicalMom` intensivity field; FTC
17recovery is theorem-derived (`ftc_recovery_of_normalized`), not an assumed
18class field. Flip of `gap5_constraint_recovery` is owned by
19`Gap5ConstraintCloseStatus` after both ledger halves bind green.
20-/
21
22namespace IndisputableMonolith
23namespace Gravity
24namespace SevenGaps
25namespace HKTKineticNormalizedRigidity
26
27open HypersurfaceDeformation DynamicStructureBracket DynamicStructureFunctionBlocker
28open HKTPointSplitTarget HKTPointSplitStrong HKTLocalFunctionalEquation
29open HKTCanonicalMomTarget HKTCanonicalMomRigidity
30open HKTVacuumSectorKill FullTheoryLedger
31
32noncomputable section
33
34open Finset
35
36private lemma zmod2_zero_add_one : (0 : ZMod 2) + 1 = 1 := by decide
37private lemma zmod2_one_add_one : (1 : ZMod 2) + 1 = 0 := by decide
38private lemma zmod2_zero_add_two : (0 : ZMod 2) + 2 = 0 := by decide
39private lemma zmod2_one_add_two : (1 : ZMod 2) + 2 = 1 := by decide
40
41/-! ## §1. Variable-kinetic profiles -/
42
43def vacuumKineticA (a : ℝ) : ℝ := (1 + a * a)⁻¹
44
45def vacuumKineticW (a b : ℝ) : ℝ :=
46 a ^ 6 / 24 + 7 * a ^ 4 / 24 - a ^ 3 * b ^ 3 / 6 - a ^ 3 * b / 2 +
47 a ^ 2 * b ^ 4 / 8 + a ^ 2 * b ^ 2 / 4 + a ^ 2 / 4 -
48 a * b ^ 3 / 6 - a * b / 2 + b ^ 4 / 8 + b ^ 2 / 4
49
50def vacuumKineticK (a b : ℝ) : ℝ :=
51 let d := b - a
52 (1 + a * a) * (d * d) / 2 + (2 * a) * (d ^ 3) / 3 + (d ^ 4) / 4
53
54theorem vacuumKineticW_eq_design (a b : ℝ) :
55 vacuumKineticW a b =
56 (1 / 2 : ℝ) * (1 + a * a) * vacuumKineticK a b := by
57 unfold vacuumKineticW vacuumKineticK; ring
58
59def vacuumKineticLocalProfile : LocalHamProfile :=
60 fun a b p => vacuumKineticA a * (p * p) + vacuumKineticW a b
61
62def vacuumKineticHamDensity (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
63 vacuumKineticLocalProfile (x.1 j) (x.1 (j + 1)) (x.2 j)
64
65theorem one_add_sq_ne_zero (a : ℝ) : (1 : ℝ) + a * a ≠ 0 := by
66 nlinarith [mul_self_nonneg a]
67
68theorem vacuumKineticA_pos (a : ℝ) : 0 < vacuumKineticA a :=
69 inv_pos.mpr (by nlinarith [mul_self_nonneg a])
70
71theorem vacuumKineticA_ne_zero (a : ℝ) : vacuumKineticA a ≠ 0 :=
72 (vacuumKineticA_pos a).ne'
73
74theorem vacuumKineticW_diag (a : ℝ) : vacuumKineticW a a = 0 := by
75 unfold vacuumKineticW; ring
76
77theorem vacuumKinetic_diag (a p : ℝ) :
78 vacuumKineticLocalProfile a a p = vacuumKineticA a * (p * p) := by
79 simp only [vacuumKineticLocalProfile, vacuumKineticW_diag a, add_zero]
80
81def vacuumKineticHbClosed (a b : ℝ) : ℝ :=
82 (1 / 2 : ℝ) * (1 + a * a) * (b - a) * (1 + b * b)
83
84def vacuumKineticHpClosed (a p : ℝ) : ℝ :=
85 (2 : ℝ) * vacuumKineticA a * p
86
87/-! ### ContDiff-2 (obligation only needs 2; avoid ContDiff ⊤ and heavy `.comp` whnf) -/
88
89/-- Inverse on ℝ first; product-space `.inv` at ⊤ times out. -/
90private theorem contDiff_vacuumKineticA :
91 ContDiff ℝ 2 vacuumKineticA := by
92 have h1a2 : ContDiff ℝ 2 (fun a : ℝ => (1 : ℝ) + a * a) :=
93 contDiff_const.add (contDiff_id.mul contDiff_id)
94 change ContDiff ℝ 2 (fun a : ℝ => ((1 : ℝ) + a * a)⁻¹)
95 exact h1a2.inv one_add_sq_ne_zero
96
97private theorem contDiff_vacuumKinetic_kinTerm :
98 ContDiff ℝ 2 (fun t : ℝ × ℝ × ℝ => vacuumKineticA t.1 * (t.2.2 * t.2.2)) := by
99 have ha : ContDiff ℝ 2 (fun t : ℝ × ℝ × ℝ => t.1) := contDiff_fst
100 have hp : ContDiff ℝ 2 (fun t : ℝ × ℝ × ℝ => t.2.2) :=
101 contDiff_snd.comp contDiff_snd
102 exact (contDiff_vacuumKineticA.comp ha).mul (hp.mul hp)
103
104/-- Direct unfold+fun_prop; `.comp` of the 2-site W ContDiff times out in whnf. -/
105private theorem contDiff_vacuumKinetic_wTerm :
106 ContDiff ℝ 2 (fun t : ℝ × ℝ × ℝ => vacuumKineticW t.1 t.2.1) := by
107 unfold vacuumKineticW
108 fun_prop
109
110set_option maxHeartbeats 800000 in
111theorem vacuumKinetic_profile_contDiff :
112 ContDiff ℝ 2 (profileMap vacuumKineticLocalProfile) := by
113 have hEq : profileMap vacuumKineticLocalProfile =
114 fun t => vacuumKineticA t.1 * (t.2.2 * t.2.2) + vacuumKineticW t.1 t.2.1 := by
115 funext t; rfl
116 rw [hEq]
117 exact contDiff_vacuumKinetic_kinTerm.add contDiff_vacuumKinetic_wTerm
118
119theorem vacuumKineticLocalProfile_contDiff2 :
120 LocalHamSmoothContDiff2Obligation vacuumKineticLocalProfile :=
121 vacuumKinetic_profile_contDiff
122
123/-! ### Closed-form derivatives -/
124
125theorem hasDerivAt_vacuumKinetic_p (a b p : ℝ) :
126 HasDerivAt (fun t => vacuumKineticLocalProfile a b t)
127 (vacuumKineticHpClosed a p) p := by
128 have hpow : HasDerivAt (fun t : ℝ => t ^ 2) ((2 : ℝ) * p) p := by
129 simpa using (hasDerivAt_id p).pow 2
130 have hkin := hpow.const_mul (vacuumKineticA a)
131 have hW : HasDerivAt (fun _ : ℝ => vacuumKineticW a b) 0 p :=
132 hasDerivAt_const p (vacuumKineticW a b)
133 have heq : (fun t => vacuumKineticLocalProfile a b t) =
134 fun t => vacuumKineticA a * t ^ 2 + vacuumKineticW a b := by
135 funext t
136 change vacuumKineticA a * (t * t) + vacuumKineticW a b =
137 vacuumKineticA a * t ^ 2 + vacuumKineticW a b
138 rw [pow_two]
139 have hrw : vacuumKineticA a * ((2 : ℝ) * p) + 0 = vacuumKineticHpClosed a p := by
140 simp [vacuumKineticHpClosed]; ring
141 rw [heq]
142 exact hrw ▸ hkin.add hW
143
144private theorem hasDerivAt_vacuumKineticK_b (a b : ℝ) :
145 HasDerivAt (fun s => vacuumKineticK a s)
146 (((1 : ℝ) + a * a) * (b - a) + (2 * a) * (b - a) ^ 2 + (b - a) ^ 3) b := by
147 have hd : HasDerivAt (fun s : ℝ => s - a) (1 : ℝ) b :=
148 (hasDerivAt_id b).sub_const a
149 -- Keep Mathlib's expanded derivative expressions, then rewrite coefficients.
150 have t1raw :=
151 ((hasDerivAt_const b ((1 : ℝ) + a * a)).mul (hd.pow 2)).div_const (2 : ℝ)
152 have t1 :
153 HasDerivAt (fun s => ((1 : ℝ) + a * a) * (s - a) ^ 2 / 2)
154 (((1 : ℝ) + a * a) * (b - a)) b := by
155 have hrw :
156 ((0 : ℝ) * (b - a) ^ 2 + ((1 : ℝ) + a * a) * (↑2 * (b - a) ^ (2 - 1) * 1)) / 2 =
157 ((1 : ℝ) + a * a) * (b - a) := by ring
158 exact hrw ▸ t1raw
159 have t2raw :=
160 ((hasDerivAt_const b ((2 : ℝ) * a)).mul (hd.pow 3)).div_const (3 : ℝ)
161 have t2 :
162 HasDerivAt (fun s => (2 * a) * (s - a) ^ 3 / 3)
163 ((2 * a) * (b - a) ^ 2) b := by
164 have hrw :
165 ((0 : ℝ) * (b - a) ^ 3 + (2 * a) * (↑3 * (b - a) ^ (3 - 1) * 1)) / 3 =
166 (2 * a) * (b - a) ^ 2 := by ring
167 exact hrw ▸ t2raw
168 have t3raw := (hd.pow 4).div_const (4 : ℝ)
169 have t3 :
170 HasDerivAt (fun s => (s - a) ^ 4 / 4) ((b - a) ^ 3) b := by
171 have hrw : (↑4 * (b - a) ^ (4 - 1) * 1) / 4 = (b - a) ^ 3 := by ring
172 exact hrw ▸ t3raw
173 have hfun :
174 (fun s => vacuumKineticK a s) =
175 fun s =>
176 ((1 : ℝ) + a * a) * (s - a) ^ 2 / 2 +
177 (2 * a) * (s - a) ^ 3 / 3 + (s - a) ^ 4 / 4 := by
178 funext s; simp only [vacuumKineticK]; ring
179 rw [hfun]
180 exact (t1.add t2).add t3
181
182theorem hasDerivAt_vacuumKineticW_b (a b : ℝ) :
183 HasDerivAt (fun s => vacuumKineticW a s) (vacuumKineticHbClosed a b) b := by
184 have hEq : (fun s => vacuumKineticW a s) =
185 fun s => (1 / 2 : ℝ) * (1 + a * a) * vacuumKineticK a s := by
186 funext s; exact vacuumKineticW_eq_design a s
187 rw [hEq]
188 have hC : HasDerivAt (fun _ : ℝ => (1 / 2 : ℝ) * (1 + a * a)) 0 b :=
189 hasDerivAt_const b _
190 have hK := hasDerivAt_vacuumKineticK_b a b
191 have hrwW :
192 0 * vacuumKineticK a b +
193 ((1 / 2 : ℝ) * (1 + a * a)) *
194 (((1 : ℝ) + a * a) * (b - a) + (2 * a) * (b - a) ^ 2 + (b - a) ^ 3) =
195 vacuumKineticHbClosed a b := by
196 simp only [vacuumKineticHbClosed]; ring
197 exact hrwW ▸ hC.mul hK
198
199theorem hasDerivAt_vacuumKinetic_b (a b p : ℝ) :
200 HasDerivAt (fun s => vacuumKineticLocalProfile a s p)
201 (vacuumKineticHbClosed a b) b := by
202 have hA : HasDerivAt (fun _ : ℝ => vacuumKineticA a * (p * p)) 0 b :=
203 hasDerivAt_const b (vacuumKineticA a * (p * p))
204 have heq : (fun s => vacuumKineticLocalProfile a s p) =
205 fun s => vacuumKineticA a * (p * p) + vacuumKineticW a s := by
206 funext s; rfl
207 have hrw : (0 : ℝ) + vacuumKineticHbClosed a b = vacuumKineticHbClosed a b := by
208 ring
209 rw [heq]
210 exact hrw ▸ hA.add (hasDerivAt_vacuumKineticW_b a b)
211
212/-! ### Slot partials via fderiv (definitional Frechet match) -/
213
214def vacuumKineticLocalHa : LocalHamProfile :=
215 fun a b p =>
216 fderiv ℝ (profileMap vacuumKineticLocalProfile) (a, b, p) (1, 0, 0)
217
218def vacuumKineticLocalHb : LocalHamProfile :=
219 fun a b p =>
220 fderiv ℝ (profileMap vacuumKineticLocalProfile) (a, b, p) (0, 1, 0)
221
222def vacuumKineticLocalHp : LocalHamProfile :=
223 fun a b p =>
224 fderiv ℝ (profileMap vacuumKineticLocalProfile) (a, b, p) (0, 0, 1)
225
226theorem vacuumKineticLocalHp_eq_closed (a b p : ℝ) :
227 vacuumKineticLocalHp a b p = vacuumKineticHpClosed a p := by
228 have hF :=
229 ((vacuumKinetic_profile_contDiff.of_le
230 (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
231 (a, b, p)).hasFDerivAt
232 have hφ : HasDerivAt (fun t : ℝ => ((a, b, t) : ℝ × ℝ × ℝ)) (0, 0, 1) p :=
233 (hasDerivAt_const p a).prodMk ((hasDerivAt_const p b).prodMk (hasDerivAt_id p))
234 have hline := hF.comp_hasDerivAt p hφ
235 have hclosed := hasDerivAt_vacuumKinetic_p a b p
236 change HasDerivAt (fun t => vacuumKineticLocalProfile a b t) _ p at hline
237 exact HasDerivAt.unique hline hclosed
238
239theorem vacuumKineticLocalHb_eq_closed (a b p : ℝ) :
240 vacuumKineticLocalHb a b p = vacuumKineticHbClosed a b := by
241 have hF :=
242 ((vacuumKinetic_profile_contDiff.of_le
243 (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
244 (a, b, p)).hasFDerivAt
245 have hφ : HasDerivAt (fun s : ℝ => ((a, s, p) : ℝ × ℝ × ℝ)) (0, 1, 0) b :=
246 (hasDerivAt_const b a).prodMk ((hasDerivAt_id b).prodMk (hasDerivAt_const b p))
247 have hline := hF.comp_hasDerivAt b hφ
248 have hclosed := hasDerivAt_vacuumKinetic_b a b p
249 change HasDerivAt (fun s => vacuumKineticLocalProfile a s p) _ b at hline
250 exact HasDerivAt.unique hline hclosed
251
252theorem vacuumKinetic_FE (a b p r : ℝ) :
253 vacuumKineticLocalHb a b p * vacuumKineticLocalHp b a r -
254 vacuumKineticLocalHb b a r * vacuumKineticLocalHp a b p =
255 (1 : ℝ) * (b - a) *
256 ((fun q => 1 + q * q) a * r + (fun q => 1 + q * q) b * p) := by
257 rw [vacuumKineticLocalHb_eq_closed, vacuumKineticLocalHp_eq_closed,
258 vacuumKineticLocalHb_eq_closed, vacuumKineticLocalHp_eq_closed]
259 simp only [vacuumKineticHbClosed, vacuumKineticHpClosed, vacuumKineticA]
260 have ha0 := one_add_sq_ne_zero a
261 have hb0 := one_add_sq_ne_zero b
262 field_simp [ha0, hb0]
263 ring
264
265theorem vacuumKinetic_localCoeff_eq_structure_mom
266 (x : PhaseSpace 2) (j : ZMod 2) :
267 vacuumKineticLocalHb (x.1 j) (x.1 (j + 1)) (x.2 j) *
268 vacuumKineticLocalHp (x.1 (j + 1)) (x.1 (j + 2)) (x.2 (j + 1)) =
269 structureDyn x j * momDynDensity x j := by
270 rw [vacuumKineticLocalHb_eq_closed, vacuumKineticLocalHp_eq_closed]
271 simp only [vacuumKineticHbClosed, vacuumKineticHpClosed, vacuumKineticA,
272 structureDyn, momDynDensity]
273 have h := one_add_sq_ne_zero (x.1 (j + 1))
274 field_simp [h]
275
276/-! ### LocalHamSmooth -/
277
278def vacuumKineticCellCoords (j : ZMod 2) (y : PhaseSpace 2) : ℝ × ℝ × ℝ :=
279 (y.1 j, y.1 (j + 1), y.2 j)
280
281def vacuumKineticCellCoordsD (j : ZMod 2) : PhaseSpace 2 →L[ℝ] ℝ × ℝ × ℝ :=
282 (coordQ j).prod ((coordQ (j + 1)).prod (coordP j))
283
284lemma hasFDerivAt_vacuumKineticCellCoords (j : ZMod 2) (x : PhaseSpace 2) :
285 HasFDerivAt (vacuumKineticCellCoords j) (vacuumKineticCellCoordsD j) x :=
286 (hasFDerivAt_coord_fst j x).prodMk
287 ((hasFDerivAt_coord_fst (j + 1) x).prodMk (hasFDerivAt_coord_snd j x))
288
289lemma hasFDerivAt_vacuumKineticLocalCell (j : ZMod 2) (x : PhaseSpace 2) :
290 HasFDerivAt (fun y : PhaseSpace 2 =>
291 vacuumKineticLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j))
292 ((vacuumKineticLocalHa (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
293 (vacuumKineticLocalHb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
294 (vacuumKineticLocalHp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j)
295 x := by
296 have hProf :=
297 ((vacuumKinetic_profile_contDiff.of_le
298 (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
299 (vacuumKineticCellCoords j x)).hasFDerivAt
300 have hcomp := hProf.comp x (hasFDerivAt_vacuumKineticCellCoords j x)
301 have hfun :
302 (fun y : PhaseSpace 2 =>
303 vacuumKineticLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j)) =
304 profileMap vacuumKineticLocalProfile ∘ vacuumKineticCellCoords j := rfl
305 rw [hfun]
306 have hL :
307 fderiv ℝ (profileMap vacuumKineticLocalProfile) (vacuumKineticCellCoords j x) ∘L
308 vacuumKineticCellCoordsD j =
309 (vacuumKineticLocalHa (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
310 (vacuumKineticLocalHb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
311 (vacuumKineticLocalHp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j := by
312 apply ContinuousLinearMap.ext
313 intro v
314 set hf :=
315 fderiv ℝ (profileMap vacuumKineticLocalProfile)
316 (vacuumKineticCellCoords j x)
317 -- Evaluate both sides on v.
318 simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
319 ContinuousLinearMap.smul_apply, ContinuousLinearMap.prod_apply,
320 vacuumKineticCellCoordsD, vacuumKineticLocalHa, vacuumKineticLocalHb,
321 vacuumKineticLocalHp, vacuumKineticCellCoords, coordQ_apply, coordP_apply,
322 smul_eq_mul]
323 -- hf (vq_j, vq_{j+1}, vp_j) = linear combination of basis images
324 have hlin :
325 hf (v.1 j, v.1 (j + 1), v.2 j) =
326 hf (1, 0, 0) * v.1 j + hf (0, 1, 0) * v.1 (j + 1) +
327 hf (0, 0, 1) * v.2 j := by
328 have hv :
329 ((v.1 j, v.1 (j + 1), v.2 j) : ℝ × ℝ × ℝ) =
330 (v.1 j : ℝ) • ((1, 0, 0) : ℝ × ℝ × ℝ) +
331 (v.1 (j + 1) : ℝ) • ((0, 1, 0) : ℝ × ℝ × ℝ) +
332 (v.2 j : ℝ) • ((0, 0, 1) : ℝ × ℝ × ℝ) := by
333 simp [Prod.smul_def]
334 rw [hv, map_add, map_add, map_smul, map_smul, map_smul]
335 simp [smul_eq_mul]
336 ring
337 exact hlin
338 exact hL ▸ hcomp
339
340def vacuumKineticLocalSmooth : LocalHamSmooth vacuumKineticLocalProfile where
341 ha := vacuumKineticLocalHa
342 hb := vacuumKineticLocalHb
343 hp := vacuumKineticLocalHp
344 hasFDerivCell := hasFDerivAt_vacuumKineticLocalCell
345
346/-! ## §2. Advection + class inhabitant -/
347
348def vacuumKineticHamAdvFrom (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
349 -bracket (fun y => ∑ i : ZMod 2, siteDelta j i * momDynDensity y i)
350 (fun y => ∑ i : ZMod 2, siteDelta j i * vacuumKineticHamDensity y i) x
351
352def vacuumKineticHamAdvTo (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
353 bracket (fun y => ∑ i : ZMod 2, siteDelta j i * momDynDensity y i)
354 (fun y => ∑ i : ZMod 2, siteDelta (j + 1) i * vacuumKineticHamDensity y i) x
355
356theorem vacuumKineticHam_eq_LocalHamFromProfile (N : ZMod 2 → ℝ) :
357 (fun y => ∑ j : ZMod 2, N j * vacuumKineticHamDensity y j) =
358 LocalHamFromProfile vacuumKineticLocalProfile N := by
359 funext y; rfl
360
361theorem differentiable_vacuumKineticHam (N : ZMod 2 → ℝ) :
362 Differentiable ℝ (fun y => ∑ j : ZMod 2, N j * vacuumKineticHamDensity y j) := by
363 simpa [vacuumKineticHam_eq_LocalHamFromProfile] using
364 differentiable_LocalHamFromProfile vacuumKineticLocalProfile
365 vacuumKineticLocalSmooth N
366
367/-- Bilinear expansion of the Poisson bracket for two-site smeared densitiess. -/
368theorem bracket_bilinear_basis_zmod2
369 (F G : ZMod 2 → PhaseSpace 2 → ℝ)
370 (hF : ∀ i, Differentiable ℝ (F i)) (hG : ∀ k, Differentiable ℝ (G k))
371 (c d : ZMod 2 → ℝ) (x : PhaseSpace 2) :
372 bracket (fun y => ∑ i : ZMod 2, c i * F i y)
373 (fun y => ∑ k : ZMod 2, d k * G k y) x =
374 ∑ i : ZMod 2, ∑ k : ZMod 2, c i * d k * bracket (F i) (G k) x := by
375 have hF0 := hF 0 x; have hF1 := hF 1 x
376 have hG0 := hG 0 x; have hG1 := hG 1 x
377 have hCL :
378 (fun y => ∑ i : ZMod 2, c i * F i y) =
379 fun y => c 0 * F 0 y + c 1 * F 1 y := by
380 funext y; simp [sum_zmod2]
381 have hDR :
382 (fun y => ∑ k : ZMod 2, d k * G k y) =
383 fun y => d 0 * G 0 y + d 1 * G 1 y := by
384 funext y; simp [sum_zmod2]
385 rw [hCL, hDR]
386 have hR :=
387 bracket_add_right (n := 2) (fun y => c 0 * F 0 y + c 1 * F 1 y)
388 (hG0.const_mul (d 0)) (hG1.const_mul (d 1))
389 have hL0 :=
390 bracket_add_left (n := 2) (G 0) (hF0.const_mul (c 0)) (hF1.const_mul (c 1))
391 have hL1 :=
392 bracket_add_left (n := 2) (G 1) (hF0.const_mul (c 0)) (hF1.const_mul (c 1))
393 have hc0G0 := bracket_const_mul_left (n := 2) (G 0) hF0 (c 0)
394 have hc1G0 := bracket_const_mul_left (n := 2) (G 0) hF1 (c 1)
395 have hc0G1 := bracket_const_mul_left (n := 2) (G 1) hF0 (c 0)
396 have hc1G1 := bracket_const_mul_left (n := 2) (G 1) hF1 (c 1)
397 have hd0F0 := bracket_const_mul_right (n := 2) (F 0) hG0 (d 0)
398 have hd0F1 := bracket_const_mul_right (n := 2) (F 1) hG0 (d 0)
399 have hd1F0 := bracket_const_mul_right (n := 2) (F 0) hG1 (d 1)
400 have hd1F1 := bracket_const_mul_right (n := 2) (F 1) hG1 (d 1)
401 -- Expand both sides on ZMod 2 and finish by bilinearity.
402 simp only [sum_zmod2]
403 have hMain :
404 bracket (fun y => c 0 * F 0 y + c 1 * F 1 y)
405 (fun y => d 0 * G 0 y + d 1 * G 1 y) x =
406 c 0 * d 0 * bracket (F 0) (G 0) x + c 0 * d 1 * bracket (F 0) (G 1) x +
407 (c 1 * d 0 * bracket (F 1) (G 0) x + c 1 * d 1 * bracket (F 1) (G 1) x) := by
408 have hStep1 := hR
409 have hStep2 :
410 bracket (fun y => c 0 * F 0 y + c 1 * F 1 y) (fun y => d 0 * G 0 y) x +
411 bracket (fun y => c 0 * F 0 y + c 1 * F 1 y) (fun y => d 1 * G 1 y) x =
412 d 0 * bracket (fun y => c 0 * F 0 y + c 1 * F 1 y) (G 0) x +
413 d 1 * bracket (fun y => c 0 * F 0 y + c 1 * F 1 y) (G 1) x := by
414 rw [bracket_const_mul_right (n := 2)
415 (fun y => c 0 * F 0 y + c 1 * F 1 y) hG0 (d 0),
416 bracket_const_mul_right (n := 2)
417 (fun y => c 0 * F 0 y + c 1 * F 1 y) hG1 (d 1)]
418 have hStep3 :
419 d 0 * bracket (fun y => c 0 * F 0 y + c 1 * F 1 y) (G 0) x +
420 d 1 * bracket (fun y => c 0 * F 0 y + c 1 * F 1 y) (G 1) x =
421 d 0 * (c 0 * bracket (F 0) (G 0) x + c 1 * bracket (F 1) (G 0) x) +
422 d 1 * (c 0 * bracket (F 0) (G 1) x + c 1 * bracket (F 1) (G 1) x) := by
423 rw [hL0, hL1, hc0G0, hc1G0, hc0G1, hc1G1]
424 linarith [hStep1, hStep2, hStep3]
425 exact hMain
426
427theorem mom_ham_split_vacuumKinetic (w N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
428 bracket (MomDyn w)
429 (fun y => ∑ j : ZMod 2, N j * vacuumKineticHamDensity y j) x =
430 ∑ j : ZMod 2,
431 w j *
432 (N (j + 1) * vacuumKineticHamAdvTo x j -
433 N j * vacuumKineticHamAdvFrom x j) := by
434 let F : ZMod 2 → PhaseSpace 2 → ℝ := fun i y =>
435 ∑ k : ZMod 2, siteDelta i k * momDynDensity y k
436 let G : ZMod 2 → PhaseSpace 2 → ℝ := fun i y =>
437 ∑ k : ZMod 2, siteDelta i k * vacuumKineticHamDensity y k
438 have hF : ∀ i, Differentiable ℝ (F i) := by
439 intro i; simpa [F, MomDyn] using differentiable_MomDyn (siteDelta i)
440 have hG : ∀ i, Differentiable ℝ (G i) := by
441 intro i
442 simpa [G] using differentiable_vacuumKineticHam (siteDelta i)
443 have hMom : MomDyn w = fun y => ∑ i : ZMod 2, w i * F i y := by
444 funext y
445 simp only [MomDyn, F, sum_zmod2, siteDelta]
446 have h00 : siteDelta (0 : ZMod 2) 0 = (1 : ℝ) := by simp [siteDelta]
447 have h11 : siteDelta (1 : ZMod 2) 1 = (1 : ℝ) := by simp [siteDelta]
448 have h01 : siteDelta (0 : ZMod 2) 1 = (0 : ℝ) := by simp [siteDelta]
449 have h10 : siteDelta (1 : ZMod 2) 0 = (0 : ℝ) := by simp [siteDelta]
450 simp [h00, h11, h01, h10]
451 have hHam :
452 (fun y => ∑ j : ZMod 2, N j * vacuumKineticHamDensity y j) =
453 fun y => ∑ k : ZMod 2, N k * G k y := by
454 funext y
455 simp only [G, sum_zmod2, siteDelta]
456 have h00 : siteDelta (0 : ZMod 2) 0 = (1 : ℝ) := by simp [siteDelta]
457 have h11 : siteDelta (1 : ZMod 2) 1 = (1 : ℝ) := by simp [siteDelta]
458 have h01 : siteDelta (0 : ZMod 2) 1 = (0 : ℝ) := by simp [siteDelta]
459 have h10 : siteDelta (1 : ZMod 2) 0 = (0 : ℝ) := by simp [siteDelta]
460 simp [h00, h11, h01, h10]
461 rw [hMom, hHam, bracket_bilinear_basis_zmod2 F G hF hG w N x]
462 -- RHS Kronecker form.
463 have hR :
464 (∑ j : ZMod 2,
465 w j *
466 (N (j + 1) * vacuumKineticHamAdvTo x j -
467 N j * vacuumKineticHamAdvFrom x j)) =
468 ∑ i : ZMod 2, ∑ k : ZMod 2, w i * N k * bracket (F i) (G k) x := by
469 simp only [vacuumKineticHamAdvFrom, vacuumKineticHamAdvTo, F, G, sum_zmod2,
470 zmod2_zero_add_one, zmod2_one_add_one]
471 ring
472 exact hR.symm
473
474theorem ham_ham_vacuumKinetic (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
475 bracket (fun y => ∑ j : ZMod 2, N j * vacuumKineticHamDensity y j)
476 (fun y => ∑ j : ZMod 2, M j * vacuumKineticHamDensity y j) x =
477 ∑ j : ZMod 2,
478 (N j * M (j + 1) - M j * N (j + 1)) *
479 (structureDyn x j * momDynDensity x j) := by
480 have hL :=
481 local_profile_ham_ham_form vacuumKineticLocalProfile vacuumKineticLocalSmooth
482 N M x
483 -- Transport density names to LocalHamFromProfile, then match coefficients.
484 simpa [vacuumKineticHam_eq_LocalHamFromProfile, localHamHamCoefficient,
485 vacuumKineticLocalSmooth, vacuumKinetic_localCoeff_eq_structure_mom] using hL
486
487def vacuumKineticNondegPhase : PhaseSpace 2 :=
488 (fun _ => (0 : ℝ), fun j => if j = (0 : ZMod 2) then (1 : ℝ) else 0)
489
490theorem vacuumKinetic_nondeg :
491 vacuumKineticHamDensity vacuumKineticNondegPhase (0 : ZMod 2) ≠ 0 := by
492 simp only [vacuumKineticHamDensity, vacuumKineticLocalProfile, vacuumKineticNondegPhase,
493 vacuumKineticA, vacuumKineticW, zmod2_zero_add_one]
494 norm_num
495
496def vacuumKineticWeakTarget : HKTPointSplitTargetDyn 2 where
497 hamDensity := vacuumKineticHamDensity
498 momDensity := momDynDensity
499 structureFunction := structureDyn
500 hamAdvFrom := vacuumKineticHamAdvFrom
501 hamAdvTo := vacuumKineticHamAdvTo
502 momBracketDensity := momDynBracketDensity
503 ham_differentiable := differentiable_vacuumKineticHam
504 mom_differentiable := differentiable_MomDyn
505 structure_nonconstant := structureDyn_not_constant
506 ham_local := by
507 intro x y j hx0 hx1 hp
508 dsimp [vacuumKineticHamDensity]
509 rw [hx0, hx1, hp]
510 ham_covariant := by
511 intro x a j
512 dsimp [vacuumKineticHamDensity]
513 have e1 : (j + a + 1 : ZMod 2) = j + 1 + a := by ring
514 simp only [e1]
515 structure_local := by
516 intro x y j hx
517 dsimp [structureDyn]; rw [hx]
518 mom_mom := by
519 intro v w x
520 simpa [MomDyn] using bracket_MomDyn_MomDyn v w x
521 mom_ham_split := by
522 intro w N x
523 simpa [MomDyn] using mom_ham_split_vacuumKinetic w N x
524 ham_ham := ham_ham_vacuumKinetic
525 nondegenerate := ⟨vacuumKineticNondegPhase, (0 : ZMod 2), vacuumKinetic_nondeg⟩
526
527theorem vacuumKinetic_kinetic_regular_witness :
528 pderivP (fun y => ∑ i : ZMod 2, vacuumKineticHamDensity y i) (0 : ZMod 2)
529 vacuumKineticNondegPhase ≠ 0 := by
530 have hEq :
531 (fun y => ∑ i : ZMod 2, vacuumKineticHamDensity y i) =
532 LocalHamFromProfile vacuumKineticLocalProfile (fun _ => (1 : ℝ)) := by
533 funext y
534 simp [LocalHamFromProfile, vacuumKineticHamDensity]
535 rw [hEq]
536 have hP :=
537 pderivP_LocalHamFromProfile vacuumKineticLocalProfile vacuumKineticLocalSmooth
538 (fun _ => (1 : ℝ)) (0 : ZMod 2) vacuumKineticNondegPhase
539 rw [hP, one_mul]
540 change vacuumKineticLocalHp (vacuumKineticNondegPhase.1 (0 : ZMod 2))
541 (vacuumKineticNondegPhase.1 ((0 : ZMod 2) + 1))
542 (vacuumKineticNondegPhase.2 (0 : ZMod 2)) ≠ 0
543 have hq0 : vacuumKineticNondegPhase.1 (0 : ZMod 2) = 0 := by
544 simp [vacuumKineticNondegPhase]
545 have hq1 : vacuumKineticNondegPhase.1 ((0 : ZMod 2) + 1) = 0 := by
546 simp [vacuumKineticNondegPhase, zmod2_zero_add_one]
547 have hp0 : vacuumKineticNondegPhase.2 (0 : ZMod 2) = 1 := by
548 simp [vacuumKineticNondegPhase]
549 rw [hq0, hq1, hp0, vacuumKineticLocalHp_eq_closed]
550 -- Goal: 2 * A(0) * 1 ≠ 0
551 simp only [vacuumKineticHpClosed, vacuumKineticA]
552 norm_num
553
554def vacuumKineticStrongTarget : HKTPointSplitTargetDynStrong 2 where
555 toHKTPointSplitTargetDyn := vacuumKineticWeakTarget
556 mom_load_bearing := by
557 refine ⟨delta0, delta1, momLoadBearingWitnessPhase, ?_⟩
558 simpa [MomDyn] using hamDyn_mom_load_bearing_witness
559 advFrom_tied := by
560 intro x j
561 simpa using hamAdvFrom_eq_computed vacuumKineticWeakTarget x j
562 advTo_tied := by
563 intro x j
564 simpa using hamAdvTo_eq_computed vacuumKineticWeakTarget x j
565 kinetic_regular :=
566 ⟨vacuumKineticNondegPhase, (0 : ZMod 2), vacuumKinetic_kinetic_regular_witness⟩
567
568theorem vacuumKineticDensity_eq_localProfile (x : PhaseSpace 2) (j : ZMod 2) :
569 vacuumKineticHamDensity x j =
570 vacuumKineticLocalProfile (x.1 j) (x.1 (j + 1)) (x.2 j) := rfl
571
572/-- THEOREM. Variable-kinetic density inhabits CanonicalMom. -/
573def vacuumKineticCanonicalMomTarget : HKTPointSplitTargetDynCanonicalMom where
574 toHKTPointSplitTargetDynStrong := vacuumKineticStrongTarget
575 local_ham_profile :=
576 ⟨vacuumKineticLocalProfile, vacuumKineticLocalSmooth, vacuumKineticDensity_eq_localProfile⟩
577 structure_profile := ⟨fun q => 1 + q * q, structureDyn_eq_g⟩
578 canonical_mom := by
579 refine ⟨(1 : ℝ), by norm_num, ?_⟩
580 intro x j
581 simpa using momDynDensity_canonical x j
582
583/-! ## §3. Kill of mod-vacuum rigidity -/
584
585def coincidentPhaseKin (q p : ℝ) : PhaseSpace 2 :=
586 (fun _ => q, fun _ => p)
587
588/-- THEOREM. Mod-vacuum CanonicalMom rigidity is false. -/
589theorem not_HKTRigidityModVacuumStatementN2 :
590 ¬ HKTRigidityModVacuumStatementN2 := by
591 intro h
592 obtain ⟨cKin, cGrad, cMom, V, hcKin, _hcGrad, _hRel, hHam, _hMom⟩ :=
593 h vacuumKineticCanonicalMomTarget
594 have hAt (q p : ℝ) :
595 vacuumKineticA q * (p * p) = cKin * (p * p) + V q := by
596 have h0 := hHam (coincidentPhaseKin q p) (0 : ZMod 2)
597 simp only [vacuumKineticCanonicalMomTarget, vacuumKineticStrongTarget,
598 vacuumKineticWeakTarget, vacuumKineticHamDensity, vacuumKineticLocalProfile,
599 structureDyn, coincidentPhaseKin, zmod2_zero_add_one, sub_self, mul_zero,
600 vacuumKineticW_diag, add_zero] at h0
601 -- h0 : A q * p² = cKin p² + cGrad * _ * 0 + V q
602 linarith
603 have hV (q : ℝ) : V q = 0 := by
604 have h0 := hAt q 0
605 simp only [mul_zero, zero_add] at h0
606 exact h0.symm
607 have hA (q : ℝ) : vacuumKineticA q = cKin := by
608 have h1 := hAt q 1
609 simp only [mul_one, hV q, add_zero] at h1
610 exact h1
611 have h0 := hA 0
612 have h1 := hA 1
613 simp only [vacuumKineticA] at h0 h1
614 norm_num at h0 h1
615 exact absurd (h0.trans h1.symm) (by norm_num : (1 : ℝ) ≠ 1 / 2)
616
617/-! ## Codified decoys -/
618
619/-- Decoy: `structure_nonconstant` does not force ADM shape (counterexample witness). -/
620theorem vacuumKinetic_structure_nonconstant :
621 ¬ PhaseSpaceConstant vacuumKineticCanonicalMomTarget.structureFunction :=
622 structureDyn_not_constant
623
624/-- Decoy: the FE is `0 = 0` on the diagonal (does not force constant kinetic). -/
625theorem fe_diagonal_trivial (a p r : ℝ) :
626 vacuumKineticLocalHb a a p * vacuumKineticLocalHp a a r -
627 vacuumKineticLocalHb a a r * vacuumKineticLocalHp a a p = 0 := by
628 have h := vacuumKinetic_FE a a p r
629 simpa using h
630
631/-- The variable-kinetic counterexample fails the mod-vacuum ham-density shape. -/
632theorem vacuumKinetic_fails_modVacuum_hamShape :
633 ¬ ∃ cKin cGrad : ℝ, ∃ V : ℝ → ℝ,
634 cKin ≠ 0 ∧ cGrad ≠ 0 ∧
635 ∀ (x : PhaseSpace 2) (j : ZMod 2),
636 vacuumKineticCanonicalMomTarget.hamDensity x j =
637 cKin * (x.2 j * x.2 j) +
638 cGrad *
639 (vacuumKineticCanonicalMomTarget.structureFunction x j *
640 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
641 V (x.1 j) := by
642 rintro ⟨cKin, cGrad, V, hcKin, _hcGrad, hHam⟩
643 have hAt (q p : ℝ) :
644 vacuumKineticA q * (p * p) = cKin * (p * p) + V q := by
645 have h0 := hHam (coincidentPhaseKin q p) (0 : ZMod 2)
646 simp only [vacuumKineticCanonicalMomTarget, vacuumKineticStrongTarget,
647 vacuumKineticWeakTarget, vacuumKineticHamDensity, vacuumKineticLocalProfile,
648 structureDyn, coincidentPhaseKin, zmod2_zero_add_one, sub_self, mul_zero,
649 vacuumKineticW_diag, add_zero] at h0
650 linarith
651 have hV (q : ℝ) : V q = 0 := by
652 have hq := hAt q 0
653 simp only [mul_zero, zero_add] at hq
654 exact hq.symm
655 have h0 := hAt 0 1
656 have h1 := hAt 1 1
657 simp only [vacuumKineticA, mul_one, hV, add_zero] at h0 h1
658 norm_num at h0 h1
659 exact absurd (h0.trans h1.symm) (by norm_num : (1 : ℝ) ≠ 1 / 2)
660
661/-! ## §4. Kinetic-normalized positive terminal (C5: FTC derived) -/
662
663/-- DISCLOSED. Kinetic-sector ultralocal intensivity normalization.
664
665Intensivity `hp = 2 cKin p` plus ContDiff-2. The former assumed
666`ftc_recovery` field is discharged as `ftc_recovery_of_normalized`
667(`D-gap5-acceptance-adjudication-20260723`). -/
668structure KineticNormalizedCanonicalMom where
669 target : HKTPointSplitTargetDynCanonicalMom
670 kinetic_normalized :
671 ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (cKin : ℝ),
672 ContDiff ℝ 2 (profileMap h) ∧
673 cKin ≠ 0 ∧
674 (∀ (x : PhaseSpace 2) (j : ZMod 2),
675 target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
676 (∀ (a b p : ℝ), S.hp a b p = (2 * cKin) * p)
677
678/-- Terminal Prop: every kinetic-normalized CanonicalMom target is ADM + vacuum profile. -/
679def HKTRigidityKineticNormalizedN2 : Prop :=
680 ∀ T : KineticNormalizedCanonicalMom,
681 ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
682 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
683 (∀ (x : PhaseSpace 2) (j : ZMod 2),
684 T.target.hamDensity x j =
685 cKin * (x.2 j * x.2 j) +
686 cGrad *
687 (T.target.structureFunction x j *
688 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
689 V (x.1 j)) ∧
690 (∀ (x : PhaseSpace 2) (j : ZMod 2),
691 T.target.momDensity x j =
692 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j))
693
694private lemma localCellD_eval_p0 (h : LocalHamProfile) (S : LocalHamSmooth h)
695 (a b p : ℝ) :
696 localCellD h S (0 : ZMod 2) (fePhase a b p 0) (0, Pi.single (0 : ZMod 2) 1) =
697 S.hp a b p := by
698 simp only [localCellD, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
699 coordQ_apply, coordP_apply, smul_eq_mul, fePhase, zmod2_zero_add_one]
700 simp [Pi.single_eq_same]
701
702private lemma localCellD_eval_b0 (h : LocalHamProfile) (S : LocalHamSmooth h)
703 (a b p : ℝ) :
704 localCellD h S (0 : ZMod 2) (fePhase a b p 0)
705 (Pi.single (1 : ZMod 2) 1, 0) =
706 S.hb a b p := by
707 simp only [localCellD, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
708 coordQ_apply, coordP_apply, smul_eq_mul, fePhase, zmod2_zero_add_one]
709 simp [Pi.single_eq_same, Pi.single_eq_of_ne (by decide : (0 : ZMod 2) ≠ 1)]
710
711/-- Frechet uniqueness: slot `hp` is independent of the LocalHamSmooth witness. -/
712theorem LocalHamSmooth_hp_unique (h : LocalHamProfile)
713 (S₁ S₂ : LocalHamSmooth h) (a b p : ℝ) :
714 S₁.hp a b p = S₂.hp a b p := by
715 let x : PhaseSpace 2 := fePhase a b p 0
716 have hL :=
717 HasFDerivAt.unique (hasFDerivAt_localCell h S₁ (0 : ZMod 2) x)
718 (hasFDerivAt_localCell h S₂ (0 : ZMod 2) x)
719 have heval :=
720 congrArg (fun L : PhaseSpace 2 →L[ℝ] ℝ => L (0, Pi.single (0 : ZMod 2) 1)) hL
721 simpa [localCellD_eval_p0 h S₁ a b p, localCellD_eval_p0 h S₂ a b p, x] using heval
722
723/-- Frechet uniqueness: slot `hb` is independent of the LocalHamSmooth witness. -/
724theorem LocalHamSmooth_hb_unique (h : LocalHamProfile)
725 (S₁ S₂ : LocalHamSmooth h) (a b p : ℝ) :
726 S₁.hb a b p = S₂.hb a b p := by
727 let x : PhaseSpace 2 := fePhase a b p 0
728 have hL :=
729 HasFDerivAt.unique (hasFDerivAt_localCell h S₁ (0 : ZMod 2) x)
730 (hasFDerivAt_localCell h S₂ (0 : ZMod 2) x)
731 have heval :=
732 congrArg (fun L : PhaseSpace 2 →L[ℝ] ℝ => L (Pi.single (1 : ZMod 2) 1, 0)) hL
733 simpa [localCellD_eval_b0 h S₁ a b p, localCellD_eval_b0 h S₂ a b p, x] using heval
734
735/-! ### ContDiff-2 slot derivatives ↔ LocalHamSmooth coefficients -/
736
737private theorem hasDerivAt_profileMap_p
738 (h : LocalHamProfile) (hcd : ContDiff ℝ 2 (profileMap h)) (a b p : ℝ) :
739 HasDerivAt (fun t => h a b t)
740 (fderiv ℝ (profileMap h) (a, b, p) (0, 0, 1)) p := by
741 have hF :=
742 ((hcd.of_le (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
743 (a, b, p)).hasFDerivAt
744 have hφ : HasDerivAt (fun t : ℝ => ((a, b, t) : ℝ × ℝ × ℝ)) (0, 0, 1) p :=
745 (hasDerivAt_const p a).prodMk ((hasDerivAt_const p b).prodMk (hasDerivAt_id p))
746 have hline := hF.comp_hasDerivAt p hφ
747 simpa [profileMap, Function.comp_def] using hline
748
749private theorem hasDerivAt_profileMap_b
750 (h : LocalHamProfile) (hcd : ContDiff ℝ 2 (profileMap h)) (a b p : ℝ) :
751 HasDerivAt (fun s => h a s p)
752 (fderiv ℝ (profileMap h) (a, b, p) (0, 1, 0)) b := by
753 have hF :=
754 ((hcd.of_le (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
755 (a, b, p)).hasFDerivAt
756 have hφ : HasDerivAt (fun s : ℝ => ((a, s, p) : ℝ × ℝ × ℝ)) (0, 1, 0) b :=
757 (hasDerivAt_const b a).prodMk ((hasDerivAt_id b).prodMk (hasDerivAt_const b p))
758 have hline := hF.comp_hasDerivAt b hφ
759 simpa [profileMap, Function.comp_def] using hline
760
761private def cellCoords0 (y : PhaseSpace 2) : ℝ × ℝ × ℝ :=
762 (y.1 (0 : ZMod 2), y.1 (1 : ZMod 2), y.2 (0 : ZMod 2))
763
764private def cellCoords0D : PhaseSpace 2 →L[ℝ] ℝ × ℝ × ℝ :=
765 (coordQ (0 : ZMod 2)).prod ((coordQ (1 : ZMod 2)).prod (coordP (0 : ZMod 2)))
766
767private lemma hasFDerivAt_cellCoords0 (x : PhaseSpace 2) :
768 HasFDerivAt cellCoords0 cellCoords0D x :=
769 (hasFDerivAt_coord_fst (0 : ZMod 2) x).prodMk
770 ((hasFDerivAt_coord_fst (1 : ZMod 2) x).prodMk
771 (hasFDerivAt_coord_snd (0 : ZMod 2) x))
772
773private theorem cellCoords0_fePhase (a b p : ℝ) :
774 cellCoords0 (fePhase a b p 0) = (a, b, p) := by
775 simp [cellCoords0, fePhase]
776
777private theorem LocalHamSmooth_hp_eq_fderiv
778 (h : LocalHamProfile) (S : LocalHamSmooth h)
779 (hcd : ContDiff ℝ 2 (profileMap h)) (a b p : ℝ) :
780 S.hp a b p = fderiv ℝ (profileMap h) (a, b, p) (0, 0, 1) := by
781 let x : PhaseSpace 2 := fePhase a b p 0
782 have hx : cellCoords0 x = (a, b, p) := cellCoords0_fePhase a b p
783 have hS := hasFDerivAt_localCell h S (0 : ZMod 2) x
784 have hProf :=
785 ((hcd.of_le (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
786 (cellCoords0 x)).hasFDerivAt
787 have hcomp := hProf.comp x (hasFDerivAt_cellCoords0 x)
788 have hfun :
789 (fun y : PhaseSpace 2 => h (y.1 (0 : ZMod 2)) (y.1 (1 : ZMod 2)) (y.2 (0 : ZMod 2))) =
790 profileMap h ∘ cellCoords0 := rfl
791 have hCD : HasFDerivAt
792 (fun y : PhaseSpace 2 => h (y.1 (0 : ZMod 2)) (y.1 (1 : ZMod 2)) (y.2 (0 : ZMod 2)))
793 (fderiv ℝ (profileMap h) (cellCoords0 x) ∘L cellCoords0D) x := by
794 simpa [hfun] using hcomp
795 have hUniq := HasFDerivAt.unique hS hCD
796 have heval :=
797 congrArg (fun L : PhaseSpace 2 →L[ℝ] ℝ => L (0, Pi.single (0 : ZMod 2) 1)) hUniq
798 have hL : localCellD h S (0 : ZMod 2) x (0, Pi.single (0 : ZMod 2) 1) = S.hp a b p :=
799 localCellD_eval_p0 h S a b p
800 have hR :
801 (fderiv ℝ (profileMap h) (cellCoords0 x) ∘L cellCoords0D)
802 (0, Pi.single (0 : ZMod 2) 1) =
803 fderiv ℝ (profileMap h) (a, b, p) (0, 0, 1) := by
804 simp only [ContinuousLinearMap.comp_apply, cellCoords0D, ContinuousLinearMap.prod_apply,
805 coordQ_apply, coordP_apply, Pi.single_eq_same, Pi.zero_apply, hx]
806 have hLR :
807 S.hp a b p =
808 (fderiv ℝ (profileMap h) (cellCoords0 x) ∘L cellCoords0D)
809 (0, Pi.single (0 : ZMod 2) 1) := by
810 simpa [hL] using heval
811 exact hLR.trans hR
812
813private theorem LocalHamSmooth_hb_eq_fderiv
814 (h : LocalHamProfile) (S : LocalHamSmooth h)
815 (hcd : ContDiff ℝ 2 (profileMap h)) (a b p : ℝ) :
816 S.hb a b p = fderiv ℝ (profileMap h) (a, b, p) (0, 1, 0) := by
817 let x : PhaseSpace 2 := fePhase a b p 0
818 have hx : cellCoords0 x = (a, b, p) := cellCoords0_fePhase a b p
819 have hS := hasFDerivAt_localCell h S (0 : ZMod 2) x
820 have hProf :=
821 ((hcd.of_le (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
822 (cellCoords0 x)).hasFDerivAt
823 have hcomp := hProf.comp x (hasFDerivAt_cellCoords0 x)
824 have hfun :
825 (fun y : PhaseSpace 2 => h (y.1 (0 : ZMod 2)) (y.1 (1 : ZMod 2)) (y.2 (0 : ZMod 2))) =
826 profileMap h ∘ cellCoords0 := rfl
827 have hCD : HasFDerivAt
828 (fun y : PhaseSpace 2 => h (y.1 (0 : ZMod 2)) (y.1 (1 : ZMod 2)) (y.2 (0 : ZMod 2)))
829 (fderiv ℝ (profileMap h) (cellCoords0 x) ∘L cellCoords0D) x := by
830 simpa [hfun] using hcomp
831 have hUniq := HasFDerivAt.unique hS hCD
832 have heval :=
833 congrArg (fun L : PhaseSpace 2 →L[ℝ] ℝ => L (Pi.single (1 : ZMod 2) 1, 0)) hUniq
834 have hL : localCellD h S (0 : ZMod 2) x (Pi.single (1 : ZMod 2) 1, 0) = S.hb a b p :=
835 localCellD_eval_b0 h S a b p
836 have hR :
837 (fderiv ℝ (profileMap h) (cellCoords0 x) ∘L cellCoords0D)
838 (Pi.single (1 : ZMod 2) 1, 0) =
839 fderiv ℝ (profileMap h) (a, b, p) (0, 1, 0) := by
840 simp only [ContinuousLinearMap.comp_apply, cellCoords0D, ContinuousLinearMap.prod_apply,
841 coordQ_apply, coordP_apply, Pi.single_eq_same, Pi.zero_apply,
842 Pi.single_eq_of_ne (by decide : (0 : ZMod 2) ≠ 1), hx]
843 have hLR :
844 S.hb a b p =
845 (fderiv ℝ (profileMap h) (cellCoords0 x) ∘L cellCoords0D)
846 (Pi.single (1 : ZMod 2) 1, 0) := by
847 simpa [hL] using heval
848 exact hLR.trans hR
849
850theorem hasDerivAt_hp_of_normalized
851 (h : LocalHamProfile) (S : LocalHamSmooth h)
852 (hcd : ContDiff ℝ 2 (profileMap h)) (a b p : ℝ) :
853 HasDerivAt (fun t => h a b t) (S.hp a b p) p := by
854 have hline := hasDerivAt_profileMap_p h hcd a b p
855 rwa [← LocalHamSmooth_hp_eq_fderiv h S hcd a b p] at hline
856
857theorem hasDerivAt_hb_of_normalized
858 (h : LocalHamProfile) (S : LocalHamSmooth h)
859 (hcd : ContDiff ℝ 2 (profileMap h)) (a b p : ℝ) :
860 HasDerivAt (fun s => h a s p) (S.hb a b p) b := by
861 have hline := hasDerivAt_profileMap_b h hcd a b p
862 rwa [← LocalHamSmooth_hb_eq_fderiv h S hcd a b p] at hline
863
864/-! ### (i) Kinetic split from intensivity -/
865
866/-- Intensivity + ContDiff-2 ⇒ `h(a,b,p) = cKin p² + h(a,b,0)`. -/
867theorem kinetic_split_of_intensivity
868 (h : LocalHamProfile) (S : LocalHamSmooth h) (cKin : ℝ)
869 (hcd : ContDiff ℝ 2 (profileMap h))
870 (hHp : ∀ (a b p : ℝ), S.hp a b p = (2 * cKin) * p)
871 (a b p : ℝ) :
872 h a b p = cKin * (p * p) + h a b 0 := by
873 let F : ℝ → ℝ := fun t => h a b t - cKin * (t * t)
874 have hFderiv (t : ℝ) : HasDerivAt F 0 t := by
875 have h1 := hasDerivAt_hp_of_normalized h S hcd a b t
876 have hpow : HasDerivAt (fun u : ℝ => u ^ 2) ((2 : ℝ) * t) t := by
877 simpa using (hasDerivAt_id t).pow 2
878 have h2pow : HasDerivAt (fun u : ℝ => cKin * u ^ 2) ((2 * cKin) * t) t := by
879 have h2' := hpow.const_mul cKin
880 convert h2' using 1; ring
881 have h2 : HasDerivAt (fun u : ℝ => cKin * (u * u)) ((2 * cKin) * t) t := by
882 have heq : (fun u : ℝ => cKin * (u * u)) = fun u => cKin * u ^ 2 := by
883 funext u; rw [pow_two]
884 simpa [heq] using h2pow
885 have hsub : HasDerivAt F (S.hp a b t - (2 * cKin) * t) t := h1.sub h2
886 simpa [hHp a b t, sub_self] using hsub
887 have hdiff : Differentiable ℝ F := fun t => (hFderiv t).differentiableAt
888 have hconst :=
889 is_const_of_deriv_eq_zero hdiff (fun t => (hFderiv t).deriv) p 0
890 have hF0 : F 0 = h a b 0 := by simp [F]
891 have hFp : F p = h a b p - cKin * (p * p) := rfl
892 linarith [hconst, hF0, hFp]
893
894/-! ### (ii) Gradient recovery from FE + intensivity -/
895
896/-- FE at `(p,r)=(0,1)` + intensivity ⇒ diagonal `hb` shape. -/
897theorem hb0_of_intensivity_FE
898 (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom cKin : ℝ)
899 (hcKin : cKin ≠ 0)
900 (hHp : ∀ (a b p : ℝ), S.hp a b p = (2 * cKin) * p)
901 (hFE : ∀ (a b p r : ℝ),
902 S.hb a b p * S.hp b a r - S.hb b a r * S.hp a b p =
903 cMom * (b - a) * (g a * r + g b * p))
904 (a b : ℝ) :
905 S.hb a b 0 = (cMom / (2 * cKin)) * (g a * (b - a)) := by
906 have h0 := hFE a b 0 1
907 have hHpba : S.hp b a 1 = 2 * cKin := by simpa using hHp b a 1
908 have hHpab : S.hp a b 0 = 0 := by simpa using hHp a b 0
909 have h0' : S.hb a b 0 * (2 * cKin) = cMom * (b - a) * g a := by
910 simpa [hHpba, hHpab, mul_zero, sub_zero, mul_one, add_zero] using h0
911 have h2 : (2 : ℝ) * cKin ≠ 0 := mul_ne_zero (by norm_num) hcKin
912 calc
913 S.hb a b 0 = (S.hb a b 0 * (2 * cKin)) / (2 * cKin) := by field_simp [h2]
914 _ = (cMom * (b - a) * g a) / (2 * cKin) := by rw [h0']
915 _ = (cMom / (2 * cKin)) * (g a * (b - a)) := by ring
916
917/-- Gradient-sector FTC: integrate the FE-forced `hb` from the diagonal. -/
918theorem gradient_recovery_of_intensivity
919 (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom cKin : ℝ)
920 (hcd : ContDiff ℝ 2 (profileMap h)) (hcKin : cKin ≠ 0)
921 (hHp : ∀ (a b p : ℝ), S.hp a b p = (2 * cKin) * p)
922 (hFE : ∀ (a b p r : ℝ),
923 S.hb a b p * S.hp b a r - S.hb b a r * S.hp a b p =
924 cMom * (b - a) * (g a * r + g b * p))
925 (a b : ℝ) :
926 h a b 0 =
927 h a a 0 + (cMom / (4 * cKin)) * (g a * ((b - a) * (b - a))) := by
928 let F : ℝ → ℝ := fun s => h a s 0
929 let Gpow : ℝ → ℝ := fun s =>
930 h a a 0 + (cMom / (4 * cKin)) * (g a * (s - a) ^ 2)
931 have hHb0 (s : ℝ) :
932 S.hb a s 0 = (cMom / (2 * cKin)) * (g a * (s - a)) :=
933 hb0_of_intensivity_FE h S g cMom cKin hcKin hHp hFE a s
934 have hFderiv (s : ℝ) : HasDerivAt F (S.hb a s 0) s :=
935 hasDerivAt_hb_of_normalized h S hcd a s 0
936 have hGderiv (s : ℝ) :
937 HasDerivAt Gpow ((cMom / (2 * cKin)) * (g a * (s - a))) s := by
938 have hd : HasDerivAt (fun s : ℝ => s - a) (1 : ℝ) s :=
939 (hasDerivAt_id s).sub_const a
940 have hsq : HasDerivAt (fun s : ℝ => (s - a) ^ 2) (2 * (s - a)) s := by
941 convert hd.pow 2 using 1 <;> ring
942 let c : ℝ := h a a 0
943 let k : ℝ := cMom / (4 * cKin)
944 have hga : HasDerivAt (fun s : ℝ => g a * (s - a) ^ 2)
945 (g a * (2 * (s - a))) s := by
946 convert (hasDerivAt_const s (g a)).mul hsq using 1 <;> ring
947 have hterm : HasDerivAt (fun s : ℝ => k * (g a * (s - a) ^ 2))
948 (k * (g a * (2 * (s - a)))) s := by
949 convert hga.const_mul k using 1 <;> ring
950 have hsum : HasDerivAt (fun s : ℝ => c + k * (g a * (s - a) ^ 2))
951 (0 + k * (g a * (2 * (s - a)))) s :=
952 (hasDerivAt_const s c).add hterm
953 have hfun : Gpow = fun s => c + k * (g a * (s - a) ^ 2) := rfl
954 rw [hfun]
955 have hrw : 0 + k * (g a * (2 * (s - a))) =
956 (cMom / (2 * cKin)) * (g a * (s - a)) := by
957 change 0 + (cMom / (4 * cKin)) * (g a * (2 * (s - a))) =
958 (cMom / (2 * cKin)) * (g a * (s - a))
959 ring
960 exact hrw ▸ hsum
961 have hDiff (s : ℝ) : HasDerivAt (fun u => F u - Gpow u) 0 s := by
962 have hsub : HasDerivAt (fun u => F u - Gpow u)
963 (S.hb a s 0 - (cMom / (2 * cKin)) * (g a * (s - a))) s :=
964 (hFderiv s).sub (hGderiv s)
965 simpa [hHb0 s, sub_self] using hsub
966 have hdiff : Differentiable ℝ (fun u => F u - Gpow u) :=
967 fun s => (hDiff s).differentiableAt
968 have hconst :=
969 is_const_of_deriv_eq_zero hdiff (fun s => (hDiff s).deriv) b a
970 have hFa : F a - Gpow a = 0 := by
971 simp only [F, Gpow, sub_self, pow_two, mul_zero, add_zero]
972 have hFb : F b - Gpow b = F a - Gpow a := hconst
973 have hEq : F b = Gpow b := by linarith [hFb, hFa]
974 -- F b = h a b 0 and Gpow b = h a a 0 + (cMom/(4 cKin)) g a (b-a)^2
975 change h a b 0 = Gpow b at hEq
976 simpa [Gpow, pow_two] using hEq
977
978/-- FE for an explicit local-profile witness (same body as
979`profiled_ham_ham_alternating_FE`, fixed `h`/`S`/`g`/`cMom`). -/
980theorem alternating_FE_of_profile
981 (T : HKTPointSplitTargetDynCanonicalMom)
982 (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom : ℝ)
983 (hHam : ∀ (x : PhaseSpace 2) (j : ZMod 2),
984 T.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j))
985 (hG : ∀ (x : PhaseSpace 2) (j : ZMod 2), T.structureFunction x j = g (x.1 j))
986 (hMom : ∀ (x : PhaseSpace 2) (j : ZMod 2),
987 T.momDensity x j = cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j))
988 (a b p r : ℝ) :
989 S.hb a b p * S.hp b a r - S.hb b a r * S.hp a b p =
990 cMom * (b - a) * (g a * r + g b * p) := by
991 let x : PhaseSpace 2 := fePhase a b p r
992 have hx0 : x.1 (0 : ZMod 2) = a := by simp [x, fePhase]
993 have hx1 : x.1 (1 : ZMod 2) = b := by simp [x, fePhase]
994 have hp0 : x.2 (0 : ZMod 2) = p := by simp [x, fePhase]
995 have hp1 : x.2 (1 : ZMod 2) = r := by simp [x, fePhase]
996 have hEq0 := hamDensity_smear_eq_LocalHamFromProfile T h hHam delta0
997 have hEq1 := hamDensity_smear_eq_LocalHamFromProfile T h hHam delta1
998 have hProf := local_profile_ham_ham_form h S delta0 delta1 x
999 have hTarget := T.ham_ham delta0 delta1 x
1000 have hProf' :
1001 bracket (LocalHamFromProfile h delta0) (LocalHamFromProfile h delta1) x =
1002 localHamHamCoefficient h S x (0 : ZMod 2) -
1003 localHamHamCoefficient h S x (1 : ZMod 2) :=
1004 hProf.trans (localHamHamCoefficient_delta01 h S x)
1005 have hTarget' :
1006 bracket (fun y => ∑ j : ZMod 2, delta0 j * T.hamDensity y j)
1007 (fun y => ∑ j : ZMod 2, delta1 j * T.hamDensity y j) x =
1008 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) -
1009 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) :=
1010 hTarget.trans (structure_mom_delta01 T.structureFunction T.momDensity x)
1011 have hBracket :
1012 bracket (LocalHamFromProfile h delta0) (LocalHamFromProfile h delta1) x =
1013 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) -
1014 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) := by
1015 simpa [hEq0, hEq1] using hTarget'
1016 have hAlt :
1017 localHamHamCoefficient h S x (0 : ZMod 2) -
1018 localHamHamCoefficient h S x (1 : ZMod 2) =
1019 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) -
1020 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) :=
1021 hProf'.symm.trans hBracket
1022 have hC0 :
1023 localHamHamCoefficient h S x (0 : ZMod 2) =
1024 S.hb a b p * S.hp b a r := by
1025 simp only [localHamHamCoefficient, zmod2_zero_add_one, zmod2_zero_add_two]
1026 rw [hx0, hx1, hp0, hp1]
1027 have hC1 :
1028 localHamHamCoefficient h S x (1 : ZMod 2) =
1029 S.hb b a r * S.hp a b p := by
1030 simp only [localHamHamCoefficient, zmod2_one_add_one, zmod2_one_add_two]
1031 rw [hx0, hx1, hp0, hp1]
1032 have hR0 :
1033 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) =
1034 g a * (cMom * r * (b - a)) := by
1035 rw [hG x (0 : ZMod 2), hMom x (0 : ZMod 2), zmod2_zero_add_one, hx0, hx1, hp1]
1036 have hR1 :
1037 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) =
1038 g b * (cMom * p * (a - b)) := by
1039 rw [hG x (1 : ZMod 2), hMom x (1 : ZMod 2), zmod2_one_add_one, hx0, hx1, hp0]
1040 have hEq := hAlt
1041 rw [hC0, hC1, hR0, hR1] at hEq
1042 have hR :
1043 g a * (cMom * r * (b - a)) - g b * (cMom * p * (a - b)) =
1044 cMom * (b - a) * (g a * r + g b * p) := by ring
1045 exact hEq.trans hR
1046
1047/-- THEOREM. FTC package derived from intensivity + ContDiff-2 + CanonicalMom FE.
1048No assumed conclusion-shaped class field. -/
1049theorem ftc_recovery_of_normalized (T : KineticNormalizedCanonicalMom) :
1050 ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (cKin : ℝ) (g : ℝ → ℝ)
1051 (cMom : ℝ),
1052 cKin ≠ 0 ∧ cMom ≠ 0 ∧
1053 (∀ (x : PhaseSpace 2) (j : ZMod 2),
1054 T.target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
1055 (∀ (x : PhaseSpace 2) (j : ZMod 2),
1056 T.target.structureFunction x j = g (x.1 j)) ∧
1057 (∀ (x : PhaseSpace 2) (j : ZMod 2),
1058 T.target.momDensity x j = cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) ∧
1059 (∀ (a b p : ℝ), S.hp a b p = (2 * cKin) * p) ∧
1060 (∀ (a b p r : ℝ),
1061 S.hb a b p * S.hp b a r - S.hb b a r * S.hp a b p =
1062 cMom * (b - a) * (g a * r + g b * p)) ∧
1063 (∀ (a b p : ℝ), h a b p = cKin * (p * p) + h a b 0) ∧
1064 (∀ (a b : ℝ),
1065 h a b 0 =
1066 h a a 0 + (cMom / (4 * cKin)) * (g a * ((b - a) * (b - a)))) := by
1067 obtain ⟨h, S, cKin, hcd, hcKin, hHam, hHp⟩ := T.kinetic_normalized
1068 obtain ⟨g, hG⟩ := T.target.structure_profile
1069 obtain ⟨cMom, hcMom, hMom⟩ := T.target.canonical_mom
1070 refine ⟨h, S, cKin, g, cMom, hcKin, hcMom, hHam, hG, hMom, hHp, ?_, ?_, ?_⟩
1071 · exact alternating_FE_of_profile T.target h S g cMom hHam hG hMom
1072 · intro a b p
1073 exact kinetic_split_of_intensivity h S cKin hcd hHp a b p
1074 · intro a b
1075 exact gradient_recovery_of_intensivity h S g cMom cKin hcd hcKin hHp
1076 (alternating_FE_of_profile T.target h S g cMom hHam hG hMom) a b
1077
1078/-- THEOREM. Kinetic-normalized CanonicalMom rigidity at `n = 2`. -/
1079theorem HKTRigidityKineticNormalizedN2_holds : HKTRigidityKineticNormalizedN2 := by
1080 intro T
1081 obtain ⟨h, S, cKin, g, cMom, hcKin, hcMom, hHam, hG, hMom, hHp, _hFE, hSplit, hInt⟩ :=
1082 ftc_recovery_of_normalized T
1083 refine ⟨cKin, cMom / (4 * cKin), cMom, fun a => h a a 0, hcKin,
1084 div_ne_zero hcMom (mul_ne_zero (by norm_num) hcKin), ?_, ?_, hMom⟩
1085 · field_simp [hcKin]
1086 · intro x j
1087 have h1 := hHam x j
1088 have h2 := hG x j
1089 have h3 := hSplit (x.1 j) (x.1 (j + 1)) (x.2 j)
1090 have h4 := hInt (x.1 j) (x.1 (j + 1))
1091 calc
1092 T.target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j) := h1
1093 _ = cKin * (x.2 j * x.2 j) + h (x.1 j) (x.1 (j + 1)) 0 := h3
1094 _ = cKin * (x.2 j * x.2 j) +
1095 (h (x.1 j) (x.1 j) 0 +
1096 (cMom / (4 * cKin)) *
1097 (g (x.1 j) *
1098 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)))) := by
1099 rw [h4]
1100 _ = cKin * (x.2 j * x.2 j) +
1101 (cMom / (4 * cKin)) *
1102 (T.target.structureFunction x j *
1103 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
1104 h (x.1 j) (x.1 j) 0 := by
1105 rw [h2]; ring
1106
1107/-! ### Anchors -/
1108
1109def hamDynKineticNormalized : KineticNormalizedCanonicalMom where
1110 target := hamDynPointSplitTargetCanonicalMom
1111 kinetic_normalized := by
1112 refine ⟨hamDynLocalProfile, hamDynLocalSmooth, (1 / 2 : ℝ),
1113 hamDynLocalProfile_contDiff2, by norm_num, hamDynDensity_eq_localProfile, ?_⟩
1114 intro a b p
1115 change hamDynLocalHp a b p = (2 * (1 / 2 : ℝ)) * p
1116 simp only [hamDynLocalHp]; ring
1117
1118theorem hamDyn_satisfies_kineticNormalized :
1119 ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
1120 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
1121 (∀ (x : PhaseSpace 2) (j : ZMod 2),
1122 hamDynKineticNormalized.target.hamDensity x j =
1123 cKin * (x.2 j * x.2 j) +
1124 cGrad *
1125 (hamDynKineticNormalized.target.structureFunction x j *
1126 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
1127 V (x.1 j)) ∧
1128 (∀ (x : PhaseSpace 2) (j : ZMod 2),
1129 hamDynKineticNormalized.target.momDensity x j =
1130 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
1131 HKTRigidityKineticNormalizedN2_holds hamDynKineticNormalized
1132
1133/-- Load-bearing: variable-kinetic counterexample is excluded (hp not globally
1134of the form `2 cKin p`). -/
1135theorem vacuumKinetic_not_kineticNormalized :
1136 ¬ ∃ T : KineticNormalizedCanonicalMom,
1137 T.target = vacuumKineticCanonicalMomTarget := by
1138 rintro ⟨T, hEq⟩
1139 obtain ⟨h, S, cKin, _hcd, hcKin, hHam, hHp⟩ := T.kinetic_normalized
1140 have hProf : h = vacuumKineticLocalProfile := by
1141 funext a b p
1142 have hT :
1143 T.target.hamDensity (fePhase a b p 0) (0 : ZMod 2) =
1144 vacuumKineticCanonicalMomTarget.hamDensity (fePhase a b p 0) (0 : ZMod 2) :=
1145 congrArg (fun U : HKTPointSplitTargetDynCanonicalMom =>
1146 U.hamDensity (fePhase a b p 0) (0 : ZMod 2)) hEq
1147 have hL := hHam (fePhase a b p 0) (0 : ZMod 2)
1148 have hR :
1149 vacuumKineticCanonicalMomTarget.hamDensity (fePhase a b p 0) (0 : ZMod 2) =
1150 vacuumKineticLocalProfile a b p := by
1151 simp [vacuumKineticCanonicalMomTarget, vacuumKineticStrongTarget,
1152 vacuumKineticWeakTarget, vacuumKineticHamDensity, fePhase, zmod2_zero_add_one]
1153 exact (hL.symm.trans hT).trans hR
1154 cases hProf
1155 have hUniq (a b p : ℝ) :
1156 S.hp a b p = vacuumKineticLocalSmooth.hp a b p :=
1157 LocalHamSmooth_hp_unique vacuumKineticLocalProfile S vacuumKineticLocalSmooth a b p
1158 have hA (a : ℝ) : vacuumKineticA a = cKin := by
1159 have hL : S.hp a 0 1 = (2 * cKin) * (1 : ℝ) := hHp a 0 1
1160 have hR : S.hp a 0 1 = vacuumKineticHpClosed a 1 :=
1161 (hUniq a 0 1).trans (by
1162 change vacuumKineticLocalHp a 0 1 = vacuumKineticHpClosed a 1
1163 exact vacuumKineticLocalHp_eq_closed a 0 1)
1164 simp only [mul_one, vacuumKineticHpClosed] at hL hR
1165 linarith
1166 have h0 := hA 0
1167 have h1 := hA 1
1168 simp only [vacuumKineticA] at h0 h1
1169 norm_num at h0 h1
1170 exact absurd (h0.trans h1.symm) (by norm_num : (1 : ℝ) ≠ 1 / 2)
1171
1172/-! ## §5. Status (C5; gap5 flipped via Gap5ConstraintCloseStatus) -/
1173
1174structure HKTKineticNormalizedRigidityStatus where
1175 modVacuumRigidityKilled : Bool
1176 kineticNormalizedRigidityClosed : Bool
1177 ftcRecoveryDerived : Bool
1178 gap5ConstraintRecovery : Bool
1179
1180def hktKineticNormalizedRigidityStatus : HKTKineticNormalizedRigidityStatus where
1181 modVacuumRigidityKilled := true
1182 kineticNormalizedRigidityClosed := true
1183 ftcRecoveryDerived := true
1184 gap5ConstraintRecovery := true
1185
1186theorem hktKineticNormalizedRigidityStatus_flags :
1187 hktKineticNormalizedRigidityStatus.modVacuumRigidityKilled = true ∧
1188 hktKineticNormalizedRigidityStatus.kineticNormalizedRigidityClosed = true ∧
1189 hktKineticNormalizedRigidityStatus.ftcRecoveryDerived = true ∧
1190 hktKineticNormalizedRigidityStatus.gap5ConstraintRecovery = true ∧
1191 fullTheoryBenchmarks.gap5_constraint_recovery = true ∧
1192 ¬ HKTRigidityModVacuumStatementN2 ∧
1193 HKTRigidityKineticNormalizedN2 :=
1194 ⟨rfl, rfl, rfl, rfl, rfl, not_HKTRigidityModVacuumStatementN2,
1195 HKTRigidityKineticNormalizedN2_holds⟩
1196
1197#print axioms not_HKTRigidityModVacuumStatementN2
1198#print axioms ftc_recovery_of_normalized
1199#print axioms HKTRigidityKineticNormalizedN2_holds
1200#print axioms hamDyn_satisfies_kineticNormalized
1201#print axioms vacuumKinetic_not_kineticNormalized
1202#print axioms kinetic_split_of_intensivity
1203#print axioms gradient_recovery_of_intensivity
1204
1205end
1206end HKTKineticNormalizedRigidity
1207end SevenGaps
1208end Gravity
1209end IndisputableMonolith
1210