IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation
IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean · 982 lines · 65 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# Hypersurface deformation: discrete constraint closure on the periodic lattice
5
6QG Seven-Gaps campaign, gap "constraint closure" (Lane 5). This file builds the
7first theorem-grade layer of the ADM/Dirac constraint-algebra program for the
8discrete gravity effort: a finite-dimensional canonical phase space on a periodic
91D lattice, an honest fderiv-based Poisson bracket, and kernel-checked closure
10relations for the discrete constraint generators in the linearized regime.
11
12## Scope (honest)
13
14The `(q, pi)` system here is ONE polarization of the linearized (TT-gauge) field
15on a 1D periodic lattice, i.e. a lattice wave field. It is offered as the first
16rung of the ADM program, not as full gravity: there is no metric degree of
17freedom on this rung, so the continuum structure function `g^{ab}` of the Dirac
18algebra is frozen to 1.
19
20## Status ledger
21
22* MODEL: `PhaseSpace`, `pderivQ`/`pderivP`/`bracket` (the bracket is total; on
23 observables that are not differentiable at `x` the `fderiv` junk value 0
24 enters, so bracket statements about general observables carry explicit
25 differentiability hypotheses). `Dgen`, `DgenSym`, `Ham` are definitional
26 lattice discretizations of the momentum and Hamiltonian constraints.
27* THEOREM (all axiom-clean, no sorry, unconditional unless stated):
28 - `bracket_antisymm`, `bracket_self` (no hypotheses);
29 - bilinearity `bracket_add_left/right`, `bracket_const_mul_left/right` and
30 Leibniz `bracket_mul_left/right`, each with explicit `DifferentiableAt`
31 hypotheses (these enter as hypotheses on theorems, never as axioms);
32 - canonical relations `bracket_coordQ_coordP`, `bracket_coordQ_coordQ`,
33 `bracket_coordP_coordP`;
34 - momentum-sector closure `bracket_Dgen_Dgen = 0`,
35 `bracket_DgenSym_DgenSym = 0` (the abelian translation sector closes
36 sharply: the bracket vanishes identically, it does not merely close up to
37 combinations of shift generators);
38 - `bracket_Dgen_Ham` (general lapse, forward difference): the TRUE identity,
39 derived by hand and then formalized;
40 - `bracket_Dgen_Ham_one`: for constant lapse the forward-difference generator
41 does NOT commute with `Ham`; the exact closure anomaly is
42 `((delta_a d)^2 - (delta_a pi)^2)/2` summed over sites. This CORRECTS the
43 naively expected `{H[1], D_a} = 0`: the naive one-sided discretization
44 breaks translation closure, and the obstruction is an explicit second-order
45 lattice artifact (it is quadratic in the a-step differences of the field
46 gradient and momentum, hence vanishes on shift-invariant configurations and
47 in the naive continuum limit).
48 - `bracket_DgenSym_Ham`: the symmetric-difference momentum generator
49 satisfies the EXACT discrete advection (hypersurface-deformation) relation
50 `{Dsym_a, H[N]} = (1/2) * sum_j (N(j+a) - N j) * (pi_j pi_{j+a} + d_j d_{j+a})`,
51 a point-split smearing of the Hamiltonian density by the lattice derivative
52 of the lapse; corollary `bracket_DgenSym_Ham_one = 0` (exact translation
53 invariance, constant lapse).
54 - `bracket_Ham_Ham`: the discrete hypersurface-deformation relation
55 `{H[N], H[M]} = sum_j (N_j M_{j+1} - M_j N_{j+1}) * pi_{j+1} (q_{j+1} - q_j)`:
56 two Hamiltonian deformations close on a D-type (momentum) generator whose
57 smearing is the discrete Wronskian of the two lapses. In the continuum limit
58 `N M' - M N'` smears `pi q'`, which is the Dirac relation
59 `{H(N), H(M)} = D(N M' - M N')` with unit structure function on this
60 flat scalar rung.
61* OPEN:
62 - Jacobi for the fderiv bracket. `JacobiOn` names the precise statement; it is
63 NOT proved here (for non-C^2 observables it can fail; for polynomial
64 observables it is expected but requires second-derivative bookkeeping).
65 - The full Dirac algebra recovery in the continuum limit (lattice spacing to
66 zero) remains OPEN.
67 - The Hojman-Kuchar-Teitelboim (HKT) recovery: the structure
68 `HojmanKucharTeitelboimTarget` names, as Prop-valued fields with real
69 mathematical content, lattice renderings of the exact HKT hypotheses
70 (representation of the hypersurface-deformation algebra by local, covariant
71 densities). It is deliberately NOT inhabited: our concrete generators
72 realize `mom_mom` exactly but `mom_ham`/`ham_ham` only in point-split form
73 (density evaluated at split lattice points), and that gap is precisely the
74 discrete-closure frontier. `HKTRigidityStatement` names the rigidity
75 conclusion (the deformation algebra forces the Einstein-Hilbert form, here:
76 the wave-Hamiltonian form of the density); it is stated, never asserted.
77
78## Design notes
79
80* Sites are `ZMod n` (`n > 0` via `[NeZero n]`), so lattice translation is
81 group addition and all reindexing is done by honest sum bijections.
82* The bracket is `sum_i (dF/dq_i * dG/dpi_i - dF/dpi_i * dG/dq_i)` with the
83 partial derivatives implemented as `fderiv R F x` applied to the basis
84 directions `(Pi.single i 1, 0)` and `(0, Pi.single i 1)`. No axiomatized
85 bracket, no `: True` fields, no `Nonempty` shells anywhere in this file.
86* All generator-closure theorems are unconditional: the generators are
87 quadratic polynomials in the coordinates, so every differentiability side
88 condition is discharged (`HasFDerivAt` built from `ContinuousLinearMap`
89 coordinates via `mul`/`sub`/`add`/`const_mul`).
90-/
91
92namespace IndisputableMonolith
93namespace Gravity
94namespace SevenGaps
95namespace HypersurfaceDeformation
96
97noncomputable section
98
99open Finset
100
101variable {n : ℕ} [NeZero n]
102
103/-- MODEL. The canonical phase space of the lattice wave field: configuration
104`q : ZMod n → ℝ` and conjugate momentum `pi : ZMod n → ℝ` on the periodic
105lattice with `n` sites. -/
106abbrev PhaseSpace (n : ℕ) : Type := (ZMod n → ℝ) × (ZMod n → ℝ)
107
108/-! ## Coordinate functionals -/
109
110/-- The configuration coordinate `q_i` as a continuous linear functional. -/
111def coordQ (i : ZMod n) : PhaseSpace n →L[ℝ] ℝ :=
112 (ContinuousLinearMap.proj i).comp (ContinuousLinearMap.fst ℝ (ZMod n → ℝ) (ZMod n → ℝ))
113
114/-- The momentum coordinate `pi_i` as a continuous linear functional. -/
115def coordP (i : ZMod n) : PhaseSpace n →L[ℝ] ℝ :=
116 (ContinuousLinearMap.proj i).comp (ContinuousLinearMap.snd ℝ (ZMod n → ℝ) (ZMod n → ℝ))
117
118omit [NeZero n] in
119@[simp] lemma coordQ_apply (i : ZMod n) (x : PhaseSpace n) : coordQ i x = x.1 i := rfl
120
121omit [NeZero n] in
122@[simp] lemma coordP_apply (i : ZMod n) (x : PhaseSpace n) : coordP i x = x.2 i := rfl
123
124/-! ## Partial derivatives and the Poisson bracket -/
125
126/-- Partial derivative of an observable in the configuration direction `q_i`:
127`fderiv` applied to the basis vector `(Pi.single i 1, 0)`. -/
128def pderivQ (F : PhaseSpace n → ℝ) (i : ZMod n) (x : PhaseSpace n) : ℝ :=
129 fderiv ℝ F x (Pi.single i 1, 0)
130
131/-- Partial derivative of an observable in the momentum direction `pi_i`:
132`fderiv` applied to the basis vector `(0, Pi.single i 1)`. -/
133def pderivP (F : PhaseSpace n → ℝ) (i : ZMod n) (x : PhaseSpace n) : ℝ :=
134 fderiv ℝ F x (0, Pi.single i 1)
135
136/-- MODEL. The Poisson bracket
137`{F, G}(x) = sum_i (dF/dq_i * dG/dpi_i - dF/dpi_i * dG/dq_i)`.
138Honest but total: for observables not differentiable at `x` the `fderiv` junk
139value `0` enters, which is why the general structure theorems below carry
140explicit `DifferentiableAt` hypotheses. -/
141def bracket (F G : PhaseSpace n → ℝ) (x : PhaseSpace n) : ℝ :=
142 ∑ i : ZMod n, (pderivQ F i x * pderivP G i x - pderivP F i x * pderivQ G i x)
143
144/-! ## Summation helpers (periodic reindexing and Kronecker collapse) -/
145
146/-- Periodic sums are invariant under lattice translation. -/
147lemma sum_shift (a : ZMod n) (f : ZMod n → ℝ) :
148 (∑ j : ZMod n, f (j + a)) = ∑ j : ZMod n, f j :=
149 Fintype.sum_equiv (Equiv.addRight a) (fun j => f (j + a)) f (fun _ => rfl)
150
151/-- Reindex a periodic sum by the translation `j ↦ j + a`. -/
152lemma sum_reindex (a : ZMod n) (f g : ZMod n → ℝ) (h : ∀ j, f (j + a) = g j) :
153 (∑ j : ZMod n, f j) = ∑ j : ZMod n, g j := by
154 rw [← sum_shift a f]
155 exact Finset.sum_congr rfl fun j _ => h j
156
157/-- Kronecker collapse: `sum_i g i * [i = c] = g c`. -/
158lemma sum_mul_ite (g : ZMod n → ℝ) (c : ZMod n) :
159 (∑ i : ZMod n, g i * (if i = c then (1 : ℝ) else 0)) = g c := by
160 rw [Finset.sum_eq_single c]
161 · simp
162 · intro b _ hb
163 simp [hb]
164 · intro h
165 exact absurd (Finset.mem_univ _) h
166
167/-- Kronecker collapse with a shifted condition: `sum_i g i * [i + a = c] = g (c - a)`. -/
168lemma sum_mul_ite_add (g : ZMod n → ℝ) (a c : ZMod n) :
169 (∑ i : ZMod n, g i * (if i + a = c then (1 : ℝ) else 0)) = g (c - a) := by
170 rw [Finset.sum_eq_single (c - a)]
171 · have h : c - a + a = c := by ring
172 simp [h]
173 · intro b _ hb
174 have hcond : ¬(b + a = c) := by
175 intro h
176 apply hb
177 rw [← h]
178 ring
179 simp [hcond]
180 · intro h
181 exact absurd (Finset.mem_univ _) h
182
183/-- Kronecker collapse with a back-shifted condition: `sum_i g i * [i - a = c] = g (c + a)`. -/
184lemma sum_mul_ite_sub (g : ZMod n → ℝ) (a c : ZMod n) :
185 (∑ i : ZMod n, g i * (if i - a = c then (1 : ℝ) else 0)) = g (c + a) := by
186 rw [Finset.sum_eq_single (c + a)]
187 · have h : c + a - a = c := by ring
188 simp [h]
189 · intro b _ hb
190 have hcond : ¬(b - a = c) := by
191 intro h
192 apply hb
193 rw [← h]
194 ring
195 simp [hcond]
196 · intro h
197 exact absurd (Finset.mem_univ _) h
198
199/-! ## Structure theorems for the bracket
200
201Antisymmetry is unconditional. Bilinearity and the Leibniz rule hold with
202explicit `DifferentiableAt` hypotheses, exactly as far as `fderiv` linearity
203gives them. Jacobi is NOT claimed (see `JacobiOn` below, recorded OPEN). -/
204
205/-- THEOREM. Antisymmetry of the bracket (no differentiability needed). -/
206theorem bracket_antisymm (F G : PhaseSpace n → ℝ) (x : PhaseSpace n) :
207 bracket F G x = - bracket G F x := by
208 have h : bracket F G x + bracket G F x = 0 := by
209 rw [bracket, bracket, ← Finset.sum_add_distrib]
210 exact Finset.sum_eq_zero fun i _ => by ring
211 linarith
212
213/-- THEOREM. The bracket of an observable with itself vanishes. -/
214theorem bracket_self (F : PhaseSpace n → ℝ) (x : PhaseSpace n) :
215 bracket F F x = 0 := by
216 have h := bracket_antisymm F F x
217 linarith
218
219lemma pderivQ_fun_add {F G : PhaseSpace n → ℝ} {x : PhaseSpace n}
220 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (i : ZMod n) :
221 pderivQ (fun y => F y + G y) i x = pderivQ F i x + pderivQ G i x := by
222 simp [pderivQ, fderiv_fun_add hF hG]
223
224lemma pderivP_fun_add {F G : PhaseSpace n → ℝ} {x : PhaseSpace n}
225 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (i : ZMod n) :
226 pderivP (fun y => F y + G y) i x = pderivP F i x + pderivP G i x := by
227 simp [pderivP, fderiv_fun_add hF hG]
228
229lemma pderivQ_const_mul {F : PhaseSpace n → ℝ} {x : PhaseSpace n}
230 (hF : DifferentiableAt ℝ F x) (c : ℝ) (i : ZMod n) :
231 pderivQ (fun y => c * F y) i x = c * pderivQ F i x := by
232 simp [pderivQ, (hF.hasFDerivAt.const_mul c).fderiv]
233
234lemma pderivP_const_mul {F : PhaseSpace n → ℝ} {x : PhaseSpace n}
235 (hF : DifferentiableAt ℝ F x) (c : ℝ) (i : ZMod n) :
236 pderivP (fun y => c * F y) i x = c * pderivP F i x := by
237 simp [pderivP, (hF.hasFDerivAt.const_mul c).fderiv]
238
239lemma pderivQ_fun_mul {F G : PhaseSpace n → ℝ} {x : PhaseSpace n}
240 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (i : ZMod n) :
241 pderivQ (fun y => F y * G y) i x = F x * pderivQ G i x + G x * pderivQ F i x := by
242 simp [pderivQ, fderiv_fun_mul hF hG]
243
244lemma pderivP_fun_mul {F G : PhaseSpace n → ℝ} {x : PhaseSpace n}
245 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (i : ZMod n) :
246 pderivP (fun y => F y * G y) i x = F x * pderivP G i x + G x * pderivP F i x := by
247 simp [pderivP, fderiv_fun_mul hF hG]
248
249/-- THEOREM. Additivity in the first argument (differentiability as explicit
250hypotheses, never axioms). -/
251theorem bracket_add_left {F G : PhaseSpace n → ℝ} (K : PhaseSpace n → ℝ) {x : PhaseSpace n}
252 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) :
253 bracket (fun y => F y + G y) K x = bracket F K x + bracket G K x := by
254 simp only [bracket, pderivQ_fun_add hF hG, pderivP_fun_add hF hG]
255 rw [← Finset.sum_add_distrib]
256 exact Finset.sum_congr rfl fun i _ => by ring
257
258/-- THEOREM. Additivity in the second argument. -/
259theorem bracket_add_right {F G : PhaseSpace n → ℝ} (K : PhaseSpace n → ℝ) {x : PhaseSpace n}
260 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) :
261 bracket K (fun y => F y + G y) x = bracket K F x + bracket K G x := by
262 have h1 := bracket_antisymm (n := n) K (fun y => F y + G y) x
263 have h2 := bracket_add_left (n := n) K hF hG
264 have h3 := bracket_antisymm (n := n) F K x
265 have h4 := bracket_antisymm (n := n) G K x
266 linarith
267
268/-- THEOREM. Scalar homogeneity in the first argument. -/
269theorem bracket_const_mul_left {F : PhaseSpace n → ℝ} (K : PhaseSpace n → ℝ)
270 {x : PhaseSpace n} (hF : DifferentiableAt ℝ F x) (c : ℝ) :
271 bracket (fun y => c * F y) K x = c * bracket F K x := by
272 simp only [bracket, pderivQ_const_mul hF c, pderivP_const_mul hF c, Finset.mul_sum]
273 exact Finset.sum_congr rfl fun i _ => by ring
274
275/-- THEOREM. Scalar homogeneity in the second argument. -/
276theorem bracket_const_mul_right {F : PhaseSpace n → ℝ} (K : PhaseSpace n → ℝ)
277 {x : PhaseSpace n} (hF : DifferentiableAt ℝ F x) (c : ℝ) :
278 bracket K (fun y => c * F y) x = c * bracket K F x := by
279 have h1 := bracket_antisymm (n := n) K (fun y => c * F y) x
280 have h2 := bracket_const_mul_left (n := n) K hF c
281 have h3 := bracket_antisymm (n := n) F K x
282 linear_combination h1 - h2 - c * h3
283
284/-- THEOREM. Leibniz rule in the first argument (from `fderiv_fun_mul`, with
285explicit differentiability hypotheses). -/
286theorem bracket_mul_left {F G : PhaseSpace n → ℝ} (K : PhaseSpace n → ℝ) {x : PhaseSpace n}
287 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) :
288 bracket (fun y => F y * G y) K x = F x * bracket G K x + G x * bracket F K x := by
289 simp only [bracket, pderivQ_fun_mul hF hG, pderivP_fun_mul hF hG, Finset.mul_sum]
290 rw [← Finset.sum_add_distrib]
291 exact Finset.sum_congr rfl fun i _ => by ring
292
293/-- THEOREM. Leibniz rule in the second argument. -/
294theorem bracket_mul_right {F G : PhaseSpace n → ℝ} (K : PhaseSpace n → ℝ) {x : PhaseSpace n}
295 (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) :
296 bracket K (fun y => F y * G y) x = F x * bracket K G x + G x * bracket K F x := by
297 have h1 := bracket_antisymm (n := n) K (fun y => F y * G y) x
298 have h2 := bracket_mul_left (n := n) K hF hG
299 have h3 := bracket_antisymm (n := n) G K x
300 have h4 := bracket_antisymm (n := n) F K x
301 linear_combination h1 - h2 - F x * h3 - G x * h4
302
303/-- OPEN. The Jacobi identity for the fderiv bracket, restricted to a class `S`
304of observables. This names the precise statement; it is NOT proved in this
305file (and is not expected to hold for observables that are not C^2). Proving it
306for the class of quadratic polynomial observables is the natural next rung. -/
307def JacobiOn (S : Set (PhaseSpace n → ℝ)) : Prop :=
308 ∀ F ∈ S, ∀ G ∈ S, ∀ H ∈ S, ∀ x : PhaseSpace n,
309 bracket F (bracket G H) x + bracket G (bracket H F) x + bracket H (bracket F G) x = 0
310
311/-! ## Canonical relations -/
312
313lemma hasFDerivAt_coord_fst (k : ZMod n) (x : PhaseSpace n) :
314 HasFDerivAt (fun y : PhaseSpace n => y.1 k) (coordQ k) x :=
315 (coordQ k).hasFDerivAt
316
317lemma hasFDerivAt_coord_snd (k : ZMod n) (x : PhaseSpace n) :
318 HasFDerivAt (fun y : PhaseSpace n => y.2 k) (coordP k) x :=
319 (coordP k).hasFDerivAt
320
321/-- THEOREM. Canonical relation `{q_k, pi_l} = delta_{kl}`. -/
322theorem bracket_coordQ_coordP (k l : ZMod n) (x : PhaseSpace n) :
323 bracket (fun y : PhaseSpace n => y.1 k) (fun y : PhaseSpace n => y.2 l) x
324 = if k = l then (1 : ℝ) else 0 := by
325 have hQ : ∀ i : ZMod n, pderivQ (fun y : PhaseSpace n => y.1 k) i x
326 = if k = i then (1 : ℝ) else 0 := by
327 intro i
328 rw [pderivQ, (hasFDerivAt_coord_fst k x).fderiv]
329 simp [coordQ, Pi.single_apply]
330 have hP0 : ∀ i : ZMod n, pderivP (fun y : PhaseSpace n => y.1 k) i x = 0 := by
331 intro i
332 rw [pderivP, (hasFDerivAt_coord_fst k x).fderiv]
333 simp [coordQ]
334 have hP : ∀ i : ZMod n, pderivP (fun y : PhaseSpace n => y.2 l) i x
335 = if l = i then (1 : ℝ) else 0 := by
336 intro i
337 rw [pderivP, (hasFDerivAt_coord_snd l x).fderiv]
338 simp [coordP, Pi.single_apply]
339 have hQ0 : ∀ i : ZMod n, pderivQ (fun y : PhaseSpace n => y.2 l) i x = 0 := by
340 intro i
341 rw [pderivQ, (hasFDerivAt_coord_snd l x).fderiv]
342 simp [coordP]
343 simp only [bracket, hQ, hP, hQ0, hP0, mul_zero, sub_zero]
344 by_cases hkl : k = l
345 · subst hkl
346 rw [Finset.sum_eq_single k]
347 · simp
348 · intro b _ hb
349 simp [Ne.symm hb]
350 · intro h
351 exact absurd (Finset.mem_univ _) h
352 · rw [if_neg hkl]
353 apply Finset.sum_eq_zero
354 intro i _
355 by_cases hk : k = i
356 · subst hk
357 have : ¬(l = k) := fun h => hkl h.symm
358 simp [this]
359 · simp [hk]
360
361/-- THEOREM. Canonical relation `{q_k, q_l} = 0`. -/
362theorem bracket_coordQ_coordQ (k l : ZMod n) (x : PhaseSpace n) :
363 bracket (fun y : PhaseSpace n => y.1 k) (fun y : PhaseSpace n => y.1 l) x = 0 := by
364 have hP0k : ∀ i : ZMod n, pderivP (fun y : PhaseSpace n => y.1 k) i x = 0 := by
365 intro i
366 rw [pderivP, (hasFDerivAt_coord_fst k x).fderiv]
367 simp [coordQ]
368 have hP0l : ∀ i : ZMod n, pderivP (fun y : PhaseSpace n => y.1 l) i x = 0 := by
369 intro i
370 rw [pderivP, (hasFDerivAt_coord_fst l x).fderiv]
371 simp [coordQ]
372 simp only [bracket, hP0k, hP0l, mul_zero, zero_mul, sub_zero]
373 exact Finset.sum_eq_zero fun i _ => by ring
374
375/-- THEOREM. Canonical relation `{pi_k, pi_l} = 0`. -/
376theorem bracket_coordP_coordP (k l : ZMod n) (x : PhaseSpace n) :
377 bracket (fun y : PhaseSpace n => y.2 k) (fun y : PhaseSpace n => y.2 l) x = 0 := by
378 have hQ0k : ∀ i : ZMod n, pderivQ (fun y : PhaseSpace n => y.2 k) i x = 0 := by
379 intro i
380 rw [pderivQ, (hasFDerivAt_coord_snd k x).fderiv]
381 simp [coordP]
382 have hQ0l : ∀ i : ZMod n, pderivQ (fun y : PhaseSpace n => y.2 l) i x = 0 := by
383 intro i
384 rw [pderivQ, (hasFDerivAt_coord_snd l x).fderiv]
385 simp [coordP]
386 simp only [bracket, hQ0k, hQ0l, mul_zero, zero_mul, sub_zero]
387 exact Finset.sum_eq_zero fun i _ => by ring
388
389/-! ## The discrete constraint generators
390
391`Dgen a` is the forward-difference (one-sided) discretization of the momentum
392constraint smeared by the constant shift vector `a`; `DgenSym a` is the
393symmetric-difference discretization; `Ham N` is the smeared quadratic
394(linearized) Hamiltonian constraint with lapse `N`. -/
395
396/-- MODEL. Forward-difference momentum (shift) generator
397`D_a[q,pi] = sum_i pi_i (q_{i+a} - q_i)`. -/
398def Dgen (a : ZMod n) (x : PhaseSpace n) : ℝ :=
399 ∑ i : ZMod n, x.2 i * (x.1 (i + a) - x.1 i)
400
401/-- MODEL. Symmetric-difference momentum generator
402`Dsym_a[q,pi] = (1/2) sum_i pi_i (q_{i+a} - q_{i-a})`. On the periodic lattice
403the symmetric difference operator is antisymmetric (discrete integration by
404parts with no boundary), and this is exactly what restores the closure of the
405momentum-Hamiltonian bracket; see `bracket_DgenSym_Ham`. -/
406def DgenSym (a : ZMod n) (x : PhaseSpace n) : ℝ :=
407 ∑ i : ZMod n, (1 / 2 : ℝ) * (x.2 i * (x.1 (i + a) - x.1 (i - a)))
408
409/-- MODEL. Smeared linearized Hamiltonian constraint
410`H[N] = sum_i N_i (pi_i^2 + (q_{i+1} - q_i)^2) / 2`. -/
411def Ham (N : ZMod n → ℝ) (x : PhaseSpace n) : ℝ :=
412 ∑ i : ZMod n, (N i / 2) * (x.2 i * x.2 i + (x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i))
413
414/-- `Ham` agrees with the squared form of the mission statement. -/
415lemma Ham_eq_sq (N : ZMod n → ℝ) (x : PhaseSpace n) :
416 Ham N x = ∑ i : ZMod n, N i * ((x.2 i) ^ 2 + (x.1 (i + 1) - x.1 i) ^ 2) / 2 :=
417 Finset.sum_congr rfl fun i _ => by ring
418
419/-- The symmetric generator is the average of the forward generator and the
420reversed one: `Dsym_a = (D_a - D_{-a}) / 2`. -/
421lemma DgenSym_eq (a : ZMod n) (x : PhaseSpace n) :
422 DgenSym a x = (Dgen a x - Dgen (-a) x) / 2 := by
423 rw [DgenSym, Dgen, Dgen, ← Finset.sum_sub_distrib, Finset.sum_div]
424 refine Finset.sum_congr rfl fun i _ => ?_
425 have e : i + -a = i - a := by ring
426 rw [e]
427 ring
428
429/-! ### Frechet derivatives of the generators (all side conditions discharged) -/
430
431/-- The derivative of `Dgen a` at `x`, as an explicit continuous linear map. -/
432def DgenD (a : ZMod n) (x : PhaseSpace n) : PhaseSpace n →L[ℝ] ℝ :=
433 ∑ i : ZMod n,
434 (x.2 i • (coordQ (i + a) - coordQ i) + (x.1 (i + a) - x.1 i) • coordP i)
435
436lemma hasFDerivAt_Dgen (a : ZMod n) (x : PhaseSpace n) :
437 HasFDerivAt (Dgen a) (DgenD a x) x := by
438 unfold Dgen DgenD
439 exact HasFDerivAt.fun_sum fun i _ =>
440 (hasFDerivAt_coord_snd i x).mul
441 ((hasFDerivAt_coord_fst (i + a) x).sub (hasFDerivAt_coord_fst i x))
442
443/-- THEOREM. `Dgen a` is (unconditionally) differentiable. -/
444theorem differentiable_Dgen (a : ZMod n) : Differentiable ℝ (Dgen (n := n) a) :=
445 fun x => (hasFDerivAt_Dgen a x).differentiableAt
446
447/-- The derivative of `DgenSym a` at `x`. -/
448def DgenSymD (a : ZMod n) (x : PhaseSpace n) : PhaseSpace n →L[ℝ] ℝ :=
449 ∑ i : ZMod n,
450 (1 / 2 : ℝ) • (x.2 i • (coordQ (i + a) - coordQ (i - a))
451 + (x.1 (i + a) - x.1 (i - a)) • coordP i)
452
453lemma hasFDerivAt_DgenSym (a : ZMod n) (x : PhaseSpace n) :
454 HasFDerivAt (DgenSym a) (DgenSymD a x) x := by
455 unfold DgenSym DgenSymD
456 exact HasFDerivAt.fun_sum fun i _ =>
457 (((hasFDerivAt_coord_snd i x).mul
458 ((hasFDerivAt_coord_fst (i + a) x).sub (hasFDerivAt_coord_fst (i - a) x))).const_mul
459 (1 / 2 : ℝ))
460
461/-- THEOREM. `DgenSym a` is (unconditionally) differentiable. -/
462theorem differentiable_DgenSym (a : ZMod n) : Differentiable ℝ (DgenSym (n := n) a) :=
463 fun x => (hasFDerivAt_DgenSym a x).differentiableAt
464
465/-- The derivative of `Ham N` at `x`. -/
466def HamD (N : ZMod n → ℝ) (x : PhaseSpace n) : PhaseSpace n →L[ℝ] ℝ :=
467 ∑ i : ZMod n,
468 (N i / 2) • ((x.2 i • coordP i + x.2 i • coordP i)
469 + ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)
470 + (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)))
471
472lemma hasFDerivAt_Ham (N : ZMod n → ℝ) (x : PhaseSpace n) :
473 HasFDerivAt (Ham N) (HamD N x) x := by
474 unfold Ham HamD
475 exact HasFDerivAt.fun_sum fun i _ =>
476 ((((hasFDerivAt_coord_snd i x).mul (hasFDerivAt_coord_snd i x)).add
477 (((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x)).mul
478 ((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x)))).const_mul
479 (N i / 2))
480
481/-- THEOREM. `Ham N` is (unconditionally) differentiable. -/
482theorem differentiable_Ham (N : ZMod n → ℝ) : Differentiable ℝ (Ham (n := n) N) :=
483 fun x => (hasFDerivAt_Ham N x).differentiableAt
484
485/-! ### Partial derivatives of the generators (Kronecker collapse) -/
486
487lemma pderivQ_Dgen (a j : ZMod n) (x : PhaseSpace n) :
488 pderivQ (Dgen a) j x = x.2 (j - a) - x.2 j := by
489 rw [pderivQ, (hasFDerivAt_Dgen a x).fderiv, DgenD, ContinuousLinearMap.sum_apply]
490 have step : ∀ i : ZMod n,
491 (x.2 i • (coordQ (i + a) - coordQ i) + (x.1 (i + a) - x.1 i) • coordP i)
492 ((Pi.single j 1, 0) : PhaseSpace n)
493 = x.2 i * (if i + a = j then (1 : ℝ) else 0)
494 - x.2 i * (if i = j then (1 : ℝ) else 0) := by
495 intro i
496 simp [Pi.single_apply, mul_sub]
497 rw [Finset.sum_congr rfl fun i _ => step i, Finset.sum_sub_distrib,
498 sum_mul_ite_add, sum_mul_ite]
499
500lemma pderivP_Dgen (a j : ZMod n) (x : PhaseSpace n) :
501 pderivP (Dgen a) j x = x.1 (j + a) - x.1 j := by
502 rw [pderivP, (hasFDerivAt_Dgen a x).fderiv, DgenD, ContinuousLinearMap.sum_apply]
503 have step : ∀ i : ZMod n,
504 (x.2 i • (coordQ (i + a) - coordQ i) + (x.1 (i + a) - x.1 i) • coordP i)
505 ((0, Pi.single j 1) : PhaseSpace n)
506 = (x.1 (i + a) - x.1 i) * (if i = j then (1 : ℝ) else 0) := by
507 intro i
508 simp [Pi.single_apply]
509 rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]
510
511lemma pderivQ_DgenSym (a j : ZMod n) (x : PhaseSpace n) :
512 pderivQ (DgenSym a) j x = (x.2 (j - a) - x.2 (j + a)) / 2 := by
513 rw [pderivQ, (hasFDerivAt_DgenSym a x).fderiv, DgenSymD, ContinuousLinearMap.sum_apply]
514 have step : ∀ i : ZMod n,
515 ((1 / 2 : ℝ) • (x.2 i • (coordQ (i + a) - coordQ (i - a))
516 + (x.1 (i + a) - x.1 (i - a)) • coordP i))
517 ((Pi.single j 1, 0) : PhaseSpace n)
518 = (x.2 i / 2) * (if i + a = j then (1 : ℝ) else 0)
519 - (x.2 i / 2) * (if i - a = j then (1 : ℝ) else 0) := by
520 intro i
521 simp [Pi.single_apply, mul_sub]
522 ring
523 rw [Finset.sum_congr rfl fun i _ => step i, Finset.sum_sub_distrib,
524 sum_mul_ite_add, sum_mul_ite_sub]
525 ring
526
527lemma pderivP_DgenSym (a j : ZMod n) (x : PhaseSpace n) :
528 pderivP (DgenSym a) j x = (x.1 (j + a) - x.1 (j - a)) / 2 := by
529 rw [pderivP, (hasFDerivAt_DgenSym a x).fderiv, DgenSymD, ContinuousLinearMap.sum_apply]
530 have step : ∀ i : ZMod n,
531 ((1 / 2 : ℝ) • (x.2 i • (coordQ (i + a) - coordQ (i - a))
532 + (x.1 (i + a) - x.1 (i - a)) • coordP i))
533 ((0, Pi.single j 1) : PhaseSpace n)
534 = ((x.1 (i + a) - x.1 (i - a)) / 2) * (if i = j then (1 : ℝ) else 0) := by
535 intro i
536 simp [Pi.single_apply]
537 ring
538 rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]
539
540lemma pderivP_Ham (N : ZMod n → ℝ) (j : ZMod n) (x : PhaseSpace n) :
541 pderivP (Ham N) j x = N j * x.2 j := by
542 rw [pderivP, (hasFDerivAt_Ham N x).fderiv, HamD, ContinuousLinearMap.sum_apply]
543 have step : ∀ i : ZMod n,
544 (((N i / 2) • ((x.2 i • coordP i + x.2 i • coordP i)
545 + ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)
546 + (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i))) :
547 PhaseSpace n →L[ℝ] ℝ))
548 ((0, Pi.single j 1) : PhaseSpace n)
549 = (N i * x.2 i) * (if i = j then (1 : ℝ) else 0) := by
550 intro i
551 simp [Pi.single_apply]
552 split_ifs <;> ring
553 rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]
554
555lemma pderivQ_Ham (N : ZMod n → ℝ) (j : ZMod n) (x : PhaseSpace n) :
556 pderivQ (Ham N) j x
557 = N (j - 1) * (x.1 j - x.1 (j - 1)) - N j * (x.1 (j + 1) - x.1 j) := by
558 rw [pderivQ, (hasFDerivAt_Ham N x).fderiv, HamD, ContinuousLinearMap.sum_apply]
559 have step : ∀ i : ZMod n,
560 (((N i / 2) • ((x.2 i • coordP i + x.2 i • coordP i)
561 + ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)
562 + (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i))) :
563 PhaseSpace n →L[ℝ] ℝ))
564 ((Pi.single j 1, 0) : PhaseSpace n)
565 = (N i * (x.1 (i + 1) - x.1 i)) * (if i + 1 = j then (1 : ℝ) else 0)
566 - (N i * (x.1 (i + 1) - x.1 i)) * (if i = j then (1 : ℝ) else 0) := by
567 intro i
568 simp [Pi.single_apply, mul_sub]
569 split_ifs <;> ring
570 rw [Finset.sum_congr rfl fun i _ => step i, Finset.sum_sub_distrib,
571 sum_mul_ite_add, sum_mul_ite]
572 have e : j - 1 + 1 = j := by ring
573 rw [e]
574
575/-! ## Closure of the momentum (diffeomorphism) sector
576
577The translation group of the periodic lattice is abelian; the sharp statement
578is that the bracket of any two shift generators vanishes identically. -/
579
580/-- THEOREM (momentum sector closes, sharp form). `{D_a, D_b} = 0` for all
581lattice displacements `a, b` and every phase-space point. Derived by explicit
582computation: after the Kronecker collapse the eight monomial sums cancel in
583pairs under the reindexings `j ↦ j + a` and `j ↦ j + b`. -/
584theorem bracket_Dgen_Dgen (a b : ZMod n) (x : PhaseSpace n) :
585 bracket (Dgen a) (Dgen b) x = 0 := by
586 simp only [bracket, pderivQ_Dgen, pderivP_Dgen]
587 have h1 : (∑ j : ZMod n, x.2 (j - a) * x.1 (j + b))
588 = ∑ j : ZMod n, x.2 j * x.1 (j + (a + b)) := by
589 refine sum_reindex a (fun k => x.2 (k - a) * x.1 (k + b)) _ fun j => ?_
590 have e1 : j + a - a = j := by ring
591 have e2 : j + a + b = j + (a + b) := by ring
592 simp only [e1, e2]
593 have h2 : (∑ j : ZMod n, x.2 (j - a) * x.1 j)
594 = ∑ j : ZMod n, x.2 j * x.1 (j + a) := by
595 refine sum_reindex a (fun k => x.2 (k - a) * x.1 k) _ fun j => ?_
596 have e1 : j + a - a = j := by ring
597 simp only [e1]
598 have h3 : (∑ j : ZMod n, x.2 (j - b) * x.1 (j + a))
599 = ∑ j : ZMod n, x.2 j * x.1 (j + (a + b)) := by
600 refine sum_reindex b (fun k => x.2 (k - b) * x.1 (k + a)) _ fun j => ?_
601 have e1 : j + b - b = j := by ring
602 have e2 : j + b + a = j + (a + b) := by ring
603 simp only [e1, e2]
604 have h4 : (∑ j : ZMod n, x.2 (j - b) * x.1 j)
605 = ∑ j : ZMod n, x.2 j * x.1 (j + b) := by
606 refine sum_reindex b (fun k => x.2 (k - b) * x.1 k) _ fun j => ?_
607 have e1 : j + b - b = j := by ring
608 simp only [e1]
609 have decomp : (∑ j : ZMod n, ((x.2 (j - a) - x.2 j) * (x.1 (j + b) - x.1 j)
610 - (x.1 (j + a) - x.1 j) * (x.2 (j - b) - x.2 j)))
611 = ((∑ j : ZMod n, x.2 (j - a) * x.1 (j + b))
612 - (∑ j : ZMod n, x.2 (j - a) * x.1 j)
613 - (∑ j : ZMod n, x.2 j * x.1 (j + b)))
614 - ((∑ j : ZMod n, x.2 (j - b) * x.1 (j + a))
615 - (∑ j : ZMod n, x.2 (j - b) * x.1 j)
616 - (∑ j : ZMod n, x.2 j * x.1 (j + a))) := by
617 simp only [← Finset.sum_sub_distrib]
618 exact Finset.sum_congr rfl fun j _ => by ring
619 rw [decomp, h1, h2, h3, h4]
620 ring
621
622/-- THEOREM (momentum sector closes, symmetric discretization).
623`{Dsym_a, Dsym_b} = 0`. -/
624theorem bracket_DgenSym_DgenSym (a b : ZMod n) (x : PhaseSpace n) :
625 bracket (DgenSym a) (DgenSym b) x = 0 := by
626 simp only [bracket, pderivQ_DgenSym, pderivP_DgenSym]
627 have h1 : (∑ j : ZMod n, x.2 (j - a) * x.1 (j + b))
628 = ∑ j : ZMod n, x.2 j * x.1 (j + (a + b)) := by
629 refine sum_reindex a (fun k => x.2 (k - a) * x.1 (k + b)) _ fun j => ?_
630 have e1 : j + a - a = j := by ring
631 have e2 : j + a + b = j + (a + b) := by ring
632 simp only [e1, e2]
633 have h2 : (∑ j : ZMod n, x.2 (j - a) * x.1 (j - b))
634 = ∑ j : ZMod n, x.2 j * x.1 (j + (a - b)) := by
635 refine sum_reindex a (fun k => x.2 (k - a) * x.1 (k - b)) _ fun j => ?_
636 have e1 : j + a - a = j := by ring
637 have e2 : j + a - b = j + (a - b) := by ring
638 simp only [e1, e2]
639 have h3 : (∑ j : ZMod n, x.2 (j + a) * x.1 (j + b))
640 = ∑ j : ZMod n, x.2 j * x.1 (j + (b - a)) := by
641 refine sum_reindex (-a) (fun k => x.2 (k + a) * x.1 (k + b)) _ fun j => ?_
642 have e1 : j + -a + a = j := by ring
643 have e2 : j + -a + b = j + (b - a) := by ring
644 simp only [e1, e2]
645 have h4 : (∑ j : ZMod n, x.2 (j + a) * x.1 (j - b))
646 = ∑ j : ZMod n, x.2 j * x.1 (j - (a + b)) := by
647 refine sum_reindex (-a) (fun k => x.2 (k + a) * x.1 (k - b)) _ fun j => ?_
648 have e1 : j + -a + a = j := by ring
649 have e2 : j + -a - b = j - (a + b) := by ring
650 simp only [e1, e2]
651 have h5 : (∑ j : ZMod n, x.2 (j - b) * x.1 (j + a))
652 = ∑ j : ZMod n, x.2 j * x.1 (j + (a + b)) := by
653 refine sum_reindex b (fun k => x.2 (k - b) * x.1 (k + a)) _ fun j => ?_
654 have e1 : j + b - b = j := by ring
655 have e2 : j + b + a = j + (a + b) := by ring
656 simp only [e1, e2]
657 have h6 : (∑ j : ZMod n, x.2 (j + b) * x.1 (j + a))
658 = ∑ j : ZMod n, x.2 j * x.1 (j + (a - b)) := by
659 refine sum_reindex (-b) (fun k => x.2 (k + b) * x.1 (k + a)) _ fun j => ?_
660 have e1 : j + -b + b = j := by ring
661 have e2 : j + -b + a = j + (a - b) := by ring
662 simp only [e1, e2]
663 have h7 : (∑ j : ZMod n, x.2 (j - b) * x.1 (j - a))
664 = ∑ j : ZMod n, x.2 j * x.1 (j + (b - a)) := by
665 refine sum_reindex b (fun k => x.2 (k - b) * x.1 (k - a)) _ fun j => ?_
666 have e1 : j + b - b = j := by ring
667 have e2 : j + b - a = j + (b - a) := by ring
668 simp only [e1, e2]
669 have h8 : (∑ j : ZMod n, x.2 (j + b) * x.1 (j - a))
670 = ∑ j : ZMod n, x.2 j * x.1 (j - (a + b)) := by
671 refine sum_reindex (-b) (fun k => x.2 (k + b) * x.1 (k - a)) _ fun j => ?_
672 have e1 : j + -b + b = j := by ring
673 have e2 : j + -b - a = j - (a + b) := by ring
674 simp only [e1, e2]
675 have decomp : (∑ j : ZMod n,
676 ((x.2 (j - a) - x.2 (j + a)) / 2 * ((x.1 (j + b) - x.1 (j - b)) / 2)
677 - (x.1 (j + a) - x.1 (j - a)) / 2 * ((x.2 (j - b) - x.2 (j + b)) / 2)))
678 = (((∑ j : ZMod n, x.2 (j - a) * x.1 (j + b))
679 - (∑ j : ZMod n, x.2 (j - a) * x.1 (j - b))
680 - (∑ j : ZMod n, x.2 (j + a) * x.1 (j + b))
681 + (∑ j : ZMod n, x.2 (j + a) * x.1 (j - b)))
682 - ((∑ j : ZMod n, x.2 (j - b) * x.1 (j + a))
683 - (∑ j : ZMod n, x.2 (j - b) * x.1 (j - a))
684 - (∑ j : ZMod n, x.2 (j + b) * x.1 (j + a))
685 + (∑ j : ZMod n, x.2 (j + b) * x.1 (j - a)))) / 4 := by
686 simp only [← Finset.sum_sub_distrib, ← Finset.sum_add_distrib, Finset.sum_div]
687 exact Finset.sum_congr rfl fun j _ => by ring
688 rw [decomp, h1, h2, h3, h4, h5, h6, h7, h8]
689 ring
690
691/-! ## Momentum-Hamiltonian sector -/
692
693/-- THEOREM (general lapse, forward difference: the TRUE identity).
694`{D_a, H[N]} = sum_j N_j (pi_j (pi_{j-a} - pi_j) + d_j (d_j - d_{j+a}))`
695where `d_j = q_{j+1} - q_j`. Derived by explicit computation; note it is NOT of
696the advected-lapse form: the one-sided difference generator does not represent
697lattice translations exactly. -/
698theorem bracket_Dgen_Ham (a : ZMod n) (N : ZMod n → ℝ) (x : PhaseSpace n) :
699 bracket (Dgen a) (Ham N) x
700 = ∑ j : ZMod n, N j * (x.2 j * (x.2 (j - a) - x.2 j)
701 + (x.1 (j + 1) - x.1 j)
702 * ((x.1 (j + 1) - x.1 j) - (x.1 (j + a + 1) - x.1 (j + a)))) := by
703 simp only [bracket, pderivQ_Dgen, pderivP_Dgen, pderivQ_Ham, pderivP_Ham]
704 have decomp1 : (∑ j : ZMod n, ((x.2 (j - a) - x.2 j) * (N j * x.2 j)
705 - (x.1 (j + a) - x.1 j)
706 * (N (j - 1) * (x.1 j - x.1 (j - 1)) - N j * (x.1 (j + 1) - x.1 j))))
707 = (∑ j : ZMod n, ((x.2 (j - a) - x.2 j) * (N j * x.2 j)
708 + (x.1 (j + a) - x.1 j) * (N j * (x.1 (j + 1) - x.1 j))))
709 - (∑ j : ZMod n, (x.1 (j + a) - x.1 j) * (N (j - 1) * (x.1 j - x.1 (j - 1)))) := by
710 simp only [← Finset.sum_sub_distrib]
711 exact Finset.sum_congr rfl fun j _ => by ring
712 rw [decomp1]
713 have hshift : (∑ j : ZMod n, (x.1 (j + a) - x.1 j) * (N (j - 1) * (x.1 j - x.1 (j - 1))))
714 = ∑ j : ZMod n, (x.1 (j + a + 1) - x.1 (j + 1)) * (N j * (x.1 (j + 1) - x.1 j)) := by
715 refine sum_reindex 1
716 (fun k => (x.1 (k + a) - x.1 k) * (N (k - 1) * (x.1 k - x.1 (k - 1)))) _ fun j => ?_
717 have e1 : j + 1 - 1 = j := by ring
718 have e2 : j + 1 + a = j + a + 1 := by ring
719 simp only [e1, e2]
720 rw [hshift, ← Finset.sum_sub_distrib]
721 exact Finset.sum_congr rfl fun j _ => by ring
722
723/-- THEOREM (constant lapse: the exact closure ANOMALY of the forward
724difference). `{D_a, H[1]} = (1/2) sum_j ((d_{j+a} - d_j)^2 - (pi_{j+a} - pi_j)^2)`.
725This is generically nonzero: the naive one-sided discretization of the momentum
726constraint does not commute with the constant-lapse Hamiltonian. The obstruction
727is an explicit lattice artifact, quadratic in the `a`-step differences of the
728field gradient `d` and the momentum `pi`; it vanishes identically on
729shift-invariant configurations. This theorem corrects the naive expectation
730`{H[1], D_a} = 0` (which DOES hold for the symmetric generator, see
731`bracket_DgenSym_Ham_one`). -/
732theorem bracket_Dgen_Ham_one (a : ZMod n) (x : PhaseSpace n) :
733 bracket (Dgen a) (Ham (fun _ => 1)) x
734 = (∑ j : ZMod n,
735 (((x.1 (j + a + 1) - x.1 (j + a)) - (x.1 (j + 1) - x.1 j)) ^ 2
736 - (x.2 (j + a) - x.2 j) ^ 2)) / 2 := by
737 simp only [bracket_Dgen_Ham, one_mul]
738 have hP1 : (∑ j : ZMod n, x.2 j * x.2 (j - a))
739 = ∑ j : ZMod n, x.2 (j + a) * x.2 j := by
740 refine sum_reindex a (fun k => x.2 k * x.2 (k - a)) _ fun j => ?_
741 have e1 : j + a - a = j := by ring
742 simp only [e1]
743 have hP2 : (∑ j : ZMod n, x.2 j * x.2 j)
744 = ∑ j : ZMod n, x.2 (j + a) * x.2 (j + a) :=
745 sum_reindex a (fun k => x.2 k * x.2 k) _ fun j => rfl
746 have hQ1 : (∑ j : ZMod n, (x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))
747 = ∑ j : ZMod n, (x.1 (j + a + 1) - x.1 (j + a)) * (x.1 (j + a + 1) - x.1 (j + a)) :=
748 sum_reindex a (fun k => (x.1 (k + 1) - x.1 k) * (x.1 (k + 1) - x.1 k)) _ fun j => rfl
749 have decompL : (∑ j : ZMod n, (x.2 j * (x.2 (j - a) - x.2 j)
750 + (x.1 (j + 1) - x.1 j)
751 * ((x.1 (j + 1) - x.1 j) - (x.1 (j + a + 1) - x.1 (j + a)))))
752 = ((∑ j : ZMod n, x.2 j * x.2 (j - a)) - (∑ j : ZMod n, x.2 j * x.2 j))
753 + ((∑ j : ZMod n, (x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))
754 - (∑ j : ZMod n,
755 (x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a)))) := by
756 simp only [← Finset.sum_sub_distrib, ← Finset.sum_add_distrib]
757 exact Finset.sum_congr rfl fun j _ => by ring
758 have decompR : (∑ j : ZMod n,
759 (((x.1 (j + a + 1) - x.1 (j + a)) - (x.1 (j + 1) - x.1 j)) ^ 2
760 - (x.2 (j + a) - x.2 j) ^ 2))
761 = ((∑ j : ZMod n, (x.1 (j + a + 1) - x.1 (j + a)) * (x.1 (j + a + 1) - x.1 (j + a)))
762 - 2 * (∑ j : ZMod n, (x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a)))
763 + (∑ j : ZMod n, (x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)))
764 - ((∑ j : ZMod n, x.2 (j + a) * x.2 (j + a))
765 - 2 * (∑ j : ZMod n, x.2 (j + a) * x.2 j)
766 + (∑ j : ZMod n, x.2 j * x.2 j)) := by
767 simp only [Finset.mul_sum, ← Finset.sum_sub_distrib, ← Finset.sum_add_distrib]
768 exact Finset.sum_congr rfl fun j _ => by ring
769 rw [decompL, decompR, ← hQ1, ← hP2, ← hP1]
770 ring
771
772/-- THEOREM (exact discrete advection / hypersurface deformation, momentum vs
773Hamiltonian). For the symmetric-difference generator the bracket with the
774smeared Hamiltonian is EXACTLY the point-split Hamiltonian density smeared by
775the discrete derivative of the lapse:
776`{Dsym_a, H[N]} = (1/2) sum_j (N_{j+a} - N_j) (pi_j pi_{j+a} + d_j d_{j+a})`.
777For constant lapse the right side vanishes identically
778(`bracket_DgenSym_Ham_one`): the symmetric discretization restores exact
779translation closure. In the continuum limit `N_{j+a} - N_j` tends to `a N'` and
780the point-split density tends to `pi^2 + (q')^2`, recovering the Dirac relation
781`{D(xi), H(N)} = H(xi N')` on this rung. -/
782theorem bracket_DgenSym_Ham (a : ZMod n) (N : ZMod n → ℝ) (x : PhaseSpace n) :
783 bracket (DgenSym a) (Ham N) x
784 = (∑ j : ZMod n, (N (j + a) - N j)
785 * (x.2 j * x.2 (j + a)
786 + (x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a)))) / 2 := by
787 simp only [bracket, pderivQ_DgenSym, pderivP_DgenSym, pderivQ_Ham, pderivP_Ham]
788 -- Stage 1: split off the `N (j-1)` piece and reindex it by one lattice step.
789 have decompL : (∑ j : ZMod n, ((x.2 (j - a) - x.2 (j + a)) / 2 * (N j * x.2 j)
790 - (x.1 (j + a) - x.1 (j - a)) / 2
791 * (N (j - 1) * (x.1 j - x.1 (j - 1)) - N j * (x.1 (j + 1) - x.1 j))))
792 = ((∑ j : ZMod n, N j * (x.2 j * x.2 (j - a)))
793 - (∑ j : ZMod n, N j * (x.2 j * x.2 (j + a)))
794 + (∑ j : ZMod n,
795 (x.1 (j + a) - x.1 (j - a)) * (N j * (x.1 (j + 1) - x.1 j)))
796 - (∑ j : ZMod n,
797 (x.1 (j + a) - x.1 (j - a)) * (N (j - 1) * (x.1 j - x.1 (j - 1))))) / 2 := by
798 simp only [← Finset.sum_sub_distrib, ← Finset.sum_add_distrib, Finset.sum_div]
799 exact Finset.sum_congr rfl fun j _ => by ring
800 rw [decompL]
801 have hshift : (∑ j : ZMod n,
802 (x.1 (j + a) - x.1 (j - a)) * (N (j - 1) * (x.1 j - x.1 (j - 1))))
803 = ∑ j : ZMod n,
804 (x.1 (j + a + 1) - x.1 (j - a + 1)) * (N j * (x.1 (j + 1) - x.1 j)) := by
805 refine sum_reindex 1
806 (fun k => (x.1 (k + a) - x.1 (k - a)) * (N (k - 1) * (x.1 k - x.1 (k - 1)))) _
807 fun j => ?_
808 have e1 : j + 1 - 1 = j := by ring
809 have e2 : j + 1 + a = j + a + 1 := by ring
810 have e3 : j + 1 - a = j - a + 1 := by ring
811 simp only [e1, e2, e3]
812 rw [hshift]
813 -- Stage 2: reindex the two back-shifted sums to canonical forward form.
814 have hpi : (∑ j : ZMod n, N j * (x.2 j * x.2 (j - a)))
815 = ∑ j : ZMod n, N (j + a) * (x.2 j * x.2 (j + a)) := by
816 refine sum_reindex a (fun k => N k * (x.2 k * x.2 (k - a))) _ fun j => ?_
817 have e1 : j + a - a = j := by ring
818 simp only [e1]
819 ring
820 rw [hpi]
821 -- Stage 3: convert the two q-sums into point-split gradient sums.
822 have decompQ : (∑ j : ZMod n,
823 (x.1 (j + a) - x.1 (j - a)) * (N j * (x.1 (j + 1) - x.1 j)))
824 - (∑ j : ZMod n,
825 (x.1 (j + a + 1) - x.1 (j - a + 1)) * (N j * (x.1 (j + 1) - x.1 j)))
826 = (∑ j : ZMod n,
827 N j * ((x.1 (j + 1) - x.1 j) * (x.1 (j - a + 1) - x.1 (j - a))))
828 - (∑ j : ZMod n,
829 N j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a)))) := by
830 simp only [← Finset.sum_sub_distrib]
831 exact Finset.sum_congr rfl fun j _ => by ring
832 have hgrad : (∑ j : ZMod n,
833 N j * ((x.1 (j + 1) - x.1 j) * (x.1 (j - a + 1) - x.1 (j - a))))
834 = ∑ j : ZMod n,
835 N (j + a) * ((x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a))) := by
836 refine sum_reindex a
837 (fun k => N k * ((x.1 (k + 1) - x.1 k) * (x.1 (k - a + 1) - x.1 (k - a)))) _
838 fun j => ?_
839 have e1 : j + a - a = j := by ring
840 simp only [e1]
841 ring
842 have decompR : (∑ j : ZMod n, (N (j + a) - N j)
843 * (x.2 j * x.2 (j + a)
844 + (x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a))))
845 = ((∑ j : ZMod n, N (j + a) * (x.2 j * x.2 (j + a)))
846 - (∑ j : ZMod n, N j * (x.2 j * x.2 (j + a))))
847 + ((∑ j : ZMod n,
848 N (j + a) * ((x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a))))
849 - (∑ j : ZMod n,
850 N j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + a + 1) - x.1 (j + a))))) := by
851 simp only [← Finset.sum_sub_distrib, ← Finset.sum_add_distrib]
852 exact Finset.sum_congr rfl fun j _ => by ring
853 rw [decompR]
854 have key := decompQ
855 rw [hgrad] at key
856 linarith [key]
857
858/-- THEOREM. Constant lapse: the symmetric-difference momentum generator
859commutes exactly with the Hamiltonian, `{Dsym_a, H[1]} = 0` (exact discrete
860translation invariance). -/
861theorem bracket_DgenSym_Ham_one (a : ZMod n) (x : PhaseSpace n) :
862 bracket (DgenSym a) (Ham (fun _ => 1)) x = 0 := by
863 rw [bracket_DgenSym_Ham]
864 simp
865
866/-- THEOREM. `{H[1], Dsym_a} = 0` (the flipped orientation, via antisymmetry). -/
867theorem bracket_Ham_one_DgenSym (a : ZMod n) (x : PhaseSpace n) :
868 bracket (Ham (fun _ => 1)) (DgenSym a) x = 0 := by
869 rw [bracket_antisymm, bracket_DgenSym_Ham_one, neg_zero]
870
871/-! ## Hamiltonian-Hamiltonian sector: the hypersurface-deformation relation -/
872
873/-- THEOREM (discrete hypersurface-deformation relation).
874`{H[N], H[M]} = sum_j (N_j M_{j+1} - M_j N_{j+1}) * pi_{j+1} (q_{j+1} - q_j)`.
875The bracket of two Hamiltonian deformations is a D-type (momentum) generator:
876a point-split momentum density `pi_{j+1} (q_{j+1} - q_j)` smeared by the
877discrete Wronskian `N_j M_{j+1} - M_j N_{j+1}` of the two lapses. In the
878continuum limit the Wronskian tends to `(N M' - M N') dx` and the density to
879`pi q'`, which is the Dirac algebra relation `{H(N), H(M)} = D(N M' - M N')`;
880the structure function (the inverse spatial metric in full gravity) is frozen
881to 1 on this flat scalar rung. Antisymmetric in `N, M` by inspection, and it
882vanishes identically for `N = M`. -/
883theorem bracket_Ham_Ham (N M : ZMod n → ℝ) (x : PhaseSpace n) :
884 bracket (Ham N) (Ham M) x
885 = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
886 * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
887 simp only [bracket, pderivQ_Ham, pderivP_Ham]
888 have step1 : (∑ j : ZMod n,
889 ((N (j - 1) * (x.1 j - x.1 (j - 1)) - N j * (x.1 (j + 1) - x.1 j)) * (M j * x.2 j)
890 - N j * x.2 j
891 * (M (j - 1) * (x.1 j - x.1 (j - 1)) - M j * (x.1 (j + 1) - x.1 j))))
892 = ∑ j : ZMod n,
893 (N (j - 1) * M j - M (j - 1) * N j) * (x.2 j * (x.1 j - x.1 (j - 1))) :=
894 Finset.sum_congr rfl fun j _ => by ring
895 rw [step1]
896 refine sum_reindex 1
897 (fun k => (N (k - 1) * M k - M (k - 1) * N k) * (x.2 k * (x.1 k - x.1 (k - 1)))) _
898 fun j => ?_
899 have e1 : j + 1 - 1 = j := by ring
900 simp only [e1]
901
902end
903
904/-! ## The Hojman-Kuchar-Teitelboim target (honesty layer)
905
906The HKT theorem (Hojman, Kuchar, Teitelboim 1976) says: a representation of the
907hypersurface-deformation (Dirac) algebra on a metric phase space, by local
908covariant constraint densities with the metric-dependent structure function in
909the `{H, H}` bracket, forces the Hamiltonian constraint to have the
910Einstein-Hilbert (ADM) form up to Newton and cosmological constants. The
911structure below names lattice renderings of the exact hypotheses as Prop-valued
912fields with real mathematical content. It is deliberately NOT inhabited in this
913file: the concrete generators above realize `mom_mom` exactly but satisfy the
914`mom_ham` and `ham_ham` relations only in point-split form (the density
915evaluated at split lattice points, see `bracket_DgenSym_Ham` and
916`bracket_Ham_Ham`), and closing that gap, together with the continuum limit and
917the rigidity implication `HKTRigidityStatement`, remains OPEN. -/
918
919/-- OPEN TARGET (deliberately uninhabited). The hypotheses of the
920Hojman-Kuchar-Teitelboim theorem, rendered on the periodic lattice: local,
921translation-covariant Hamiltonian and momentum densities whose smeared
922generators represent the hypersurface-deformation algebra: abelian momentum
923sector (`mom_mom`), lapse advection (`mom_ham`), and the `{H, H}` relation
924closing on the momentum density with the Wronskian smearing (`ham_ham`; the
925structure function is 1 on this flat scalar rung, in full gravity it is the
926inverse spatial metric). Every field is a real mathematical statement; none is
927`True` and no instance is provided anywhere in this file. -/
928structure HojmanKucharTeitelboimTarget (n : ℕ) [NeZero n] where
929 /-- The local Hamiltonian-constraint density `h_j[q, pi]`. -/
930 hamDensity : PhaseSpace n → ZMod n → ℝ
931 /-- The local momentum-constraint density `p_j[q, pi]`. -/
932 momDensity : PhaseSpace n → ZMod n → ℝ
933 /-- Smeared Hamiltonian generators are differentiable observables. -/
934 ham_differentiable : ∀ N : ZMod n → ℝ,
935 Differentiable ℝ (fun x : PhaseSpace n => ∑ j : ZMod n, N j * hamDensity x j)
936 /-- Smeared momentum generators are differentiable observables. -/
937 mom_differentiable : ∀ w : ZMod n → ℝ,
938 Differentiable ℝ (fun x : PhaseSpace n => ∑ j : ZMod n, w j * momDensity x j)
939 /-- Locality: the Hamiltonian density at site `j` depends only on the field
940 in the elementary cell `{j, j+1}` and the momentum at `j`. -/
941 ham_local : ∀ (x y : PhaseSpace n) (j : ZMod n),
942 x.1 j = y.1 j → x.1 (j + 1) = y.1 (j + 1) → x.2 j = y.2 j →
943 hamDensity x j = hamDensity y j
944 /-- Translation covariance of the Hamiltonian density. -/
945 ham_covariant : ∀ (x : PhaseSpace n) (a j : ZMod n),
946 hamDensity (fun i => x.1 (i + a), fun i => x.2 (i + a)) j = hamDensity x (j + a)
947 /-- Dirac relation 1: the smeared momentum sector is abelian. -/
948 mom_mom : ∀ (v w : ZMod n → ℝ) (x : PhaseSpace n),
949 bracket (fun y => ∑ j : ZMod n, v j * momDensity y j)
950 (fun y => ∑ j : ZMod n, w j * momDensity y j) x = 0
951 /-- Dirac relation 2: the momentum generator advects the lapse,
952 `{D[w], H[N]} = H[w * (discrete derivative of N)]`. -/
953 mom_ham : ∀ (w N : ZMod n → ℝ) (x : PhaseSpace n),
954 bracket (fun y => ∑ j : ZMod n, w j * momDensity y j)
955 (fun y => ∑ j : ZMod n, N j * hamDensity y j) x
956 = ∑ j : ZMod n, (w j * (N (j + 1) - N j)) * hamDensity x j
957 /-- Dirac relation 3 (hypersurface deformation): two Hamiltonian deformations
958 close on the momentum density smeared by the discrete Wronskian of the
959 lapses. -/
960 ham_ham : ∀ (N M : ZMod n → ℝ) (x : PhaseSpace n),
961 bracket (fun y => ∑ j : ZMod n, N j * hamDensity y j)
962 (fun y => ∑ j : ZMod n, M j * hamDensity y j) x
963 = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1)) * momDensity x j
964
965/-- OPEN. The HKT rigidity statement on this rung: any representation of the
966hypersurface-deformation algebra in the sense of `HojmanKucharTeitelboimTarget`
967has a Hamiltonian density of the canonical (wave / Einstein-Hilbert-form)
968shape, kinetic plus gradient-squared plus a vacuum constant. This Prop is
969DEFINED here so the target is precise; it is neither proved nor assumed
970anywhere in this file, and no axiom about it is introduced. -/
971def HKTRigidityStatement (n : ℕ) [NeZero n] : Prop :=
972 ∀ T : HojmanKucharTeitelboimTarget n,
973 ∃ cKin cGrad cVac : ℝ, ∀ (x : PhaseSpace n) (j : ZMod n),
974 T.hamDensity x j
975 = cKin * (x.2 j * x.2 j)
976 + cGrad * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)) + cVac
977
978end HypersurfaceDeformation
979end SevenGaps
980end Gravity
981end IndisputableMonolith
982