IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation

   1import IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation
   2
   3/-!
   4# Wave C2 R5/R6 groundwork: local-profile functional equation (n = 2)
   5
   6Landed at n = 2 (mirrors HamDyn). Reduces Dyn ham_ham for local profiles to
   7momDensity_j = h_b(j) * h_p(j+1). R6 attack surface; nothing proves rigidity.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Gravity
  12namespace SevenGaps
  13namespace HKTLocalFunctionalEquation
  14
  15open HypersurfaceDeformation
  16
  17noncomputable section
  18
  19open Finset
  20
  21abbrev LocalHamProfile : Type := ℝ → ℝ → ℝ → ℝ
  22
  23def LocalHamFromProfile (h : LocalHamProfile) (N : ZMod 2 → ℝ)
  24    (x : PhaseSpace 2) : ℝ :=
  25  ∑ j : ZMod 2, N j * h (x.1 j) (x.1 (j + 1)) (x.2 j)
  26
  27structure LocalHamSmooth (h : LocalHamProfile) where
  28  ha : LocalHamProfile
  29  hb : LocalHamProfile
  30  hp : LocalHamProfile
  31  hasFDerivCell :
  32    ∀ (j : ZMod 2) (x : PhaseSpace 2),
  33      HasFDerivAt (fun y : PhaseSpace 2 => h (y.1 j) (y.1 (j + 1)) (y.2 j))
  34        ((ha (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
  35          (hb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
  36          (hp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j)
  37        x
  38
  39def localCellD (h : LocalHamProfile) (S : LocalHamSmooth h) (j : ZMod 2)
  40    (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
  41  (S.ha (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ j +
  42    (S.hb (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordQ (j + 1) +
  43    (S.hp (x.1 j) (x.1 (j + 1)) (x.2 j)) • coordP j
  44
  45lemma hasFDerivAt_localCell (h : LocalHamProfile) (S : LocalHamSmooth h)
  46    (j : ZMod 2) (x : PhaseSpace 2) :
  47    HasFDerivAt (fun y : PhaseSpace 2 => h (y.1 j) (y.1 (j + 1)) (y.2 j))
  48      (localCellD h S j x) x :=
  49  S.hasFDerivCell j x
  50
  51def LocalHamFromProfileD (h : LocalHamProfile) (S : LocalHamSmooth h)
  52    (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
  53  ∑ j : ZMod 2, (N j) • localCellD h S j x
  54
  55lemma hasFDerivAt_LocalHamFromProfile (h : LocalHamProfile) (S : LocalHamSmooth h)
  56    (N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
  57    HasFDerivAt (LocalHamFromProfile h N) (LocalHamFromProfileD h S N x) x := by
  58  unfold LocalHamFromProfile LocalHamFromProfileD
  59  exact HasFDerivAt.fun_sum fun j _ =>
  60    (hasFDerivAt_localCell h S j x).const_mul (N j)
  61
  62theorem differentiable_LocalHamFromProfile (h : LocalHamProfile)
  63    (S : LocalHamSmooth h) (N : ZMod 2 → ℝ) :
  64    Differentiable ℝ (LocalHamFromProfile h N) :=
  65  fun x => (hasFDerivAt_LocalHamFromProfile h S N x).differentiableAt
  66
  67private lemma cellD_pdir (h : LocalHamProfile) (S : LocalHamSmooth h)
  68    (j k : ZMod 2) (x : PhaseSpace 2) :
  69    localCellD h S j x (0, Pi.single k 1)
  70      = S.hp (x.1 j) (x.1 (j + 1)) (x.2 j) * (if j = k then (1 : ℝ) else 0) := by
  71  simp only [localCellD, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
  72    coordQ_apply, coordP_apply, Pi.single_apply]
  73  by_cases hjk : j = k <;> simp [hjk]
  74
  75private lemma cellD_qdir (h : LocalHamProfile) (S : LocalHamSmooth h)
  76    (j k : ZMod 2) (x : PhaseSpace 2) :
  77    localCellD h S j x (Pi.single k 1, 0)
  78      = S.ha (x.1 j) (x.1 (j + 1)) (x.2 j) * (if j = k then (1 : ℝ) else 0)
  79        + S.hb (x.1 j) (x.1 (j + 1)) (x.2 j) * (if j + 1 = k then (1 : ℝ) else 0) := by
  80  simp only [localCellD, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
  81    coordQ_apply, coordP_apply, Pi.single_apply]
  82  by_cases hjk : j = k
  83  · subst hjk
  84    have hjp : (j + 1 : ZMod 2) ≠ j := by
  85      intro h
  86      have : (1 : ZMod 2) = 0 := by
  87        calc (1 : ZMod 2) = j + 1 - j := by ring
  88          _ = j - j := by rw [h]
  89          _ = 0 := by ring
  90      exact absurd this (by decide)
  91    simp [hjp]
  92  · by_cases hjp : j + 1 = k
  93    · simp [hjk, hjp]
  94    · simp [hjk, hjp]
  95
  96theorem pderivP_LocalHamFromProfile (h : LocalHamProfile) (S : LocalHamSmooth h)
  97    (N : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
  98    pderivP (LocalHamFromProfile h N) k x
  99      = N k * S.hp (x.1 k) (x.1 (k + 1)) (x.2 k) := by
 100  rw [pderivP, (hasFDerivAt_LocalHamFromProfile h S N x).fderiv,
 101    LocalHamFromProfileD, ContinuousLinearMap.sum_apply]
 102  have step : ∀ j : ZMod 2,
 103      (((N j) • localCellD h S j x : PhaseSpace 2 →L[ℝ] ℝ)
 104        ((0, Pi.single k 1) : PhaseSpace 2))
 105      = (N j * S.hp (x.1 j) (x.1 (j + 1)) (x.2 j)) *
 106          (if j = k then (1 : ℝ) else 0) := by
 107    intro j
 108    simp only [ContinuousLinearMap.smul_apply, cellD_pdir, smul_eq_mul]
 109    ring
 110  rw [Finset.sum_congr rfl fun j _ => step j, sum_mul_ite]
 111
 112theorem pderivQ_LocalHamFromProfile (h : LocalHamProfile) (S : LocalHamSmooth h)
 113    (N : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
 114    pderivQ (LocalHamFromProfile h N) k x
 115      = N k * S.ha (x.1 k) (x.1 (k + 1)) (x.2 k)
 116        + N (k - 1) * S.hb (x.1 (k - 1)) (x.1 k) (x.2 (k - 1)) := by
 117  rw [pderivQ, (hasFDerivAt_LocalHamFromProfile h S N x).fderiv,
 118    LocalHamFromProfileD, ContinuousLinearMap.sum_apply]
 119  have step : ∀ j : ZMod 2,
 120      (((N j) • localCellD h S j x : PhaseSpace 2 →L[ℝ] ℝ)
 121        ((Pi.single k 1, 0) : PhaseSpace 2))
 122      = (N j * S.ha (x.1 j) (x.1 (j + 1)) (x.2 j)) *
 123            (if j = k then (1 : ℝ) else 0)
 124        + (N j * S.hb (x.1 j) (x.1 (j + 1)) (x.2 j)) *
 125            (if j + 1 = k then (1 : ℝ) else 0) := by
 126    intro j
 127    simp only [ContinuousLinearMap.smul_apply, cellD_qdir, smul_eq_mul]
 128    ring
 129  rw [Finset.sum_congr rfl fun j _ => step j, Finset.sum_add_distrib,
 130    sum_mul_ite, sum_mul_ite_add]
 131  have e : k - 1 + 1 = k := by ring
 132  simp only [e]
 133
 134def localHamHamCoefficient (h : LocalHamProfile) (S : LocalHamSmooth h)
 135    (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 136  S.hb (x.1 j) (x.1 (j + 1)) (x.2 j) *
 137    S.hp (x.1 (j + 1)) (x.1 (j + 2)) (x.2 (j + 1))
 138
 139theorem local_profile_ham_ham_form (h : LocalHamProfile) (S : LocalHamSmooth h)
 140    (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 141    bracket (LocalHamFromProfile h N) (LocalHamFromProfile h M) x
 142      = ∑ j : ZMod 2,
 143          (N j * M (j + 1) - M j * N (j + 1)) *
 144            localHamHamCoefficient h S x j := by
 145  unfold bracket localHamHamCoefficient
 146  simp_rw [pderivQ_LocalHamFromProfile h S, pderivP_LocalHamFromProfile h S]
 147  have step1 :
 148      (∑ k : ZMod 2,
 149          ((N k * S.ha (x.1 k) (x.1 (k + 1)) (x.2 k)
 150              + N (k - 1) * S.hb (x.1 (k - 1)) (x.1 k) (x.2 (k - 1))) *
 151            (M k * S.hp (x.1 k) (x.1 (k + 1)) (x.2 k))
 152            - (N k * S.hp (x.1 k) (x.1 (k + 1)) (x.2 k)) *
 153              (M k * S.ha (x.1 k) (x.1 (k + 1)) (x.2 k)
 154                + M (k - 1) * S.hb (x.1 (k - 1)) (x.1 k) (x.2 (k - 1)))))
 155        = ∑ k : ZMod 2,
 156            (N (k - 1) * M k - M (k - 1) * N k) *
 157              (S.hb (x.1 (k - 1)) (x.1 k) (x.2 (k - 1)) *
 158                S.hp (x.1 k) (x.1 (k + 1)) (x.2 k)) :=
 159    Finset.sum_congr rfl fun k _ => by ring
 160  rw [step1]
 161  refine sum_reindex (n := 2) 1
 162    (fun k =>
 163      (N (k - 1) * M k - M (k - 1) * N k) *
 164        (S.hb (x.1 (k - 1)) (x.1 k) (x.2 (k - 1)) *
 165          S.hp (x.1 k) (x.1 (k + 1)) (x.2 k))) _
 166    fun j => ?_
 167  have e1 : j + 1 - 1 = j := by ring
 168  have e2 : j + 1 + 1 = j + 2 := by ring
 169  simp only [e1, e2]
 170
 171def LocalProfileMomDensityIdentity (h : LocalHamProfile) (_S : LocalHamSmooth h)
 172    (momDensity : PhaseSpace 2 → ZMod 2 → ℝ) : Prop :=
 173  ∀ (N M : ZMod 2 → ℝ) (x : PhaseSpace 2),
 174    bracket (LocalHamFromProfile h N) (LocalHamFromProfile h M) x
 175      = ∑ j : ZMod 2,
 176          (N j * M (j + 1) - M j * N (j + 1)) * momDensity x j
 177
 178theorem localHamHamCoefficient_witnesses_identity (h : LocalHamProfile)
 179    (S : LocalHamSmooth h) :
 180    LocalProfileMomDensityIdentity h S (localHamHamCoefficient h S) := by
 181  intro N M x
 182  exact local_profile_ham_ham_form h S N M x
 183
 184/-- General-n packaging Prop (defined; proved form is the n=2 theorem above). -/
 185def LocalProfileHamHamFormGeneral (n : ℕ) [NeZero n]
 186    (h : LocalHamProfile) (hb hp : LocalHamProfile) : Prop :=
 187  ∀ (N M : ZMod n → ℝ) (x : PhaseSpace n),
 188    bracket (fun y => ∑ j : ZMod n, N j * h (y.1 j) (y.1 (j + 1)) (y.2 j))
 189      (fun y => ∑ j : ZMod n, M j * h (y.1 j) (y.1 (j + 1)) (y.2 j)) x
 190      = ∑ j : ZMod n,
 191          (N j * M (j + 1) - M j * N (j + 1)) *
 192            (hb (x.1 j) (x.1 (j + 1)) (x.2 j) *
 193              hp (x.1 (j + 1)) (x.1 (j + 2)) (x.2 (j + 1)))
 194
 195end
 196end HKTLocalFunctionalEquation
 197end SevenGaps
 198end Gravity
 199end IndisputableMonolith
 200