IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
IndisputableMonolith/Gravity/SevenGaps/HKTCanonicalMomTarget.lean · 665 lines · 53 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong
2import IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation
3import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
4
5/-!
6# Wave C2 gap5: kill strong rigidity + repaired CanonicalMom class
7
8Binding design: `D-qg-hkt-rigidity-route-20260722`.
9
10Session A: inhabit `HKTPointSplitTargetDynStrong 2` by the balanced quartic
11falsifier and prove `¬ HKTRigidityStatementPointSplitDynN2Strong`.
12
13Session B: define `HKTPointSplitTargetDynCanonicalMom`, exhibit the honest
14HamDyn inhabitant, separate the balanced quartic, and bank DEFINED-only
15`HKTRigidityStatementPointSplitDynN2Canonical` (sessions C prove it).
16
17No ledger flag is flipped (`gap5_constraint_recovery` stays false).
18-/
19
20namespace IndisputableMonolith
21namespace Gravity
22namespace SevenGaps
23namespace HKTCanonicalMomTarget
24
25open HypersurfaceDeformation DynamicStructureBracket DynamicStructureFunctionBlocker
26open HKTPointSplitTarget HKTPointSplitStrong HKTLocalFunctionalEquation
27open FullTheoryLedger
28
29noncomputable section
30
31open Finset
32
33private lemma zmod2_zero_add_one : (0 : ZMod 2) + 1 = 1 := by decide
34private lemma zmod2_one_add_one : (1 : ZMod 2) + 1 = 0 := by decide
35private lemma zmod2_succ_ne (j : ZMod 2) : (j + 1 : ZMod 2) ≠ j := by
36 fin_cases j <;> decide
37
38/-! ## Session A: balanced-quartic strong falsifier -/
39
40/-- MODEL. Structure `1 + q_j^2` (same shape as `structureDyn`). -/
41def quarticBalancedStructure2 (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
42 1 + x.1 j * x.1 j
43
44/-- MODEL. Quartic kinetic density `π_j^4`. -/
45def quarticBalancedHamDensity2 (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
46 (x.2 j) ^ 4
47
48/-- MODEL. Load-bearing momentum:
49`m_j = (π_0 + π_1) · structure(x, j+1)`. Balance identity
50`structure_0 · m_0 = structure_1 · m_1` cancels the `ham_ham` RHS on `ZMod 2`. -/
51def quarticBalancedMomDensity2 (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
52 (x.2 0 + x.2 1) * quarticBalancedStructure2 x (j + 1)
53
54/-- Honest source advection from `{Mom δ_j, Ham δ_j}`: vanishes because
55`∂_q Mom_j` is supported only at site `j+1`. -/
56def quarticBalancedHamAdvFrom2 (_x : PhaseSpace 2) (_j : ZMod 2) : ℝ :=
57 0
58
59/-- Honest target advection from `{Mom δ_j, Ham δ_{j+1}}`:
60`8 · (π_0+π_1) · q_{j+1} · π_{j+1}^3`. -/
61def quarticBalancedHamAdvTo2 (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
62 8 * (x.2 0 + x.2 1) * x.1 (j + 1) * (x.2 (j + 1)) ^ 3
63
64/-- Wronskian density witnessing nonabelian `{Mom, Mom}` for the balanced
65momentum. Chosen so
66`(mb_0 - mb_1) = 2(π_0+π_1)(q_1 S_0 - q_0 S_1)`. -/
67def quarticBalancedMomBracketDensity2 (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
68 (x.2 0 + x.2 1) *
69 (x.1 (j + 1) * quarticBalancedStructure2 x j -
70 x.1 j * quarticBalancedStructure2 x (j + 1))
71
72def quarticBalancedHam2 (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
73 ∑ j : ZMod 2, N j * quarticBalancedHamDensity2 x j
74
75def MomBalanced (w : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
76 ∑ j : ZMod 2, w j * quarticBalancedMomDensity2 x j
77
78theorem quarticBalanced_balance (x : PhaseSpace 2) :
79 quarticBalancedStructure2 x (0 : ZMod 2) * quarticBalancedMomDensity2 x 0 =
80 quarticBalancedStructure2 x (1 : ZMod 2) * quarticBalancedMomDensity2 x 1 := by
81 simp only [quarticBalancedMomDensity2, quarticBalancedStructure2, zmod2_zero_add_one,
82 zmod2_one_add_one]
83 ring
84
85theorem MomBalanced_closed (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
86 MomBalanced w x =
87 (x.2 0 + x.2 1) *
88 (w 0 * quarticBalancedStructure2 x 1 + w 1 * quarticBalancedStructure2 x 0) := by
89 unfold MomBalanced quarticBalancedMomDensity2
90 simp only [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
91 ring
92
93/-- Product-rule Frechet data for `MomBalanced`
94(`f x • g' + g x • f'` with `f = π₀+π₁`). -/
95def MomBalancedD (w : ZMod 2 → ℝ) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
96 (x.2 0 + x.2 1) •
97 (w 0 • (0 + (x.1 1 • coordQ 1 + x.1 1 • coordQ 1)) +
98 w 1 • (0 + (x.1 0 • coordQ 0 + x.1 0 • coordQ 0))) +
99 (w 0 * (1 + x.1 1 * x.1 1) + w 1 * (1 + x.1 0 * x.1 0)) •
100 (coordP (0 : ZMod 2) + coordP 1)
101
102lemma hasFDerivAt_MomBalanced (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
103 HasFDerivAt (MomBalanced w) (MomBalancedD w x) x := by
104 have hform :
105 MomBalanced w =
106 ((fun y : PhaseSpace 2 => y.2 0) + fun y => y.2 1) *
107 ((fun y => w 0 * (1 + y.1 1 * y.1 1)) +
108 fun y => w 1 * (1 + y.1 0 * y.1 0)) := by
109 funext y
110 dsimp [Pi.add_apply]
111 simpa [quarticBalancedStructure2] using MomBalanced_closed w y
112 have hq1 := hasFDerivAt_coord_fst (1 : ZMod 2) x
113 have hq0 := hasFDerivAt_coord_fst (0 : ZMod 2) x
114 -- Match Mathlib's `const.add` shape, including the `0 +` derivative term.
115 have hS1 := (hasFDerivAt_const (1 : ℝ) x).add (hq1.mul hq1)
116 have hS0 := (hasFDerivAt_const (1 : ℝ) x).add (hq0.mul hq0)
117 have hRight := (hS1.const_mul (w 0)).add (hS0.const_mul (w 1))
118 have hLeft :=
119 (hasFDerivAt_coord_snd (0 : ZMod 2) x).add (hasFDerivAt_coord_snd 1 x)
120 rw [hform]
121 exact hLeft.mul hRight
122
123theorem differentiable_MomBalanced (w : ZMod 2 → ℝ) :
124 Differentiable ℝ (MomBalanced w) :=
125 fun x => (hasFDerivAt_MomBalanced w x).differentiableAt
126
127theorem pderivQ_MomBalanced (w : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
128 pderivQ (MomBalanced w) k x =
129 (x.2 0 + x.2 1) * (2 * x.1 k) * w (k - 1) := by
130 rw [pderivQ, (hasFDerivAt_MomBalanced w x).fderiv, MomBalancedD]
131 simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, coordQ_apply,
132 coordP_apply, Pi.single_apply, smul_eq_mul, zero_add]
133 fin_cases k <;> simp [mul_assoc, mul_left_comm, mul_comm] <;> ring
134
135theorem pderivP_MomBalanced (w : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
136 pderivP (MomBalanced w) k x =
137 w 0 * quarticBalancedStructure2 x 1 + w 1 * quarticBalancedStructure2 x 0 := by
138 rw [pderivP, (hasFDerivAt_MomBalanced w x).fderiv, MomBalancedD]
139 simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, coordQ_apply,
140 coordP_apply, Pi.single_apply, smul_eq_mul, zero_add, quarticBalancedStructure2]
141 fin_cases k <;> simp [quarticBalancedStructure2]
142
143theorem bracket_MomBalanced_MomBalanced (v w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
144 bracket (MomBalanced v) (MomBalanced w) x
145 = ∑ j : ZMod 2,
146 (v j * w (j + 1) - w j * v (j + 1)) *
147 quarticBalancedMomBracketDensity2 x j := by
148 have hL :
149 bracket (MomBalanced v) (MomBalanced w) x =
150 (pderivQ (MomBalanced v) (0 : ZMod 2) x * pderivP (MomBalanced w) (0 : ZMod 2) x -
151 pderivP (MomBalanced v) (0 : ZMod 2) x * pderivQ (MomBalanced w) (0 : ZMod 2) x) +
152 (pderivQ (MomBalanced v) (1 : ZMod 2) x * pderivP (MomBalanced w) (1 : ZMod 2) x -
153 pderivP (MomBalanced v) (1 : ZMod 2) x * pderivQ (MomBalanced w) (1 : ZMod 2) x) := by
154 unfold bracket
155 rw [sum_zmod2]
156 have hR :
157 (∑ j : ZMod 2,
158 (v j * w (j + 1) - w j * v (j + 1)) *
159 quarticBalancedMomBracketDensity2 x j) =
160 (v 0 * w 1 - w 0 * v 1) * quarticBalancedMomBracketDensity2 x 0 +
161 (v 1 * w 0 - w 1 * v 0) * quarticBalancedMomBracketDensity2 x 1 := by
162 rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
163 rw [hL, hR, pderivQ_MomBalanced v (0 : ZMod 2) x, pderivQ_MomBalanced v (1 : ZMod 2) x,
164 pderivQ_MomBalanced w (0 : ZMod 2) x, pderivQ_MomBalanced w (1 : ZMod 2) x,
165 pderivP_MomBalanced v (0 : ZMod 2) x, pderivP_MomBalanced v (1 : ZMod 2) x,
166 pderivP_MomBalanced w (0 : ZMod 2) x, pderivP_MomBalanced w (1 : ZMod 2) x]
167 simp only [quarticBalancedMomBracketDensity2, quarticBalancedStructure2, zmod2_zero_add_one,
168 zmod2_one_add_one]
169 -- On ZMod 2: 0-1 = 1 and 1-1 = 0.
170 have e0 : ((0 : ZMod 2) - 1) = 1 := by decide
171 have e1 : ((1 : ZMod 2) - 1) = 0 := by decide
172 simp only [e0, e1]
173 ring
174
175set_option maxHeartbeats 800000 in
176theorem bracket_MomBalanced_quarticHam (w N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
177 bracket (MomBalanced w) (quarticBalancedHam2 N) x
178 = ∑ j : ZMod 2,
179 w j *
180 (N (j + 1) * quarticBalancedHamAdvTo2 x j -
181 N j * quarticBalancedHamAdvFrom2 x j) := by
182 -- Quartic ham is pure-π; expand via existing quartic Frechet from Strong.
183 have hHamD := hasFDerivAt_quarticHam2 N x
184 have hQ :
185 ∀ k : ZMod 2, pderivQ (quarticBalancedHam2 N) k x = 0 := by
186 intro k
187 -- Identify with Strong's `quarticHam2`.
188 have hEq : quarticBalancedHam2 N = quarticHam2 N := by
189 funext y
190 simp [quarticBalancedHam2, quarticHam2, quarticBalancedHamDensity2, quarticHamDensity2]
191 simpa [hEq] using pderivQ_quarticHam2 N k x
192 have hP :
193 ∀ k : ZMod 2,
194 pderivP (quarticBalancedHam2 N) k x = N k * (4 * (x.2 k) ^ 3) := by
195 intro k
196 have hEq : quarticBalancedHam2 N = quarticHam2 N := by
197 funext y
198 simp [quarticBalancedHam2, quarticHam2, quarticBalancedHamDensity2, quarticHamDensity2]
199 rw [hEq, pderivP, (hasFDerivAt_quarticHam2 N x).fderiv, quarticHam2D,
200 ContinuousLinearMap.sum_apply]
201 have step : ∀ i : ZMod 2,
202 (((N i) • ((4 • (x.2 i) ^ 3) • coordP i) : PhaseSpace 2 →L[ℝ] ℝ)
203 ((0, Pi.single k 1) : PhaseSpace 2))
204 = (N i * (4 * (x.2 i) ^ 3)) * (if i = k then (1 : ℝ) else 0) := by
205 intro i
206 simp only [ContinuousLinearMap.smul_apply, coordP_apply, Pi.single_apply, smul_eq_mul,
207 nsmul_eq_mul, Nat.cast_ofNat]
208 by_cases hik : i = k <;> simp [hik] <;> ring
209 rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]
210 have hL :
211 bracket (MomBalanced w) (quarticBalancedHam2 N) x =
212 (pderivQ (MomBalanced w) (0 : ZMod 2) x * pderivP (quarticBalancedHam2 N) (0 : ZMod 2) x -
213 pderivP (MomBalanced w) (0 : ZMod 2) x * pderivQ (quarticBalancedHam2 N) (0 : ZMod 2) x) +
214 (pderivQ (MomBalanced w) (1 : ZMod 2) x * pderivP (quarticBalancedHam2 N) (1 : ZMod 2) x -
215 pderivP (MomBalanced w) (1 : ZMod 2) x * pderivQ (quarticBalancedHam2 N) (1 : ZMod 2) x) := by
216 unfold bracket
217 rw [sum_zmod2]
218 have hR :
219 (∑ j : ZMod 2,
220 w j *
221 (N (j + 1) * quarticBalancedHamAdvTo2 x j -
222 N j * quarticBalancedHamAdvFrom2 x j)) =
223 w 0 * (N 1 * quarticBalancedHamAdvTo2 x 0 - N 0 * quarticBalancedHamAdvFrom2 x 0) +
224 w 1 * (N 0 * quarticBalancedHamAdvTo2 x 1 - N 1 * quarticBalancedHamAdvFrom2 x 1) := by
225 rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
226 rw [hL, hR, pderivQ_MomBalanced w (0 : ZMod 2) x, pderivQ_MomBalanced w (1 : ZMod 2) x,
227 pderivP_MomBalanced w (0 : ZMod 2) x, pderivP_MomBalanced w (1 : ZMod 2) x,
228 hQ 0, hQ 1, hP 0, hP 1]
229 have e0 : ((0 : ZMod 2) - 1) = 1 := by decide
230 have e1 : ((1 : ZMod 2) - 1) = 0 := by decide
231 simp only [e0, e1, quarticBalancedHamAdvFrom2, quarticBalancedHamAdvTo2, zmod2_zero_add_one,
232 zmod2_one_add_one, mul_zero, sub_zero]
233 ring
234
235theorem bracket_quarticBalancedHam_quarticBalancedHam (N M : ZMod 2 → ℝ)
236 (x : PhaseSpace 2) :
237 bracket (quarticBalancedHam2 N) (quarticBalancedHam2 M) x = 0 := by
238 have hEqN : quarticBalancedHam2 N = quarticHam2 N := by
239 funext y
240 simp [quarticBalancedHam2, quarticHam2, quarticBalancedHamDensity2, quarticHamDensity2]
241 have hEqM : quarticBalancedHam2 M = quarticHam2 M := by
242 funext y
243 simp [quarticBalancedHam2, quarticHam2, quarticBalancedHamDensity2, quarticHamDensity2]
244 simpa [hEqN, hEqM] using bracket_quarticHam2_quarticHam2 N M x
245
246theorem quarticBalancedStructure2_not_constant :
247 ¬ PhaseSpaceConstant quarticBalancedStructure2 := by
248 intro h
249 have hEq := h zeroPhasePoint unitConfigurationPoint (0 : ZMod 2)
250 simp only [quarticBalancedStructure2, zeroPhasePoint, unitConfigurationPoint] at hEq
251 norm_num at hEq
252
253def quarticBalancedNondegPhase : PhaseSpace 2 :=
254 (fun _ => (0 : ℝ), fun j => if j = (0 : ZMod 2) then (1 : ℝ) else 0)
255
256theorem quarticBalancedHamDensity2_nondeg :
257 quarticBalancedHamDensity2 quarticBalancedNondegPhase (0 : ZMod 2) ≠ 0 := by
258 simp only [quarticBalancedHamDensity2, quarticBalancedNondegPhase]
259 norm_num
260
261/-- Design witness for `mom_load_bearing`: `q=(1,0)`, `π=(1,0)`. -/
262def quarticBalancedLoadPhase : PhaseSpace 2 :=
263 (fun j : ZMod 2 => if j = (0 : ZMod 2) then (1 : ℝ) else 0,
264 fun j : ZMod 2 => if j = (0 : ZMod 2) then (1 : ℝ) else 0)
265
266theorem quarticBalanced_mom_load_bearing_witness :
267 bracket (MomBalanced delta0) (MomBalanced delta1) quarticBalancedLoadPhase ≠ 0 := by
268 have h := bracket_MomBalanced_MomBalanced delta0 delta1 quarticBalancedLoadPhase
269 have hδ0 : delta0 (0 : ZMod 2) = (1 : ℝ) ∧ delta0 (1 : ZMod 2) = 0 := by simp [delta0]
270 have hδ1 : delta1 (0 : ZMod 2) = (0 : ℝ) ∧ delta1 (1 : ZMod 2) = 1 := by simp [delta1]
271 have hq0 : quarticBalancedLoadPhase.1 (0 : ZMod 2) = 1 := by simp [quarticBalancedLoadPhase]
272 have hq1 : quarticBalancedLoadPhase.1 (1 : ZMod 2) = 0 := by simp [quarticBalancedLoadPhase]
273 have hp0 : quarticBalancedLoadPhase.2 (0 : ZMod 2) = 1 := by simp [quarticBalancedLoadPhase]
274 have hp1 : quarticBalancedLoadPhase.2 (1 : ZMod 2) = 0 := by simp [quarticBalancedLoadPhase]
275 have hd0 :
276 quarticBalancedMomBracketDensity2 quarticBalancedLoadPhase (0 : ZMod 2) = (-1 : ℝ) := by
277 simp [quarticBalancedMomBracketDensity2, quarticBalancedStructure2, zmod2_zero_add_one,
278 hq0, hq1, hp0, hp1]
279 have hd1 :
280 quarticBalancedMomBracketDensity2 quarticBalancedLoadPhase (1 : ZMod 2) = (1 : ℝ) := by
281 simp [quarticBalancedMomBracketDensity2, quarticBalancedStructure2, zmod2_one_add_one,
282 hq0, hq1, hp0, hp1]
283 rw [h, sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one, hδ0.1, hδ0.2, hδ1.1, hδ1.2, hd0, hd1]
284 norm_num
285
286theorem quarticBalanced_kinetic_regular_witness :
287 pderivP (fun y => ∑ i : ZMod 2, quarticBalancedHamDensity2 y i) (0 : ZMod 2)
288 quarticBalancedNondegPhase ≠ 0 := by
289 have hEq :
290 (fun y => ∑ i : ZMod 2, quarticBalancedHamDensity2 y i) =
291 quarticBalancedHam2 (fun _ => (1 : ℝ)) := by
292 funext y
293 simp [quarticBalancedHam2]
294 have hEq' : quarticBalancedHam2 (fun _ => (1 : ℝ)) = quarticHam2 (fun _ => (1 : ℝ)) := by
295 funext y
296 simp [quarticBalancedHam2, quarticHam2, quarticBalancedHamDensity2, quarticHamDensity2]
297 rw [hEq, hEq', pderivP, (hasFDerivAt_quarticHam2 (fun _ => (1 : ℝ))
298 quarticBalancedNondegPhase).fderiv, quarticHam2D, ContinuousLinearMap.sum_apply]
299 simp only [quarticBalancedNondegPhase, ContinuousLinearMap.smul_apply, coordP_apply,
300 Pi.single_apply, smul_eq_mul, nsmul_eq_mul, Nat.cast_ofNat]
301 -- Only the i=0 term survives: 1 * 4 * 1^3 * 1 = 4.
302 have huniv : (univ : Finset (ZMod 2)) = {0, 1} := by decide
303 rw [huniv, Finset.sum_pair (by decide : (0 : ZMod 2) ≠ 1)]
304 norm_num
305
306/-- THEOREM. Balanced quartic inhabits the WEAK point-split schema. -/
307def quarticBalancedWeakTarget : HKTPointSplitTargetDyn 2 where
308 hamDensity := quarticBalancedHamDensity2
309 momDensity := quarticBalancedMomDensity2
310 structureFunction := quarticBalancedStructure2
311 hamAdvFrom := quarticBalancedHamAdvFrom2
312 hamAdvTo := quarticBalancedHamAdvTo2
313 momBracketDensity := quarticBalancedMomBracketDensity2
314 ham_differentiable := by
315 intro N
316 have hEq : (fun x => ∑ j : ZMod 2, N j * quarticBalancedHamDensity2 x j) =
317 quarticHam2 N := by
318 funext x
319 simp [quarticHam2, quarticBalancedHamDensity2, quarticHamDensity2]
320 simpa [hEq] using differentiable_quarticHam2 N
321 mom_differentiable := by
322 intro w
323 simpa [MomBalanced] using differentiable_MomBalanced w
324 structure_nonconstant := quarticBalancedStructure2_not_constant
325 ham_local := by
326 intro x y j _ _ hp
327 dsimp only [quarticBalancedHamDensity2]
328 rw [hp]
329 ham_covariant := by
330 intro x a j
331 simp [quarticBalancedHamDensity2]
332 structure_local := by
333 intro x y j hx
334 simp [quarticBalancedStructure2, hx]
335 mom_mom := by
336 intro v w x
337 simpa [MomBalanced] using bracket_MomBalanced_MomBalanced v w x
338 mom_ham_split := by
339 intro w N x
340 have hEq :
341 (fun y => ∑ j : ZMod 2, N j * quarticBalancedHamDensity2 y j) =
342 quarticBalancedHam2 N := by
343 funext y
344 rfl
345 simpa [MomBalanced, hEq] using bracket_MomBalanced_quarticHam w N x
346 ham_ham := by
347 intro N M x
348 have hL := bracket_quarticBalancedHam_quarticBalancedHam N M x
349 have hBal := quarticBalanced_balance x
350 have hR :
351 (∑ j : ZMod 2,
352 (N j * M (j + 1) - M j * N (j + 1)) *
353 (quarticBalancedStructure2 x j * quarticBalancedMomDensity2 x j)) = 0 := by
354 rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
355 have hdiff :
356 quarticBalancedStructure2 x 0 * quarticBalancedMomDensity2 x 0 -
357 quarticBalancedStructure2 x 1 * quarticBalancedMomDensity2 x 1 = 0 := by
358 linarith [hBal]
359 -- (N0 M1 - M0 N1)*(s0 m0) + (N1 M0 - M1 N0)*(s1 m1)
360 -- = (N0 M1 - M0 N1)*(s0 m0 - s1 m1).
361 calc
362 (N 0 * M 1 - M 0 * N 1) *
363 (quarticBalancedStructure2 x 0 * quarticBalancedMomDensity2 x 0) +
364 (N 1 * M 0 - M 1 * N 0) *
365 (quarticBalancedStructure2 x 1 * quarticBalancedMomDensity2 x 1)
366 = (N 0 * M 1 - M 0 * N 1) *
367 (quarticBalancedStructure2 x 0 * quarticBalancedMomDensity2 x 0 -
368 quarticBalancedStructure2 x 1 * quarticBalancedMomDensity2 x 1) := by
369 ring
370 _ = (N 0 * M 1 - M 0 * N 1) * 0 := by rw [hdiff]
371 _ = 0 := by ring
372 have hL' :
373 bracket (fun y => ∑ j : ZMod 2, N j * quarticBalancedHamDensity2 y j)
374 (fun y => ∑ j : ZMod 2, M j * quarticBalancedHamDensity2 y j) x = 0 := by
375 simpa [quarticBalancedHam2] using hL
376 exact hL'.trans hR.symm
377 nondegenerate := ⟨quarticBalancedNondegPhase, (0 : ZMod 2), quarticBalancedHamDensity2_nondeg⟩
378
379/-- THEOREM. Balanced quartic inhabits the STRENGTHENED class
380(honest advection slots; load-bearing momentum; kinetic regularity). -/
381def quarticBalancedStrongTarget : HKTPointSplitTargetDynStrong 2 where
382 toHKTPointSplitTargetDyn := quarticBalancedWeakTarget
383 mom_load_bearing := by
384 refine ⟨delta0, delta1, quarticBalancedLoadPhase, ?_⟩
385 simpa [MomBalanced] using quarticBalanced_mom_load_bearing_witness
386 advFrom_tied := by
387 intro x j
388 simpa using hamAdvFrom_eq_computed quarticBalancedWeakTarget x j
389 advTo_tied := by
390 intro x j
391 simpa using hamAdvTo_eq_computed quarticBalancedWeakTarget x j
392 kinetic_regular :=
393 ⟨quarticBalancedNondegPhase, (0 : ZMod 2), quarticBalanced_kinetic_regular_witness⟩
394
395/-- Constant-configuration phase point used in the rigidity kill. -/
396def constConfigPhase (q p : ℝ) : PhaseSpace 2 :=
397 (fun _ => q, fun _ => p)
398
399/-- THEOREM. Strong-class rigidity is false: the balanced quartic forces
400`p^4 = cKin p^2 + cVac` at three momenta, a contradiction. -/
401theorem not_HKTRigidityStatementPointSplitDynN2Strong :
402 ¬ HKTRigidityStatementPointSplitDynN2Strong := by
403 intro h
404 obtain ⟨cKin, cGrad, cVac, hForm⟩ := h quarticBalancedStrongTarget
405 -- Evaluate at constant configuration (gradient term vanishes) and three momenta.
406 have hAt (p : ℝ) :
407 (p : ℝ) ^ 4 = cKin * (p * p) + cVac := by
408 have h0 := hForm (constConfigPhase 0 p) (0 : ZMod 2)
409 -- Unfold the strong-target densities at constant q = 0.
410 simp [quarticBalancedStrongTarget, quarticBalancedWeakTarget, quarticBalancedHamDensity2,
411 quarticBalancedStructure2, constConfigPhase, zmod2_zero_add_one] at h0
412 -- h0 : p^4 = cKin * p^2 + cGrad * 0 + cVac
413 linarith
414 have h0 := hAt 0
415 have h1 := hAt 1
416 have h2 := hAt 2
417 norm_num at h0 h1 h2
418 -- 0 = cVac; 1 = cKin + cVac; 16 = 4 cKin + cVac.
419 linarith
420
421/-! ## Session B: CanonicalMom repaired class -/
422
423/-- REPAIRED TARGET. Extends the strong class by three load-bearing fields:
424(1) local Hamiltonian profile (cells of the form `h(q_j, q_{j+1}, π_j)`);
425(2) structure profile `g(q_j)`;
426(3) canonical momentum density
427`m_j = cMom · π_{j+1} · (q_{j+1} - q_j)` with `cMom ≠ 0`
428(the true HamDyn shape; the balanced quartic fails it). -/
429structure HKTPointSplitTargetDynCanonicalMom
430 extends HKTPointSplitTargetDynStrong 2 where
431 local_ham_profile :
432 ∃ (h : LocalHamProfile) (_S : LocalHamSmooth h),
433 ∀ (x : PhaseSpace 2) (j : ZMod 2),
434 hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)
435 structure_profile :
436 ∃ g : ℝ → ℝ, ∀ (x : PhaseSpace 2) (j : ZMod 2),
437 structureFunction x j = g (x.1 j)
438 canonical_mom :
439 ∃ cMom : ℝ, cMom ≠ 0 ∧
440 ∀ (x : PhaseSpace 2) (j : ZMod 2),
441 momDensity x j = cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)
442
443/-- Local profile for the honest HamDyn density (written with `* (1/2)` so the
444Frechet data matches `HasFDerivAt.const_mul`). -/
445def hamDynLocalProfile : LocalHamProfile :=
446 fun a b p =>
447 (1 / 2 : ℝ) * (p * p + (1 + a * a) * ((b - a) * (b - a)))
448
449def hamDynLocalHa : LocalHamProfile :=
450 fun a b _p => a * ((b - a) * (b - a)) - (1 + a * a) * (b - a)
451
452def hamDynLocalHb : LocalHamProfile :=
453 fun a b _p => (1 + a * a) * (b - a)
454
455def hamDynLocalHp : LocalHamProfile :=
456 fun _a _b p => p
457
458/-- Frechet data matching Mathlib's product-rule expansion of the numerator,
459scaled by `1/2`. -/
460def hamDynLocalCellD (j : ZMod 2) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
461 (1 / 2 : ℝ) •
462 ((x.2 j • coordP j + x.2 j • coordP j) +
463 (((1 : ℝ) + x.1 j * x.1 j) •
464 ((x.1 (j + 1) - x.1 j) • (coordQ (j + 1) - coordQ j) +
465 (x.1 (j + 1) - x.1 j) • (coordQ (j + 1) - coordQ j)) +
466 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)) •
467 (0 + (x.1 j • coordQ j + x.1 j • coordQ j))))
468
469lemma hamDynLocalCellD_eq_profilePartials (j : ZMod 2) (x : PhaseSpace 2) :
470 hamDynLocalCellD j x =
471 (hamDynLocalHa (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
472 (hamDynLocalHb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
473 (hamDynLocalHp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j := by
474 apply ContinuousLinearMap.ext
475 intro v
476 -- Evaluate both linear maps on a phase-space vector; close by ring.
477 simp only [hamDynLocalCellD, hamDynLocalHa, hamDynLocalHb, hamDynLocalHp,
478 ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
479 ContinuousLinearMap.sub_apply, coordQ_apply, coordP_apply, smul_eq_mul, zero_add]
480 ring
481
482set_option maxHeartbeats 800000 in
483lemma hasFDerivAt_hamDynLocalCell_raw (j : ZMod 2) (x : PhaseSpace 2) :
484 HasFDerivAt (fun y : PhaseSpace 2 =>
485 hamDynLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j))
486 (hamDynLocalCellD j x) x := by
487 have hqj := hasFDerivAt_coord_fst j x
488 have hqjp := hasFDerivAt_coord_fst (j + 1) x
489 have hpj := hasFDerivAt_coord_snd j x
490 have hDiff := hqjp.sub hqj
491 have hDiffSq := hDiff.mul hDiff
492 have ha2 := hqj.mul hqj
493 have hOneA2 := (hasFDerivAt_const (1 : ℝ) x).add ha2
494 have hStructGrad := hOneA2.mul hDiffSq
495 have hp2 := hpj.mul hpj
496 have hSum := hp2.add hStructGrad
497 have hHalf := hSum.const_mul (1 / 2 : ℝ)
498 -- Identify profile with `(1/2) * numerator`.
499 have hform :
500 (fun y : PhaseSpace 2 => hamDynLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j)) =
501 fun y =>
502 (1 / 2 : ℝ) *
503 (y.2 j * y.2 j +
504 (1 + y.1 j * y.1 j) *
505 ((y.1 (j + 1) - y.1 j) * (y.1 (j + 1) - y.1 j))) := by
506 funext y
507 rfl
508 rw [hform]
509 exact hHalf
510
511lemma hasFDerivAt_hamDynLocalCell (j : ZMod 2) (x : PhaseSpace 2) :
512 HasFDerivAt (fun y : PhaseSpace 2 =>
513 hamDynLocalProfile (y.1 j) (y.1 (j + 1)) (y.2 j))
514 ((hamDynLocalHa (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
515 (hamDynLocalHb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
516 (hamDynLocalHp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j)
517 x := by
518 rw [← hamDynLocalCellD_eq_profilePartials]
519 exact hasFDerivAt_hamDynLocalCell_raw j x
520
521def hamDynLocalSmooth : LocalHamSmooth hamDynLocalProfile where
522 ha := hamDynLocalHa
523 hb := hamDynLocalHb
524 hp := hamDynLocalHp
525 hasFDerivCell := hasFDerivAt_hamDynLocalCell
526
527theorem hamDynDensity_eq_localProfile (x : PhaseSpace 2) (j : ZMod 2) :
528 hamDynDensity x j = hamDynLocalProfile (x.1 j) (x.1 (j + 1)) (x.2 j) := by
529 unfold hamDynDensity hamDynLocalProfile
530 ring
531
532theorem structureDyn_eq_g (x : PhaseSpace 2) (j : ZMod 2) :
533 structureDyn x j = (fun q : ℝ => 1 + q * q) (x.1 j) := by
534 unfold structureDyn
535 rfl
536
537theorem momDynDensity_canonical (x : PhaseSpace 2) (j : ZMod 2) :
538 momDynDensity x j = (1 : ℝ) * x.2 (j + 1) * (x.1 (j + 1) - x.1 j) := by
539 unfold momDynDensity
540 ring
541
542/-- THEOREM. Honest HamDyn inhabitant of the CanonicalMom repaired class. -/
543def hamDynPointSplitTargetCanonicalMom : HKTPointSplitTargetDynCanonicalMom where
544 toHKTPointSplitTargetDynStrong := hamDynPointSplitTargetStrong
545 local_ham_profile :=
546 ⟨hamDynLocalProfile, hamDynLocalSmooth, hamDynDensity_eq_localProfile⟩
547 structure_profile :=
548 ⟨fun q => 1 + q * q, structureDyn_eq_g⟩
549 canonical_mom := by
550 refine ⟨(1 : ℝ), by norm_num, ?_⟩
551 intro x j
552 simpa using momDynDensity_canonical x j
553
554theorem hktPointSplitTargetDynCanonicalMom_nonvacuous :
555 Nonempty (HKTPointSplitTargetDynCanonicalMom) :=
556 ⟨hamDynPointSplitTargetCanonicalMom⟩
557
558/-- Cheapest separation: at coincident configuration and equal momenta the
559canonical form vanishes, while balanced-quartic momentum is nonzero. -/
560def canonicalMomSepPhase : PhaseSpace 2 :=
561 (fun _ => (0 : ℝ), fun _ => (1 : ℝ))
562
563theorem quarticBalanced_fails_canonical_mom :
564 ¬ ∃ cMom : ℝ, cMom ≠ 0 ∧
565 ∀ (x : PhaseSpace 2) (j : ZMod 2),
566 quarticBalancedMomDensity2 x j =
567 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j) := by
568 rintro ⟨cMom, _, hForm⟩
569 have h := hForm canonicalMomSepPhase (0 : ZMod 2)
570 -- LHS = (1+1)*(1+0) = 2; RHS = cMom * 1 * 0 = 0.
571 simp only [quarticBalancedMomDensity2, quarticBalancedStructure2, canonicalMomSepPhase,
572 zmod2_zero_add_one] at h
573 norm_num at h
574
575/-- THEOREM. The balanced-quartic strong falsifier does not inhabit CanonicalMom. -/
576theorem canonicalMom_excludes_balanced_quartic :
577 ¬ ∃ C : HKTPointSplitTargetDynCanonicalMom,
578 C.toHKTPointSplitTargetDynStrong = quarticBalancedStrongTarget := by
579 rintro ⟨C, hEq⟩
580 obtain ⟨cMom, hc, hMom⟩ := C.canonical_mom
581 apply quarticBalanced_fails_canonical_mom
582 refine ⟨cMom, hc, ?_⟩
583 intro x j
584 have hC := hMom x j
585 -- Transport through equality of strong targets.
586 have hDens :
587 C.momDensity x j = quarticBalancedStrongTarget.momDensity x j :=
588 congrArg (fun S : HKTPointSplitTargetDynStrong 2 => S.momDensity x j) hEq
589 -- Strong target momentum is definitionally the balanced density.
590 have hBal :
591 quarticBalancedStrongTarget.momDensity x j = quarticBalancedMomDensity2 x j :=
592 rfl
593 exact (hDens.trans hBal).symm.trans hC
594
595/-! ## DEFINED-only CanonicalMom rigidity (sessions C) -/
596
597/-- DEFINED only. GR-strength rigidity over the CanonicalMom class at `n = 2`.
598
599Proving this is **sessions C**, via
600`profiled_ham_ham_alternating_FE` then `solve_profile_FE_quadratic`
601(separation of variables + `LocalHamSmooth` integration). Do not cite as a
602theorem.
603
604Prover decoys (from `D-qg-hkt-rigidity-route-20260722`):
6051. uniqueness only over `LocalHamFromProfile` images (misses non-profiled
606 strong targets; the CanonicalMom field closes that gap);
6072. subclass with canonical_form baked into the density constructors
608 (content-free: proves nothing about forced shape);
6093. pointwise coefficient extraction at `n = 2` (false: `ham_ham` only fixes
610 the alternating difference `C0 - C1 = R0 - R1` on `ZMod 2`). -/
611def HKTRigidityStatementPointSplitDynN2Canonical : Prop :=
612 ∀ T : HKTPointSplitTargetDynCanonicalMom,
613 ∃ cKin cGrad cVac cMom : ℝ,
614 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
615 (∀ (x : PhaseSpace 2) (j : ZMod 2),
616 T.hamDensity x j =
617 cKin * (x.2 j * x.2 j) +
618 cGrad *
619 (T.structureFunction x j *
620 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
621 cVac) ∧
622 (∀ (x : PhaseSpace 2) (j : ZMod 2),
623 T.momDensity x j =
624 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j))
625
626/-! ## Status (gap5 unflipped) -/
627
628structure HKTCanonicalMomStatus where
629 /-- Session A: strong rigidity killed by balanced quartic. -/
630 rigidityStrongKilled : Bool
631 /-- Session B: CanonicalMom class + honest inhabitant banked. -/
632 canonicalMomDefined : Bool
633 /-- Sessions C still open. -/
634 canonicalMomRigidityOpen : Bool
635 /-- Ledger flag stays false. -/
636 gap5ConstraintRecovery : Bool
637
638def hktCanonicalMomStatus : HKTCanonicalMomStatus where
639 rigidityStrongKilled := true
640 canonicalMomDefined := true
641 canonicalMomRigidityOpen := true
642 gap5ConstraintRecovery := false
643
644theorem hktCanonicalMomStatus_flags :
645 hktCanonicalMomStatus.rigidityStrongKilled = true ∧
646 hktCanonicalMomStatus.canonicalMomDefined = true ∧
647 hktCanonicalMomStatus.canonicalMomRigidityOpen = true ∧
648 hktCanonicalMomStatus.gap5ConstraintRecovery = false ∧
649 fullTheoryBenchmarks.gap5_constraint_recovery = true := by
650 decide
651
652/-! ### Axiom receipts -/
653
654#print axioms not_HKTRigidityStatementPointSplitDynN2Strong
655#print axioms quarticBalanced_mom_load_bearing_witness
656#print axioms canonicalMom_excludes_balanced_quartic
657#print axioms hktPointSplitTargetDynCanonicalMom_nonvacuous
658#print axioms hktCanonicalMomStatus_flags
659
660end
661end HKTCanonicalMomTarget
662end SevenGaps
663end Gravity
664end IndisputableMonolith
665