IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBinding

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum
   3import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketN
   4
   5/-!
   6# Wave C2 R4 repair Steps 3–4: sampled HamDynN binding + periodic terminal
   7
   8Binds the freestanding Riemann shape `sampledDynamicBracketSum` to the
   9genuine lattice bracket `bracket (HamDynN ·) (HamDynN ·)` after the
  10periodic wrap treatment, then lands the ledger terminal
  11`dirac_algebra_continuum_limit` for 1-periodic C¹ data.
  12
  13## Wrap treatment
  14
  15On `ZMod n`, site `n-1` has successor `0`. The non-periodic mesh samples
  16`(k+1)/n = 1` at the last cell; the periodic mesh samples `0`. For
  171-periodic fields these agree, so
  18`periodicSampledDynamicBracketSum = sampledDynamicBracketSum`.
  19
  20True structure-factor placement from `bracket_HamDynN_HamDynN` is `g` at
  21the left split point `j`, matching `dynamicStructureProfile q (k/n)`.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Gravity
  26namespace SevenGaps
  27namespace DiracAlgebraContinuumBinding
  28
  29open HypersurfaceDeformation
  30open DynamicStructureBracketN
  31open DiracAlgebraContinuum
  32open DynamicStructureContinuumSmearing
  33open Filter Topology Set Finset
  34
  35noncomputable section
  36
  37/-! ## Step 3: sampled phase / lapse -/
  38
  39/-- Sample continuum fields onto the `ZMod n` lattice at nodes `j.val / n`. -/
  40def sampledPhasePoint (n : ℕ) [NeZero n] (q p : ℝ → ℝ) : PhaseSpace n :=
  41  (fun j : ZMod n => q ((j.val : ℝ) / n), fun j : ZMod n => p ((j.val : ℝ) / n))
  42
  43/-- Sample a continuum lapse onto lattice sites. -/
  44def sampledLapse (n : ℕ) [NeZero n] (N : ℝ → ℝ) : ZMod n → ℝ :=
  45  fun j => N ((j.val : ℝ) / n)
  46
  47/-- Wrap-successor index on `{0,…,n-1}`: `n-1 ↦ 0`, else `k ↦ k+1`. -/
  48def wrapSucc (n k : ℕ) : ℕ :=
  49  if k + 1 = n then 0 else k + 1
  50
  51/-- Periodic sampled RHS: last cell uses wrap samples at `0`, not at `1`. -/
  52def periodicSampledDynamicBracketSum (n : ℕ) (N M q p : ℝ → ℝ) : ℝ :=
  53  ∑ k ∈ range n,
  54    (N ((k : ℝ) / n) * M ((wrapSucc n k : ℕ) / n) -
  55        M ((k : ℝ) / n) * N ((wrapSucc n k : ℕ) / n)) *
  56      (dynamicStructureProfile q ((k : ℝ) / n) *
  57        (p ((wrapSucc n k : ℕ) / n) *
  58          (q ((wrapSucc n k : ℕ) / n) - q ((k : ℝ) / n))))
  59
  60/-- Lattice bracket evaluated on continuum samples (junk `0` at `n = 0`). -/
  61def continuumLatticeBracket (n : ℕ) (N M q p : ℝ → ℝ) : ℝ :=
  62  if hn : n = 0 then 0
  63  else
  64    haveI : NeZero n := ⟨hn⟩
  65    bracket (HamDynN (sampledLapse n N)) (HamDynN (sampledLapse n M))
  66      (sampledPhasePoint n q p)
  67
  68/-! ## ZMod sampling lemmas -/
  69
  70private lemma zmod_val_of_lt {n k : ℕ} [NeZero n] (hk : k < n) :
  71    ((k : ZMod n).val : ℕ) = k :=
  72  ZMod.val_natCast_of_lt hk
  73
  74private lemma wrapSucc_lt (n k : ℕ) [NeZero n] (hk : k < n) : wrapSucc n k < n := by
  75  unfold wrapSucc
  76  split_ifs with h
  77  · exact NeZero.pos n
  78  · exact Nat.lt_of_le_of_ne (Nat.succ_le_of_lt hk) h
  79
  80private lemma zmod_succ_val {n k : ℕ} [NeZero n] (hk : k < n) :
  81    (((k : ZMod n) + 1).val : ℕ) = wrapSucc n k := by
  82  unfold wrapSucc
  83  by_cases h : k + 1 = n
  84  · simp only [h, ↓reduceIte]
  85    have h0 : (k : ZMod n) + 1 = 0 := by
  86      rw [← Nat.cast_one, ← Nat.cast_add, h, ZMod.natCast_self]
  87    simp [h0]
  88  · simp only [h, ↓reduceIte]
  89    have hlt : k + 1 < n := Nat.lt_of_le_of_ne (Nat.succ_le_of_lt hk) h
  90    have : ((k : ZMod n) + 1) = ((k + 1 : ℕ) : ZMod n) := by
  91      simp [Nat.cast_succ]
  92    rw [this, zmod_val_of_lt hlt]
  93
  94private lemma sum_zmod_eq_sum_range {n : ℕ} [NeZero n] (f : ZMod n → ℝ) :
  95    (∑ j : ZMod n, f j) = ∑ k ∈ range n, f (k : ZMod n) := by
  96  refine sum_nbij (fun j : ZMod n => j.val)
  97    (fun j _ => mem_range.2 j.val_lt)
  98    (fun _ _ _ _ h => ZMod.val_injective n h)
  99    (fun k hk => ⟨(k : ZMod n), mem_univ _, zmod_val_of_lt (mem_range.1 hk)⟩)
 100    (fun j _ => by rw [ZMod.natCast_zmod_val])
 101
 102/-! ## Step 3 binding -/
 103
 104/-- THEOREM. At continuum samples, the general-`n` dynamic bracket equals the
 105periodic sampled sum (definitional unfolding of `bracket_HamDynN_HamDynN`). -/
 106theorem bracket_HamDynN_eq_periodicSampled
 107    (n : ℕ) [NeZero n] (N M q p : ℝ → ℝ) :
 108    bracket (HamDynN (sampledLapse n N)) (HamDynN (sampledLapse n M))
 109        (sampledPhasePoint n q p)
 110      = periodicSampledDynamicBracketSum n N M q p := by
 111  rw [bracket_HamDynN_HamDynN]
 112  simp only [sampledLapse, sampledPhasePoint, periodicSampledDynamicBracketSum,
 113    dynamicStructureProfile]
 114  rw [sum_zmod_eq_sum_range]
 115  refine sum_congr rfl fun k hk => ?_
 116  have hk' : k < n := mem_range.1 hk
 117  have hv : ((k : ZMod n).val : ℕ) = k := zmod_val_of_lt hk'
 118  have hs : (((k : ZMod n) + 1).val : ℕ) = wrapSucc n k := zmod_succ_val hk'
 119  simp only [hv, hs, pow_two]
 120
 121theorem continuumLatticeBracket_eq_periodic
 122    (n : ℕ) (N M q p : ℝ → ℝ) :
 123    continuumLatticeBracket n N M q p
 124      = periodicSampledDynamicBracketSum n N M q p := by
 125  unfold continuumLatticeBracket
 126  split_ifs with hn
 127  · subst hn
 128    simp [periodicSampledDynamicBracketSum]
 129  · haveI : NeZero n := ⟨hn⟩
 130    exact bracket_HamDynN_eq_periodicSampled (n := n) N M q p
 131
 132/-! ## Step 4: periodicity equates wrap and non-wrap meshes -/
 133
 134/-- 1-periodic real function on the circle of length 1. -/
 135def Periodic1 (f : ℝ → ℝ) : Prop :=
 136  ∀ t : ℝ, f (t + 1) = f t
 137
 138theorem Periodic1.eval_one (f : ℝ → ℝ) (hf : Periodic1 f) : f 1 = f 0 := by
 139  simpa using hf 0
 140
 141private lemma wrapSucc_eq_succ_or_zero (n k : ℕ) :
 142    wrapSucc n k = k + 1 ∨ (k + 1 = n ∧ wrapSucc n k = 0) := by
 143  unfold wrapSucc
 144  by_cases h : k + 1 = n
 145  · exact Or.inr ⟨h, by simp [h]⟩
 146  · exact Or.inl (by simp [h])
 147
 148/-- THEOREM. For 1-periodic data, the wrap mesh equals the non-periodic mesh
 149(last cell: samples at `1` equal samples at `0`). -/
 150theorem periodicSampled_eq_sampled_of_periodic
 151    (n : ℕ) (N M q p : ℝ → ℝ)
 152    (hN : Periodic1 N) (hM : Periodic1 M) (hq : Periodic1 q) (hp : Periodic1 p) :
 153    periodicSampledDynamicBracketSum n N M q p
 154      = sampledDynamicBracketSum n N M q p := by
 155  unfold periodicSampledDynamicBracketSum sampledDynamicBracketSum
 156  refine sum_congr rfl fun k hk => ?_
 157  have hk' : k < n := mem_range.1 hk
 158  rcases wrapSucc_eq_succ_or_zero n k with h | ⟨hEq, hW⟩
 159  · simp [h]
 160  · have hnR : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.ne_zero_of_lt hk')
 161    have hdiv : (n : ℝ) / n = 1 := by field_simp
 162    have hN1 : N ((n : ℝ) / n) = N 0 := by rw [hdiv]; exact Periodic1.eval_one N hN
 163    have hM1 : M ((n : ℝ) / n) = M 0 := by rw [hdiv]; exact Periodic1.eval_one M hM
 164    have hq1 : q ((n : ℝ) / n) = q 0 := by rw [hdiv]; exact Periodic1.eval_one q hq
 165    have hp1 : p ((n : ℝ) / n) = p 0 := by rw [hdiv]; exact Periodic1.eval_one p hp
 166    simp [hW, hEq, hN1, hM1, hq1, hp1, zero_div]
 167
 168/-- Scaled lattice bracket equals scaled freestanding shape under periodicity. -/
 169theorem scaled_continuumLatticeBracket_eq_scaled_sampled
 170    (n : ℕ) (N M q p : ℝ → ℝ)
 171    (hN : Periodic1 N) (hM : Periodic1 M) (hq : Periodic1 q) (hp : Periodic1 p) :
 172    (n : ℝ) * continuumLatticeBracket n N M q p
 173      = (n : ℝ) * sampledDynamicBracketSum n N M q p := by
 174  rw [continuumLatticeBracket_eq_periodic,
 175    periodicSampled_eq_sampled_of_periodic n N M q p hN hM hq hp]
 176
 177/-! ## Ledger terminal -/
 178
 179/-- THEOREM (ledger terminal, repaired). For 1-periodic ContDiff-1 lapses /
 180configuration and 1-periodic continuous momentum, the scaled general-`n`
 181dynamic Hamiltonian bracket at continuum samples tends to the continuum Dirac
 182density. Proved by Step-3 binding + periodicity +
 183`dynamic_bracket_shape_continuum_limit`. -/
 184theorem dirac_algebra_continuum_limit (N M q p : ℝ → ℝ)
 185    (hNper : Periodic1 N) (hMper : Periodic1 M) (hqper : Periodic1 q)
 186    (hpper : Periodic1 p)
 187    (hN : ContDiff ℝ 1 N) (hM : ContDiff ℝ 1 M) (hq : ContDiff ℝ 1 q)
 188    (hp : ContinuousOn p (Icc 0 1)) :
 189    Tendsto (fun n : ℕ => (n : ℝ) * continuumLatticeBracket n N M q p)
 190      atTop
 191      (nhds (∫ t in (0 : ℝ)..1, continuumDiracDensity N M q p t)) := by
 192  have hshape :=
 193    dynamic_bracket_shape_continuum_limit N M q p hN hM hq hp
 194  refine hshape.congr fun n => ?_
 195  exact (scaled_continuumLatticeBracket_eq_scaled_sampled
 196    n N M q p hNper hMper hqper hpper).symm
 197
 198/-- Unpack: lattice form with explicit `HamDynN` for `n > 0`. -/
 199theorem dirac_algebra_continuum_limit_hamDynN (N M q p : ℝ → ℝ)
 200    (hNper : Periodic1 N) (hMper : Periodic1 M) (hqper : Periodic1 q)
 201    (hpper : Periodic1 p)
 202    (hN : ContDiff ℝ 1 N) (hM : ContDiff ℝ 1 M) (hq : ContDiff ℝ 1 q)
 203    (hp : ContinuousOn p (Icc 0 1)) :
 204    Tendsto
 205      (fun n : ℕ =>
 206        if hn : n = 0 then (0 : ℝ)
 207        else
 208          haveI : NeZero n := ⟨hn⟩
 209          (n : ℝ) *
 210            bracket (HamDynN (sampledLapse n N)) (HamDynN (sampledLapse n M))
 211              (sampledPhasePoint n q p))
 212      atTop
 213      (nhds (∫ t in (0 : ℝ)..1, continuumDiracDensity N M q p t)) := by
 214  have h := dirac_algebra_continuum_limit N M q p hNper hMper hqper hpper hN hM hq hp
 215  refine h.congr fun n => ?_
 216  unfold continuumLatticeBracket
 217  split_ifs with hn
 218  · simp [hn]
 219  · rfl
 220
 221/-! ### Axiom receipts -/
 222
 223#print axioms bracket_HamDynN_eq_periodicSampled
 224#print axioms periodicSampled_eq_sampled_of_periodic
 225#print axioms dirac_algebra_continuum_limit
 226#print axioms dirac_algebra_continuum_limit_hamDynN
 227
 228end
 229end DiracAlgebraContinuumBinding
 230end SevenGaps
 231end Gravity
 232end IndisputableMonolith
 233