IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketN

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket
   3import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker
   4
   5/-!
   6# Wave C2 R4 repair Step 2: general-`n` dynamic structure bracket
   7
   8Generalizes `DynamicStructureBracket.HamDyn` / `bracket_HamDyn_HamDyn` from
   9`n = 2` to arbitrary `n` with `[NeZero n]`. The Frechet bookkeeping
  10(`HamDynD`, `∂g/∂q` correction, Kronecker collapse, periodic reindex) is
  11the same pattern as the two-site proof; ZMod wraparound is periodic, so
  12there is no boundary term.
  13
  14True general RHS (derived from the calculus, matching the `n = 2` case):
  15
  16```
  17bracket (HamDynN N) (HamDynN M) x
  18  = ∑ j, (N j * M (j+1) - M j * N (j+1))
  19      * ((1 + (x.1 j)^2) * (x.2 (j+1) * (x.1 (j+1) - x.1 j)))
  20```
  21
  22Structure factor `g_j = 1 + (x.1 j)^2` sits at the left split point `j`
  23(same placement as `HamW`'s background weight `w j`).
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Gravity
  28namespace SevenGaps
  29namespace DynamicStructureBracketN
  30
  31open HypersurfaceDeformation WeightedHypersurfaceBracket
  32open DynamicStructureFunctionBlocker DynamicStructureBracket
  33
  34noncomputable section
  35
  36open Finset
  37
  38variable {n : ℕ} [NeZero n]
  39
  40/-! ## General-`n` dynamic Hamiltonian -/
  41
  42/-- MODEL. Exact shape of `HamDyn` at general `n`: kinetic slot unweighted,
  43stiffness slot carries `g x j = 1 + (x.1 j)^2`. -/
  44def HamDynN (N : ZMod n → ℝ) (x : PhaseSpace n) : ℝ :=
  45  ∑ i : ZMod n, (N i / 2) *
  46    (x.2 i * x.2 i +
  47      (1 + x.1 i * x.1 i) *
  48        ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))
  49
  50/-- Consistency: at `n = 2`, `HamDynN` is definitionally `HamDyn`. -/
  51theorem HamDynN_eq_HamDyn (N : ZMod 2 → ℝ) :
  52    HamDynN (n := 2) N = HamDyn N :=
  53  rfl
  54
  55/-- Inverse-metric factor used in the structure slot. -/
  56def dynamicInverseMetricN (x : PhaseSpace n) (j : ZMod n) : ℝ :=
  57  1 + (x.1 j) ^ 2
  58
  59omit [NeZero n] in
  60theorem dynamicInverseMetricN_eq (x : PhaseSpace n) (j : ZMod n) :
  61    dynamicInverseMetricN x j = 1 + x.1 j * x.1 j := by
  62  simp [dynamicInverseMetricN, pow_two]
  63
  64/-! ## Frechet derivative (honest; includes ∂g/∂q) -/
  65
  66/-- Frechet derivative of `HamDynN N`. Final summand carries `0 + …` to match
  67`HasFDerivAt.const.add` from the metric factor (same as `HamDynD`). -/
  68def HamDynND (N : ZMod n → ℝ) (x : PhaseSpace n) : PhaseSpace n →L[ℝ] ℝ :=
  69  ∑ i : ZMod n,
  70    (N i / 2) •
  71      ((x.2 i • coordP i + x.2 i • coordP i) +
  72        ((1 + x.1 i * x.1 i) •
  73            ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i) +
  74              (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)) +
  75          ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)) •
  76            (0 + (x.1 i • coordQ i + x.1 i • coordQ i))))
  77
  78lemma hasFDerivAt_HamDynN (N : ZMod n → ℝ) (x : PhaseSpace n) :
  79    HasFDerivAt (HamDynN N) (HamDynND N x) x := by
  80  unfold HamDynN HamDynND
  81  exact HasFDerivAt.fun_sum fun i _ =>
  82    ((((hasFDerivAt_coord_snd i x).mul (hasFDerivAt_coord_snd i x)).add
  83      (((hasFDerivAt_const (1 : ℝ) x).add
  84          ((hasFDerivAt_coord_fst i x).mul (hasFDerivAt_coord_fst i x))).mul
  85        (((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x)).mul
  86          ((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x))))).const_mul
  87      (N i / 2))
  88
  89/-- THEOREM. Momentum partial: kinetic slot unchanged by `g`. -/
  90theorem pderivP_HamDynN (N : ZMod n → ℝ) (j : ZMod n) (x : PhaseSpace n) :
  91    pderivP (HamDynN N) j x = N j * x.2 j := by
  92  rw [pderivP, (hasFDerivAt_HamDynN N x).fderiv, HamDynND, ContinuousLinearMap.sum_apply]
  93  have step : ∀ i : ZMod n,
  94      (((N i / 2) •
  95          ((x.2 i • coordP i + x.2 i • coordP i) +
  96            ((1 + x.1 i * x.1 i) •
  97                ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i) +
  98                  (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)) +
  99              ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)) •
 100                (0 + (x.1 i • coordQ i + x.1 i • coordQ i)))) :
 101            PhaseSpace n →L[ℝ] ℝ))
 102        ((0, Pi.single j 1) : PhaseSpace n)
 103      = (N i * x.2 i) * (if i = j then (1 : ℝ) else 0) := by
 104    intro i
 105    simp [Pi.single_apply]
 106    split_ifs <;> ring
 107  rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]
 108
 109/-- THEOREM. Honest configuration partial: frozen `HamW`-style contribution
 110plus the `∂g/∂q` correction `N_j q_j (Δq_j)²`. -/
 111theorem pderivQ_HamDynN (N : ZMod n → ℝ) (j : ZMod n) (x : PhaseSpace n) :
 112    pderivQ (HamDynN N) j x
 113      = N (j - 1) * ((1 + x.1 (j - 1) * x.1 (j - 1)) * (x.1 j - x.1 (j - 1)))
 114        - N j * ((1 + x.1 j * x.1 j) * (x.1 (j + 1) - x.1 j))
 115        + N j * (x.1 j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) := by
 116  rw [pderivQ, (hasFDerivAt_HamDynN N x).fderiv, HamDynND, ContinuousLinearMap.sum_apply]
 117  have step : ∀ i : ZMod n,
 118      (((N i / 2) •
 119          ((x.2 i • coordP i + x.2 i • coordP i) +
 120            ((1 + x.1 i * x.1 i) •
 121                ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i) +
 122                  (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)) +
 123              ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)) •
 124                (0 + (x.1 i • coordQ i + x.1 i • coordQ i)))) :
 125            PhaseSpace n →L[ℝ] ℝ))
 126        ((Pi.single j 1, 0) : PhaseSpace n)
 127      = (N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) *
 128            (if i + 1 = j then (1 : ℝ) else 0)
 129        - (N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) *
 130            (if i = j then (1 : ℝ) else 0)
 131        + (N i * (x.1 i * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))) *
 132            (if i = j then (1 : ℝ) else 0) := by
 133    intro i
 134    simp [Pi.single_apply, mul_sub]
 135    split_ifs <;> ring
 136  rw [Finset.sum_congr rfl fun i _ => step i]
 137  simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]
 138  rw [sum_mul_ite_add
 139      (fun i => N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) 1 j,
 140    sum_mul_ite
 141      (fun i => N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) j,
 142    sum_mul_ite
 143      (fun i => N i * (x.1 i * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))) j]
 144  have e : j - 1 + 1 = j := by ring
 145  simp only [e]
 146
 147theorem differentiable_HamDynN (N : ZMod n → ℝ) :
 148    Differentiable ℝ (HamDynN N) :=
 149  fun x => (hasFDerivAt_HamDynN N x).differentiableAt
 150
 151/-- THEOREM (headline). Exact dynamic structure-function identity at general
 152`n`. Structure factor at left split point `j`. The `∂g/∂q` corrections cancel
 153in the Hamiltonian–Hamiltonian bracket (same telescoping as `n = 2`). -/
 154theorem bracket_HamDynN_HamDynN (N M : ZMod n → ℝ) (x : PhaseSpace n) :
 155    bracket (HamDynN N) (HamDynN M) x
 156      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1)) *
 157          ((1 + x.1 j * x.1 j) *
 158            (x.2 (j + 1) * (x.1 (j + 1) - x.1 j))) := by
 159  simp only [bracket, pderivQ_HamDynN, pderivP_HamDynN]
 160  have step1 :
 161      (∑ j : ZMod n,
 162          ((N (j - 1) * ((1 + x.1 (j - 1) * x.1 (j - 1)) * (x.1 j - x.1 (j - 1)))
 163              - N j * ((1 + x.1 j * x.1 j) * (x.1 (j + 1) - x.1 j))
 164              + N j * (x.1 j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)))) *
 165            (M j * x.2 j)
 166            - (N j * x.2 j) *
 167              (M (j - 1) * ((1 + x.1 (j - 1) * x.1 (j - 1)) * (x.1 j - x.1 (j - 1)))
 168                - M j * ((1 + x.1 j * x.1 j) * (x.1 (j + 1) - x.1 j))
 169                + M j * (x.1 j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))))))
 170        = ∑ j : ZMod n,
 171            (N (j - 1) * M j - M (j - 1) * N j) *
 172              ((1 + x.1 (j - 1) * x.1 (j - 1)) *
 173                (x.2 j * (x.1 j - x.1 (j - 1)))) :=
 174    Finset.sum_congr rfl fun j _ => by ring
 175  rw [step1]
 176  refine sum_reindex 1
 177    (fun k =>
 178      (N (k - 1) * M k - M (k - 1) * N k) *
 179        ((1 + x.1 (k - 1) * x.1 (k - 1)) *
 180          (x.2 k * (x.1 k - x.1 (k - 1))))) _
 181    fun j => ?_
 182  have e1 : j + 1 - 1 = j := by ring
 183  simp only [e1]
 184
 185/-- Equivalent form with `dynamicInverseMetricN`. -/
 186theorem bracket_HamDynN_HamDynN' (N M : ZMod n → ℝ) (x : PhaseSpace n) :
 187    bracket (HamDynN N) (HamDynN M) x
 188      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1)) *
 189          (dynamicInverseMetricN x j *
 190            (x.2 (j + 1) * (x.1 (j + 1) - x.1 j))) := by
 191  simpa [dynamicInverseMetricN, pow_two] using bracket_HamDynN_HamDynN N M x
 192
 193/-- Consistency: at `n = 2`, recovers `bracket_HamDyn_HamDyn`. -/
 194theorem bracket_HamDynN_HamDynN_eq_two
 195    (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 196    bracket (HamDynN (n := 2) N) (HamDynN (n := 2) M) x
 197      = bracket (HamDyn N) (HamDyn M) x := by
 198  rw [HamDynN_eq_HamDyn, HamDynN_eq_HamDyn]
 199
 200theorem bracket_HamDynN_recovers_bracket_HamDyn
 201    (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 202    bracket (HamDynN (n := 2) N) (HamDynN (n := 2) M) x
 203      = ∑ j : ZMod 2, (N j * M (j + 1) - M j * N (j + 1)) *
 204          (concreteDynamicInverseMetric x j *
 205            (x.2 (j + 1) * (x.1 (j + 1) - x.1 j))) := by
 206  rw [bracket_HamDynN_HamDynN_eq_two, bracket_HamDyn_HamDyn]
 207
 208/-! ### Axiom receipts -/
 209
 210#print axioms hasFDerivAt_HamDynN
 211#print axioms pderivP_HamDynN
 212#print axioms pderivQ_HamDynN
 213#print axioms differentiable_HamDynN
 214#print axioms bracket_HamDynN_HamDynN
 215#print axioms bracket_HamDynN_recovers_bracket_HamDyn
 216
 217end
 218end DynamicStructureBracketN
 219end SevenGaps
 220end Gravity
 221end IndisputableMonolith
 222