IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochTorusBridge4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   3import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbolZero4D
   5
   6/-!
   7# Discrete torus family glued into midpoint Bloch Tendsto
   8
   9Composes the banked continuous-scale Tendsto
  10`tendsto_exactMidpointBloch_m2_div` along the mesh scale
  11`t(j) = 2π / torusSide j → 𝓝[≠] 0`.
  12
  13The centered bridge is unconditional.  The uncentered form matching
  14`TypedResidual_discrete_torus_family_bridge` uses R2
  15(`ReggeExactFlatHessianBlochSymbolZero4D.exactMidpointBlochSymbolZero_eq_zero`).
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Gravity
  20namespace Analysis
  21namespace ReggeExactFlatHessianBlochTorusBridge4D
  22
  23open Regge4DContinuumPreflight
  24open ReggeExactFlatHessianBlochSymbol4D
  25open ReggeExactFlatHessianBlochSymbolZero4D
  26open BigOperators Filter Topology
  27
  28noncomputable section
  29
  30abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  31abbrev Wave4 := Regge4DContinuumPreflight.Wave4
  32
  33/-! ## §1. Mesh scale and mode identities -/
  34
  35/-- Continuum scale for continuum index `j`: `2π / (j+3)`. -/
  36def torusScale (j : ℕ) : ℝ :=
  37  (2 * Real.pi) / (torusSide j : ℝ)
  38
  39theorem torusScale_eq (j : ℕ) :
  40    torusScale j = (2 * Real.pi) / ((j + 3 : ℕ) : ℝ) := by
  41  unfold torusScale torusSide
  42  rfl
  43
  44theorem realMode_eq_scale (j : ℕ) (m : IntMode4) :
  45    realMode (torusSide j) m = fun i => torusScale j * (m i : ℝ) := by
  46  funext i
  47  unfold realMode torusScale
  48  ring
  49
  50theorem waveNormSq_intMode_eq (m : IntMode4) :
  51    waveNormSq (fun i => (m i : ℝ)) = ∑ i : Fin 4, (m i : ℝ) ^ 2 := by
  52  unfold waveNormSq
  53  refine Finset.sum_congr rfl fun i _ => ?_
  54  ring
  55
  56theorem waveNormSq_intMode_ne_zero (m : IntMode4) (hm : m ≠ 0) :
  57    waveNormSq (fun i => (m i : ℝ)) ≠ 0 := by
  58  rw [waveNormSq_intMode_eq]
  59  intro hzero
  60  have hmi : ∀ i : Fin 4, (m i : ℝ) = 0 := by
  61    intro i
  62    have :=
  63      (Finset.sum_eq_zero_iff_of_nonneg
  64          (fun i (_ : i ∈ Finset.univ) => sq_nonneg (m i : ℝ))).1
  65        hzero i (Finset.mem_univ i)
  66    exact sq_eq_zero_iff.mp this
  67  apply hm
  68  funext i
  69  exact Int.cast_eq_zero.mp (hmi i)
  70
  71theorem momentumNormSq_eq_scale_sq (j : ℕ) (m : IntMode4) :
  72    momentumNormSq (torusSide j) m =
  73      torusScale j ^ 2 * waveNormSq (fun i => (m i : ℝ)) := by
  74  simp [momentumNormSq_eq, waveNormSq_intMode_eq, torusScale]
  75
  76/-! ## §2. Scale Tendsto into the punctured neighborhood of 0 -/
  77
  78theorem tendsto_torusScale_nhds_zero :
  79    Tendsto torusScale atTop (nhds (0 : ℝ)) := by
  80  have h :=
  81    (tendsto_const_div_atTop_nhds_zero_nat (2 * Real.pi)).comp
  82      (tendsto_add_atTop_nat 3)
  83  refine h.congr fun j => ?_
  84  simp [torusScale, torusSide]
  85
  86theorem eventually_torusScale_ne_zero :
  87    ∀ᶠ j : ℕ in atTop, torusScale j ≠ 0 := by
  88  filter_upwards with j
  89  have hden : ((torusSide j : ℕ) : ℝ) ≠ 0 := by
  90    exact Nat.cast_ne_zero.mpr (ne_of_gt (by unfold torusSide; omega))
  91  have hnum : (2 * Real.pi : ℝ) ≠ 0 :=
  92    mul_ne_zero (by norm_num : (2 : ℝ) ≠ 0) Real.pi_ne_zero
  93  exact div_ne_zero hnum hden
  94
  95theorem tendsto_torusScale_nhdsWithin_ne_zero :
  96    Tendsto torusScale atTop (𝓝[≠] (0 : ℝ)) := by
  97  refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ tendsto_torusScale_nhds_zero ?_
  98  filter_upwards [eventually_torusScale_ne_zero] with j hj
  99  simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
 100  exact hj
 101
 102/-! ## §3. Torus-family Tendsto (centered, then uncentered under R2) -/
 103
 104/-- Centered discrete torus family: banked continuous Tendsto along `t(j)`. -/
 105theorem tendsto_exactMidpointBloch_torus_family_centered
 106    (m : IntMode4) (E : Mat4) (hm : m ≠ 0) :
 107    Tendsto
 108      (fun j : ℕ =>
 109        (exactMidpointBlochSymbol E (realMode (torusSide j) m) -
 110            exactMidpointBlochSymbolZero E) /
 111          momentumNormSq (torusSide j) m)
 112      atTop
 113      (nhds
 114        (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
 115          waveNormSq (fun i => (m i : ℝ)))) := by
 116  let dir : Wave4 := fun i => (m i : ℝ)
 117  let n : ℝ := waveNormSq dir
 118  have hn : n ≠ 0 := waveNormSq_intMode_ne_zero m hm
 119  have hcont := tendsto_exactMidpointBloch_m2_div E dir n hn
 120  have hcomp := hcont.comp tendsto_torusScale_nhdsWithin_ne_zero
 121  refine hcomp.congr' ?_
 122  filter_upwards with j
 123  dsimp only [Function.comp_apply]
 124  rw [realMode_eq_scale, momentumNormSq_eq_scale_sq]
 125
 126/-- Uncentered form matching `TypedResidual_discrete_torus_family_bridge`.
 127Requires the R2 hypothesis `exactMidpointBlochSymbolZero E = 0`. -/
 128theorem tendsto_exactMidpointBloch_torus_family
 129    (m : IntMode4) (E : Mat4) (hm : m ≠ 0)
 130    (h0 : exactMidpointBlochSymbolZero E = 0) :
 131    Tendsto
 132      (fun j : ℕ =>
 133        exactMidpointBlochSymbol E (realMode (torusSide j) m) /
 134          momentumNormSq (torusSide j) m)
 135      atTop
 136      (nhds
 137        (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
 138          waveNormSq (fun i => (m i : ℝ)))) := by
 139  have h := tendsto_exactMidpointBloch_torus_family_centered m E hm
 140  refine h.congr' ?_
 141  filter_upwards with j
 142  rw [h0, sub_zero]
 143
 144/-- Package: R2 for all polarizations inhabits the discrete torus bridge Prop
 145shape (same binders as `TypedResidual_discrete_torus_family_bridge`). -/
 146theorem discrete_torus_family_bridge_of_symbolZero
 147    (hZ : ∀ H : Mat4, exactMidpointBlochSymbolZero H = 0) :
 148    ∀ (m : IntMode4) (E : Mat4),
 149      m ≠ 0 →
 150        Tendsto
 151          (fun j : ℕ =>
 152            exactMidpointBlochSymbol E (realMode (torusSide j) m) /
 153              momentumNormSq (torusSide j) m)
 154          atTop
 155          (nhds
 156            (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
 157              waveNormSq (fun i => (m i : ℝ)))) :=
 158  fun m E hm => tendsto_exactMidpointBloch_torus_family m E hm (hZ E)
 159
 160/-- **THEOREM (R4):** discrete torus family bridge, uncentered, for all
 161nonzero modes and all polarizations.  Composes banked continuous Tendsto
 162with R2 (`typedResidual_midpointBloch_symbolZero`). -/
 163theorem discrete_torus_family_bridge :
 164    ∀ (m : IntMode4) (E : Mat4),
 165      m ≠ 0 →
 166        Tendsto
 167          (fun j : ℕ =>
 168            exactMidpointBlochSymbol E (realMode (torusSide j) m) /
 169              momentumNormSq (torusSide j) m)
 170          atTop
 171          (nhds
 172            (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
 173              waveNormSq (fun i => (m i : ℝ)))) :=
 174  discrete_torus_family_bridge_of_symbolZero
 175    ReggeExactFlatHessianBlochSymbolZero4D.typedResidual_midpointBloch_symbolZero
 176
 177/-- Mesh ContinuumSymbolIs binder is definitionally the torus-family
 178midpoint sequence; bridge therefore inhabits ContinuumSymbolIs at the
 179m² Rayleigh value (still geometric / j-dependent; not a constant face). -/
 180theorem continuumSymbolIs_midpoint_rayleigh
 181    (m : IntMode4) (E : Mat4) (hm : m ≠ 0) :
 182    Regge4DContinuumSymbolIs m E
 183      (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
 184        waveNormSq (fun i => (m i : ℝ))) :=
 185  discrete_torus_family_bridge m E hm
 186
 187end
 188
 189end ReggeExactFlatHessianBlochTorusBridge4D
 190end Analysis
 191end Gravity
 192end IndisputableMonolith
 193