IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill
IndisputableMonolith/Gravity/SevenGaps/HKTVacuumSectorKill.lean · 627 lines · 44 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE
2import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
3
4/-!
5# Wave C3 gap5: vacuum-sector kill of unconditioned CanonicalMom rigidity
6
7Binding: `D-qg-hkt-rigidity-gauge-scope-20260723` (Codex cross-family
8adjudication 2026-07-23; fork resolved as branch A).
9
10The unconditioned Prop `HKTRigidityStatementPointSplitDynN2Canonical` is
11FALSE. Killer: vacuum-shift density at `n = 2`
12
13 h(a,b,p) = (1/2)·(p² + (1+a²)(b-a)²) + a²
14 g(a) = 1 + a²
15 mⱼ = π_{j+1}·(q_{j+1}-qⱼ), cMom = 1
16
17The ham_ham alternating FE is blind to the zero-gradient vacuum term `a²`;
18tied advection slots record the computed Mom–Ham brackets (contentless as a
19constraint); `mom_mom`, `mom_load_bearing`, `kinetic_regular`, and
20`structure_nonconstant` hold as for HamDyn. The rigidity conclusion forces a
21constant vacuum `cVac`, while this density evaluates at coincident
22configurations to `q²` (nonconstant).
23
24`sqrtAffineProfile` does **not** lift to CanonicalMom (its FE forces `g`
25constant, violating `structure_nonconstant`); it is not the kill.
26
27Repaired terminal (DEFINED only): `HKTRigidityModVacuumStatementN2`.
28Whether `structure_nonconstant` + FE forces the kinetic/gradient sectors
29remains OPEN mathematics.
30
31Do NOT flip `gap5_constraint_recovery`.
32-/
33
34namespace IndisputableMonolith
35namespace Gravity
36namespace SevenGaps
37namespace HKTVacuumSectorKill
38
39open HypersurfaceDeformation DynamicStructureBracket DynamicStructureFunctionBlocker
40open HKTPointSplitTarget HKTPointSplitStrong HKTLocalFunctionalEquation
41open HKTCanonicalMomTarget HKTCanonicalMomRigidity FullTheoryLedger
42
43noncomputable section
44
45open Finset
46
47private lemma zmod2_zero_add_one : (0 : ZMod 2) + 1 = 1 := by decide
48private lemma zmod2_one_add_one : (1 : ZMod 2) + 1 = 0 := by decide
49
50/-! ## Vacuum-shift densities -/
51
52/-- MODEL. HamDyn density plus vacuum shift `qⱼ²`. -/
53def vacuumShiftHamDensity (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
54 hamDynDensity x j + x.1 j * x.1 j
55
56/-- Local profile: `h(a,b,p) = (1/2)·(p² + (1+a²)(b-a)²) + a²`. -/
57def vacuumShiftLocalProfile : LocalHamProfile :=
58 fun a b p => hamDynLocalProfile a b p + a * a
59
60def vacuumShiftLocalHa : LocalHamProfile :=
61 fun a b p => hamDynLocalHa a b p + (2 : ℝ) * a
62
63def vacuumShiftLocalHb : LocalHamProfile := hamDynLocalHb
64
65def vacuumShiftLocalHp : LocalHamProfile := hamDynLocalHp
66
67/-- Source advection unchanged by the vacuum shift (Vac has vanishing π-partial). -/
68def vacuumShiftHamAdvFrom (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
69 hamDynAdvFrom x j
70
71/-- Target advection: HamDyn slot plus vacuum correction
72`-2 · (q_{j+1}-qⱼ) · q_{j+1}`. -/
73def vacuumShiftHamAdvTo (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
74 hamDynAdvTo x j - (2 : ℝ) * (x.1 (j + 1) - x.1 j) * x.1 (j + 1)
75
76theorem vacuumShiftDensity_eq_localProfile (x : PhaseSpace 2) (j : ZMod 2) :
77 vacuumShiftHamDensity x j =
78 vacuumShiftLocalProfile (x.1 j) (x.1 (j + 1)) (x.2 j) := by
79 unfold vacuumShiftHamDensity vacuumShiftLocalProfile hamDynDensity hamDynLocalProfile
80 ring
81
82/-! ## Vacuum smear and Frechet data -/
83
84def VacSmear (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
85 ∑ j : ZMod 2, N j * (x.1 j * x.1 j)
86
87def VacSmearD (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
88 ∑ j : ZMod 2, (N j) • (x.1 j • coordQ j + x.1 j • coordQ j)
89
90lemma hasFDerivAt_VacSmear (N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
91 HasFDerivAt (VacSmear N) (VacSmearD N x) x := by
92 unfold VacSmear VacSmearD
93 exact HasFDerivAt.fun_sum fun j _ =>
94 ((hasFDerivAt_coord_fst j x).mul (hasFDerivAt_coord_fst j x)).const_mul (N j)
95
96theorem pderivQ_VacSmear (N : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
97 pderivQ (VacSmear N) k x = (2 : ℝ) * N k * x.1 k := by
98 rw [pderivQ, (hasFDerivAt_VacSmear N x).fderiv, VacSmearD,
99 ContinuousLinearMap.sum_apply]
100 have step : ∀ j : ZMod 2,
101 (((N j) • (x.1 j • coordQ j + x.1 j • coordQ j) : PhaseSpace 2 →L[ℝ] ℝ)
102 ((Pi.single k 1, 0) : PhaseSpace 2))
103 = ((2 : ℝ) * N j * x.1 j) * (if j = k then (1 : ℝ) else 0) := by
104 intro j
105 simp only [ContinuousLinearMap.smul_apply, ContinuousLinearMap.add_apply, coordQ_apply,
106 Pi.single_apply, smul_eq_mul]
107 by_cases hjk : j = k <;> (simp [hjk]; try ring)
108 rw [Finset.sum_congr rfl fun j _ => step j, sum_mul_ite]
109
110theorem pderivP_VacSmear (N : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
111 pderivP (VacSmear N) k x = 0 := by
112 rw [pderivP, (hasFDerivAt_VacSmear N x).fderiv, VacSmearD,
113 ContinuousLinearMap.sum_apply]
114 refine Finset.sum_eq_zero fun j _ => ?_
115 simp [coordQ]
116
117def HamVac (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
118 ∑ j : ZMod 2, N j * vacuumShiftHamDensity x j
119
120theorem HamVac_eq_HamDyn_add_Vac (N : ZMod 2 → ℝ) :
121 HamVac N = fun x => HamDyn N x + VacSmear N x := by
122 funext x
123 unfold HamVac VacSmear vacuumShiftHamDensity
124 have hsum :
125 (∑ j : ZMod 2, N j * (hamDynDensity x j + x.1 j * x.1 j)) =
126 (∑ j : ZMod 2, N j * hamDynDensity x j) +
127 ∑ j : ZMod 2, N j * (x.1 j * x.1 j) := by
128 simp only [mul_add, sum_add_distrib]
129 rw [hsum]
130 have hDyn : (∑ j : ZMod 2, N j * hamDynDensity x j) = HamDyn N x := by
131 simpa using (congrArg (fun F : PhaseSpace 2 → ℝ => F x) (hamDynDensity_smear N))
132 rw [hDyn]
133
134theorem differentiable_HamVac (N : ZMod 2 → ℝ) :
135 Differentiable ℝ (HamVac N) := by
136 intro x
137 have hEq := HamVac_eq_HamDyn_add_Vac N
138 rw [hEq]
139 exact ((differentiable_HamDyn N x).add (hasFDerivAt_VacSmear N x).differentiableAt)
140
141/-! ## LocalHamSmooth for the vacuum profile -/
142
143def vacuumShiftLocalCellD (j : ZMod 2) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
144 hamDynLocalCellD j x + ((2 : ℝ) * x.1 j) • coordQ j
145
146lemma vacuumShiftLocalCellD_eq_profilePartials (j : ZMod 2) (x : PhaseSpace 2) :
147 vacuumShiftLocalCellD j x =
148 (vacuumShiftLocalHa (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
149 (vacuumShiftLocalHb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
150 (vacuumShiftLocalHp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j := by
151 -- Start from the HamDyn identity and add the vacuum Frechet term.
152 have h := hamDynLocalCellD_eq_profilePartials j x
153 apply ContinuousLinearMap.ext
154 intro v
155 have hv := congrArg (fun L : PhaseSpace 2 →L[ℝ] ℝ => L v) h
156 simp only [vacuumShiftLocalCellD, vacuumShiftLocalHa, vacuumShiftLocalHb,
157 vacuumShiftLocalHp, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
158 coordQ_apply, coordP_apply, smul_eq_mul] at hv ⊢
159 simp only [hamDynLocalHa, hamDynLocalHb, hamDynLocalHp] at hv ⊢
160 linarith [hv]
161
162set_option maxHeartbeats 800000 in
163lemma hasFDerivAt_vacuumShiftLocalCell_raw (j : ZMod 2) (x : PhaseSpace 2) :
164 HasFDerivAt (fun y : PhaseSpace 2 =>
165 vacuumShiftLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j))
166 (vacuumShiftLocalCellD j x) x := by
167 have hDyn := hasFDerivAt_hamDynLocalCell_raw j x
168 have hVac :=
169 ((hasFDerivAt_coord_fst j x).mul (hasFDerivAt_coord_fst j x))
170 have hform :
171 (fun y : PhaseSpace 2 =>
172 vacuumShiftLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j)) =
173 (fun y => hamDynLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j)) +
174 fun y => y.1 j * y.1 j := by
175 funext y
176 rfl
177 rw [hform]
178 have hAdd := hDyn.add hVac
179 -- Match derivative: hamDynLocalCellD + (q·coordQ + q·coordQ) = vacuumShiftLocalCellD.
180 convert hAdd using 1
181 apply ContinuousLinearMap.ext
182 intro v
183 simp only [vacuumShiftLocalCellD, ContinuousLinearMap.add_apply,
184 ContinuousLinearMap.smul_apply, coordQ_apply, smul_eq_mul]
185 ring
186
187lemma hasFDerivAt_vacuumShiftLocalCell (j : ZMod 2) (x : PhaseSpace 2) :
188 HasFDerivAt (fun y : PhaseSpace 2 =>
189 vacuumShiftLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j))
190 ((vacuumShiftLocalHa (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
191 (vacuumShiftLocalHb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
192 (vacuumShiftLocalHp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j)
193 x := by
194 rw [← vacuumShiftLocalCellD_eq_profilePartials]
195 exact hasFDerivAt_vacuumShiftLocalCell_raw j x
196
197def vacuumShiftLocalSmooth : LocalHamSmooth vacuumShiftLocalProfile where
198 ha := vacuumShiftLocalHa
199 hb := vacuumShiftLocalHb
200 hp := vacuumShiftLocalHp
201 hasFDerivCell := hasFDerivAt_vacuumShiftLocalCell
202
203/-! ## Bracket calculus -/
204
205theorem bracket_MomDyn_VacSmear (w N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
206 bracket (MomDyn w) (VacSmear N) x =
207 (2 : ℝ) * (x.1 1 - x.1 0) *
208 (w 1 * N 0 * x.1 0 - w 0 * N 1 * x.1 1) := by
209 have hL :
210 bracket (MomDyn w) (VacSmear N) x =
211 (pderivQ (MomDyn w) (0 : ZMod 2) x * pderivP (VacSmear N) (0 : ZMod 2) x -
212 pderivP (MomDyn w) (0 : ZMod 2) x * pderivQ (VacSmear N) (0 : ZMod 2) x) +
213 (pderivQ (MomDyn w) (1 : ZMod 2) x * pderivP (VacSmear N) (1 : ZMod 2) x -
214 pderivP (MomDyn w) (1 : ZMod 2) x * pderivQ (VacSmear N) (1 : ZMod 2) x) := by
215 unfold bracket
216 rw [sum_zmod2]
217 rw [hL, pderivQ_MomDyn_zero w x, pderivQ_MomDyn_one w x, pderivP_MomDyn_zero w x,
218 pderivP_MomDyn_one w x, pderivQ_VacSmear N (0 : ZMod 2) x, pderivQ_VacSmear N (1 : ZMod 2) x,
219 pderivP_VacSmear N (0 : ZMod 2) x, pderivP_VacSmear N (1 : ZMod 2) x]
220 ring
221
222set_option maxHeartbeats 800000 in
223theorem bracket_MomDyn_HamVac (w N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
224 bracket (MomDyn w) (HamVac N) x
225 = ∑ j : ZMod 2,
226 w j *
227 (N (j + 1) * vacuumShiftHamAdvTo x j -
228 N j * vacuumShiftHamAdvFrom x j) := by
229 have hFun : HamVac N = fun y => HamDyn N y + VacSmear N y :=
230 HamVac_eq_HamDyn_add_Vac N
231 have hDiffDyn : DifferentiableAt ℝ (HamDyn N) x := differentiable_HamDyn N x
232 have hDiffVac : DifferentiableAt ℝ (VacSmear N) x :=
233 (hasFDerivAt_VacSmear N x).differentiableAt
234 have hBracket :
235 bracket (MomDyn w) (HamVac N) x =
236 bracket (MomDyn w) (HamDyn N) x + bracket (MomDyn w) (VacSmear N) x := by
237 rw [hFun]
238 exact HypersurfaceDeformation.bracket_add_right (n := 2) (MomDyn w) hDiffDyn hDiffVac
239 have hDyn := bracket_MomDyn_HamDyn w N x
240 have hVac := bracket_MomDyn_VacSmear w N x
241 have hR :
242 (∑ j : ZMod 2,
243 w j *
244 (N (j + 1) * vacuumShiftHamAdvTo x j -
245 N j * vacuumShiftHamAdvFrom x j)) =
246 w 0 * (N 1 * vacuumShiftHamAdvTo x 0 - N 0 * vacuumShiftHamAdvFrom x 0) +
247 w 1 * (N 0 * vacuumShiftHamAdvTo x 1 - N 1 * vacuumShiftHamAdvFrom x 1) := by
248 rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
249 have hR' :
250 w 0 * (N 1 * vacuumShiftHamAdvTo x 0 - N 0 * vacuumShiftHamAdvFrom x 0) +
251 w 1 * (N 0 * vacuumShiftHamAdvTo x 1 - N 1 * vacuumShiftHamAdvFrom x 1) =
252 (w 0 * (N 1 * hamDynAdvTo x 0 - N 0 * hamDynAdvFrom x 0) +
253 w 1 * (N 0 * hamDynAdvTo x 1 - N 1 * hamDynAdvFrom x 1)) +
254 (2 : ℝ) * (x.1 1 - x.1 0) *
255 (w 1 * N 0 * x.1 0 - w 0 * N 1 * x.1 1) := by
256 simp only [vacuumShiftHamAdvTo, vacuumShiftHamAdvFrom, zmod2_zero_add_one,
257 zmod2_one_add_one]
258 ring
259 have hDynSum :
260 bracket (MomDyn w) (HamDyn N) x =
261 w 0 * (N 1 * hamDynAdvTo x 0 - N 0 * hamDynAdvFrom x 0) +
262 w 1 * (N 0 * hamDynAdvTo x 1 - N 1 * hamDynAdvFrom x 1) := by
263 rw [hDyn, sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
264 calc
265 bracket (MomDyn w) (HamVac N) x
266 = bracket (MomDyn w) (HamDyn N) x + bracket (MomDyn w) (VacSmear N) x :=
267 hBracket
268 _ = (w 0 * (N 1 * hamDynAdvTo x 0 - N 0 * hamDynAdvFrom x 0) +
269 w 1 * (N 0 * hamDynAdvTo x 1 - N 1 * hamDynAdvFrom x 1)) +
270 (2 : ℝ) * (x.1 1 - x.1 0) *
271 (w 1 * N 0 * x.1 0 - w 0 * N 1 * x.1 1) := by
272 rw [hDynSum, hVac]
273 _ = w 0 * (N 1 * vacuumShiftHamAdvTo x 0 - N 0 * vacuumShiftHamAdvFrom x 0) +
274 w 1 * (N 0 * vacuumShiftHamAdvTo x 1 - N 1 * vacuumShiftHamAdvFrom x 1) :=
275 hR'.symm
276 _ = ∑ j : ZMod 2,
277 w j *
278 (N (j + 1) * vacuumShiftHamAdvTo x j -
279 N j * vacuumShiftHamAdvFrom x j) := hR.symm
280
281theorem bracket_VacSmear_VacSmear (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
282 bracket (VacSmear N) (VacSmear M) x = 0 := by
283 simp only [bracket, pderivP_VacSmear]
284 exact Finset.sum_eq_zero fun _ _ => by ring
285
286theorem bracket_HamDyn_VacSmear (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
287 bracket (HamDyn N) (VacSmear M) x =
288 -∑ k : ZMod 2, (2 : ℝ) * N k * x.2 k * M k * x.1 k := by
289 unfold bracket
290 have hterm : ∀ k : ZMod 2,
291 pderivQ (HamDyn N) k x * pderivP (VacSmear M) k x -
292 pderivP (HamDyn N) k x * pderivQ (VacSmear M) k x =
293 -((2 : ℝ) * N k * x.2 k * M k * x.1 k) := by
294 intro k
295 rw [pderivP_VacSmear, pderivP_HamDyn, pderivQ_VacSmear]
296 ring
297 rw [Finset.sum_congr rfl fun k _ => hterm k, ← Finset.sum_neg_distrib]
298
299theorem bracket_VacSmear_HamDyn (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
300 bracket (VacSmear N) (HamDyn M) x =
301 ∑ k : ZMod 2, (2 : ℝ) * M k * x.2 k * N k * x.1 k := by
302 have h := bracket_HamDyn_VacSmear M N x
303 have hAnti := HypersurfaceDeformation.bracket_antisymm (n := 2) (VacSmear N) (HamDyn M) x
304 -- -(-(∑ 2 M π N q)) = ∑ 2 M π N q, after commuting scalars.
305 calc
306 bracket (VacSmear N) (HamDyn M) x
307 = -bracket (HamDyn M) (VacSmear N) x := hAnti
308 _ = -(-∑ k : ZMod 2, (2 : ℝ) * M k * x.2 k * N k * x.1 k) := by rw [h]
309 _ = ∑ k : ZMod 2, (2 : ℝ) * M k * x.2 k * N k * x.1 k := neg_neg _
310
311theorem bracket_HamVac_HamVac (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
312 bracket (HamVac N) (HamVac M) x = bracket (HamDyn N) (HamDyn M) x := by
313 have hN : HamVac N = fun y => HamDyn N y + VacSmear N y :=
314 HamVac_eq_HamDyn_add_Vac N
315 have hM : HamVac M = fun y => HamDyn M y + VacSmear M y :=
316 HamVac_eq_HamDyn_add_Vac M
317 have hDiffDynN : DifferentiableAt ℝ (HamDyn N) x := differentiable_HamDyn N x
318 have hDiffDynM : DifferentiableAt ℝ (HamDyn M) x := differentiable_HamDyn M x
319 have hDiffVacN : DifferentiableAt ℝ (VacSmear N) x :=
320 (hasFDerivAt_VacSmear N x).differentiableAt
321 have hDiffVacM : DifferentiableAt ℝ (VacSmear M) x :=
322 (hasFDerivAt_VacSmear M x).differentiableAt
323 have hCancel :
324 bracket (HamDyn N) (VacSmear M) x + bracket (VacSmear N) (HamDyn M) x = 0 := by
325 rw [bracket_HamDyn_VacSmear, bracket_VacSmear_HamDyn]
326 simp only [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib]
327 refine Finset.sum_eq_zero fun k _ => by ring
328 -- Expand both sides by bilinearity.
329 calc
330 bracket (HamVac N) (HamVac M) x
331 = bracket (fun y => HamDyn N y + VacSmear N y)
332 (fun y => HamDyn M y + VacSmear M y) x := by
333 simp [hN, hM]
334 _ = bracket (fun y => HamDyn N y + VacSmear N y) (HamDyn M) x +
335 bracket (fun y => HamDyn N y + VacSmear N y) (VacSmear M) x :=
336 HypersurfaceDeformation.bracket_add_right
337 (fun y => HamDyn N y + VacSmear N y) hDiffDynM hDiffVacM
338 _ = (bracket (HamDyn N) (HamDyn M) x + bracket (VacSmear N) (HamDyn M) x) +
339 (bracket (HamDyn N) (VacSmear M) x + bracket (VacSmear N) (VacSmear M) x) := by
340 rw [HypersurfaceDeformation.bracket_add_left (HamDyn M) hDiffDynN hDiffVacN,
341 HypersurfaceDeformation.bracket_add_left (VacSmear M) hDiffDynN hDiffVacN]
342 _ = bracket (HamDyn N) (HamDyn M) x +
343 (bracket (HamDyn N) (VacSmear M) x + bracket (VacSmear N) (HamDyn M) x) := by
344 rw [bracket_VacSmear_VacSmear, add_zero]
345 abel
346 _ = bracket (HamDyn N) (HamDyn M) x + 0 := by rw [hCancel]
347 _ = bracket (HamDyn N) (HamDyn M) x := by ring
348
349/-! ## Weak / strong / CanonicalMom inhabitants -/
350
351def vacuumShiftWeakTarget : HKTPointSplitTargetDyn 2 where
352 hamDensity := vacuumShiftHamDensity
353 momDensity := momDynDensity
354 structureFunction := structureDyn
355 hamAdvFrom := vacuumShiftHamAdvFrom
356 hamAdvTo := vacuumShiftHamAdvTo
357 momBracketDensity := momDynBracketDensity
358 ham_differentiable := by
359 intro N
360 have hEq : (fun x => ∑ j : ZMod 2, N j * vacuumShiftHamDensity x j) = HamVac N := by
361 funext x
362 rfl
363 simpa [hEq] using differentiable_HamVac N
364 mom_differentiable := differentiable_MomDyn
365 structure_nonconstant := structureDyn_not_constant
366 ham_local := by
367 intro x y j hx0 hx1 hp
368 dsimp only [vacuumShiftHamDensity, hamDynDensity]
369 rw [hx0, hx1, hp]
370 ham_covariant := by
371 intro x a j
372 unfold vacuumShiftHamDensity hamDynDensity
373 have e1 : (j + a + 1 : ZMod 2) = j + 1 + a := by ring
374 simp only [e1]
375 structure_local := by
376 intro x y j hx
377 dsimp only [structureDyn]
378 rw [hx]
379 mom_mom := by
380 intro v w x
381 simpa [MomDyn] using bracket_MomDyn_MomDyn v w x
382 mom_ham_split := by
383 intro w N x
384 have hEq :
385 (fun y => ∑ j : ZMod 2, N j * vacuumShiftHamDensity y j) = HamVac N := by
386 funext y
387 rfl
388 simpa [MomDyn, hEq] using bracket_MomDyn_HamVac w N x
389 ham_ham := by
390 intro N M x
391 have hL := bracket_HamVac_HamVac N M x
392 have hDyn := bracket_HamDyn_HamDyn N M x
393 have hL' :
394 bracket (fun y => ∑ j : ZMod 2, N j * vacuumShiftHamDensity y j)
395 (fun y => ∑ j : ZMod 2, M j * vacuumShiftHamDensity y j) x =
396 bracket (HamDyn N) (HamDyn M) x := by
397 simpa [HamVac] using hL
398 have hR :
399 (∑ j : ZMod 2,
400 (N j * M (j + 1) - M j * N (j + 1)) *
401 (structureDyn x j * momDynDensity x j)) =
402 bracket (HamDyn N) (HamDyn M) x := by
403 -- Match HamDyn identity rewritten in structureDyn / momDynDensity.
404 have h := hDyn
405 simp only [structureDyn, momDynDensity, concreteDynamicInverseMetric, pow_two] at h ⊢
406 exact h.symm
407 exact hL'.trans hR.symm
408 nondegenerate := by
409 refine ⟨hamDynNondegPhase, (0 : ZMod 2), ?_⟩
410 simp only [vacuumShiftHamDensity, hamDynDensity, hamDynNondegPhase]
411 norm_num
412
413def vacuumShiftStrongTarget : HKTPointSplitTargetDynStrong 2 where
414 toHKTPointSplitTargetDyn := vacuumShiftWeakTarget
415 mom_load_bearing := by
416 refine ⟨delta0, delta1, momLoadBearingWitnessPhase, ?_⟩
417 simpa [MomDyn] using hamDyn_mom_load_bearing_witness
418 advFrom_tied := by
419 intro x j
420 simpa using hamAdvFrom_eq_computed vacuumShiftWeakTarget x j
421 advTo_tied := by
422 intro x j
423 simpa using hamAdvTo_eq_computed vacuumShiftWeakTarget x j
424 kinetic_regular := by
425 refine ⟨hamDynNondegPhase, (0 : ZMod 2), ?_⟩
426 -- Unit-lapse vacuum Ham = HamDyn 1 + VacSmear 1; π-partial of Vac vanishes.
427 have hEq :
428 (fun y => ∑ i : ZMod 2, vacuumShiftHamDensity y i) =
429 fun y => HamDyn (fun _ => (1 : ℝ)) y + VacSmear (fun _ => (1 : ℝ)) y := by
430 funext y
431 have h1 : (∑ i : ZMod 2, vacuumShiftHamDensity y i) =
432 HamVac (fun _ => (1 : ℝ)) y := by
433 simp only [HamVac, one_mul]
434 have h2 : HamVac (fun _ => (1 : ℝ)) y =
435 HamDyn (fun _ => (1 : ℝ)) y + VacSmear (fun _ => (1 : ℝ)) y := by
436 simpa using congrArg (fun F : PhaseSpace 2 → ℝ => F y)
437 (HamVac_eq_HamDyn_add_Vac (fun _ => (1 : ℝ)))
438 exact h1.trans h2
439 have hDiffDyn : DifferentiableAt ℝ (HamDyn (fun _ => (1 : ℝ))) hamDynNondegPhase :=
440 differentiable_HamDyn (fun _ => (1 : ℝ)) hamDynNondegPhase
441 have hDiffVac : DifferentiableAt ℝ (VacSmear (fun _ => (1 : ℝ))) hamDynNondegPhase :=
442 (hasFDerivAt_VacSmear (fun _ => (1 : ℝ)) hamDynNondegPhase).differentiableAt
443 have hSum :
444 pderivP (fun y => ∑ i : ZMod 2, vacuumShiftHamDensity y i) (0 : ZMod 2)
445 hamDynNondegPhase =
446 pderivP (HamDyn (fun _ => (1 : ℝ))) (0 : ZMod 2) hamDynNondegPhase +
447 pderivP (VacSmear (fun _ => (1 : ℝ))) (0 : ZMod 2) hamDynNondegPhase := by
448 rw [hEq]
449 exact pderivP_fun_add (n := 2) hDiffDyn hDiffVac (0 : ZMod 2)
450 have hPVac :
451 pderivP (VacSmear (fun _ => (1 : ℝ))) (0 : ZMod 2) hamDynNondegPhase = 0 :=
452 pderivP_VacSmear (fun _ => (1 : ℝ)) (0 : ZMod 2) hamDynNondegPhase
453 have hPDyn :
454 pderivP (HamDyn (fun _ => (1 : ℝ))) (0 : ZMod 2) hamDynNondegPhase ≠ 0 := by
455 rw [pderivP_HamDyn]
456 simp only [hamDynNondegPhase]
457 norm_num
458 -- Goal uses the weak-target field, definitionally the vacuum density.
459 change pderivP (fun y => ∑ i : ZMod 2, vacuumShiftHamDensity y i) (0 : ZMod 2)
460 hamDynNondegPhase ≠ 0
461 rw [hSum, hPVac, add_zero]
462 exact hPDyn
463
464/-- THEOREM. Vacuum-shift density inhabits the CanonicalMom repaired class. -/
465def vacuumShiftCanonicalMomTarget : HKTPointSplitTargetDynCanonicalMom where
466 toHKTPointSplitTargetDynStrong := vacuumShiftStrongTarget
467 local_ham_profile :=
468 ⟨vacuumShiftLocalProfile, vacuumShiftLocalSmooth, vacuumShiftDensity_eq_localProfile⟩
469 structure_profile :=
470 ⟨fun q => 1 + q * q, structureDyn_eq_g⟩
471 canonical_mom := by
472 refine ⟨(1 : ℝ), by norm_num, ?_⟩
473 intro x j
474 simpa using momDynDensity_canonical x j
475
476/-! ## Kill of unconditioned CanonicalMom rigidity -/
477
478/-- Coincident configuration used in the vacuum kill: `qⱼ ≡ q`, `πⱼ ≡ 0`. -/
479def coincidentPhase (q : ℝ) : PhaseSpace 2 :=
480 (fun _ => q, fun _ => (0 : ℝ))
481
482/-- THEOREM. Unconditioned CanonicalMom rigidity is false. -/
483theorem not_HKTRigidityStatementPointSplitDynN2Canonical :
484 ¬ HKTRigidityStatementPointSplitDynN2Canonical := by
485 intro h
486 obtain ⟨cKin, cGrad, cVac, cMom, _hcKin, _hcGrad, _hRel, hHam, _hMom⟩ :=
487 h vacuumShiftCanonicalMomTarget
488 have hAt (q : ℝ) :
489 q * q = cVac := by
490 have h0 := hHam (coincidentPhase q) (0 : ZMod 2)
491 simp only [vacuumShiftCanonicalMomTarget, vacuumShiftStrongTarget, vacuumShiftWeakTarget,
492 vacuumShiftHamDensity, hamDynDensity, structureDyn, coincidentPhase,
493 zmod2_zero_add_one, sub_self, mul_zero, add_zero] at h0
494 -- h0 : q² = cKin·0 + cGrad·(1+q²)·0 + cVac
495 linarith
496 have h0 := hAt 0
497 have h1 := hAt 1
498 norm_num at h0 h1
499 linarith
500
501/-! ## Repaired terminal (DEFINED only) -/
502
503/-- DEFINED only. CanonicalMom rigidity modulo vacuum profile.
504
505Same quantification as `HKTRigidityStatementPointSplitDynN2Canonical`, with
506constant `cVac` weakened to a vacuum profile `V : ℝ → ℝ`. Do **not** cite as
507a theorem: whether `structure_nonconstant` + the alternating FE forces the
508kinetic/gradient sectors remains OPEN mathematics. -/
509def HKTRigidityModVacuumStatementN2 : Prop :=
510 ∀ T : HKTPointSplitTargetDynCanonicalMom,
511 ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
512 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
513 (∀ (x : PhaseSpace 2) (j : ZMod 2),
514 T.hamDensity x j =
515 cKin * (x.2 j * x.2 j) +
516 cGrad *
517 (T.structureFunction x j *
518 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
519 V (x.1 j)) ∧
520 (∀ (x : PhaseSpace 2) (j : ZMod 2),
521 T.momDensity x j =
522 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j))
523
524/-- Honesty wall (named note). ContDiff-2 + FE alone do not force the
525kinetic/gradient sectors (`sqrtAffineProfile`); that witness is blocked from
526CanonicalMom only by `structure_nonconstant` (`g ≡ 1`). Superseded by C4:
527`structure_nonconstant` also fails to close mod-vacuum (variable-kinetic kill
528in `HKTKineticNormalizedRigidity`). -/
529def Note_modVacuumSectorsRemainOpen : Prop := True
530
531theorem note_modVacuumSectorsRemainOpen : Note_modVacuumSectorsRemainOpen := trivial
532
533/-- C4 flip marker (bool status lives with the kill in
534`HKTKineticNormalizedRigidity`; this note records the supersession). -/
535def Note_modVacuumKilledInC4 : Prop := True
536
537theorem note_modVacuumKilledInC4 : Note_modVacuumKilledInC4 := trivial
538
539/-- ANCHOR (a). Vacuum-shift target satisfies the mod-vacuum conclusion shape. -/
540theorem vacuumShift_satisfies_modVacuum :
541 ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
542 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
543 (∀ (x : PhaseSpace 2) (j : ZMod 2),
544 vacuumShiftCanonicalMomTarget.hamDensity x j =
545 cKin * (x.2 j * x.2 j) +
546 cGrad *
547 (vacuumShiftCanonicalMomTarget.structureFunction x j *
548 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
549 V (x.1 j)) ∧
550 (∀ (x : PhaseSpace 2) (j : ZMod 2),
551 vacuumShiftCanonicalMomTarget.momDensity x j =
552 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
553 refine ⟨(1 / 2 : ℝ), (1 / 2 : ℝ), (1 : ℝ), fun a => a * a, by norm_num, by norm_num, ?_, ?_, ?_⟩
554 · norm_num
555 · intro x j
556 simp only [vacuumShiftCanonicalMomTarget, vacuumShiftStrongTarget, vacuumShiftWeakTarget,
557 vacuumShiftHamDensity, hamDynDensity, structureDyn]
558 ring
559 · intro x j
560 simp only [vacuumShiftCanonicalMomTarget, vacuumShiftStrongTarget, vacuumShiftWeakTarget,
561 momDynDensity]
562 ring
563
564/-- ANCHOR (b). Honest HamDyn CanonicalMom target satisfies the mod-vacuum shape
565(constant vacuum `V ≡ 0`). -/
566theorem hamDyn_satisfies_modVacuum :
567 ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
568 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
569 (∀ (x : PhaseSpace 2) (j : ZMod 2),
570 hamDynPointSplitTargetCanonicalMom.hamDensity x j =
571 cKin * (x.2 j * x.2 j) +
572 cGrad *
573 (hamDynPointSplitTargetCanonicalMom.structureFunction x j *
574 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
575 V (x.1 j)) ∧
576 (∀ (x : PhaseSpace 2) (j : ZMod 2),
577 hamDynPointSplitTargetCanonicalMom.momDensity x j =
578 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
579 obtain ⟨cKin, cGrad, cVac, cMom, hcKin, hcGrad, hRel, hHam, hMom⟩ :=
580 hamDyn_smooth_scoped_rigidity
581 refine ⟨cKin, cGrad, cMom, fun _ => cVac, hcKin, hcGrad, hRel, ?_, hMom⟩
582 intro x j
583 simpa using hHam x j
584
585/-! ## Status (C3; gap5 unflipped) -/
586
587structure HKTVacuumSectorKillStatus where
588 /-- Unconditioned CanonicalMom rigidity killed by vacuum shift. -/
589 canonicalMomRigidityKilled : Bool
590 /-- Mod-vacuum repaired terminal: open at C3 close; killed in C4
591 (`HKTKineticNormalizedRigidity.not_HKTRigidityModVacuumStatementN2`). -/
592 modVacuumRigidityOpen : Bool
593 /-- Local C3 status bit (historical): this module did not flip the ledger.
594 Ledger flip is owned by `Gap5ConstraintCloseStatus` (C5). -/
595 gap5ConstraintRecovery : Bool
596
597def hktVacuumSectorKillStatus : HKTVacuumSectorKillStatus where
598 canonicalMomRigidityKilled := true
599 modVacuumRigidityOpen := false
600 gap5ConstraintRecovery := false
601
602/-- Binding: C3 kill of unconditioned rigidity; mod-vacuum open bit flipped
603false by C4 (kill theorem lives in `HKTKineticNormalizedRigidity` to avoid a
604circular import). Local gap5 bit stays false; ledger gap5 flipped at C5. -/
605theorem hktVacuumSectorKillStatus_flags :
606 hktVacuumSectorKillStatus.canonicalMomRigidityKilled = true ∧
607 hktVacuumSectorKillStatus.modVacuumRigidityOpen = false ∧
608 hktVacuumSectorKillStatus.gap5ConstraintRecovery = false ∧
609 fullTheoryBenchmarks.gap5_constraint_recovery = true ∧
610 ¬ HKTRigidityStatementPointSplitDynN2Canonical ∧
611 Note_modVacuumKilledInC4 :=
612 ⟨rfl, rfl, rfl, rfl, not_HKTRigidityStatementPointSplitDynN2Canonical,
613 note_modVacuumKilledInC4⟩
614
615/-! ### Axiom receipts -/
616
617#print axioms not_HKTRigidityStatementPointSplitDynN2Canonical
618#print axioms vacuumShift_satisfies_modVacuum
619#print axioms hamDyn_satisfies_modVacuum
620#print axioms hktVacuumSectorKillStatus_flags
621
622end
623end HKTVacuumSectorKill
624end SevenGaps
625end Gravity
626end IndisputableMonolith
627