IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochData4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochTendsto4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D
   5
   6/-!
   7# Exact midpoint Bloch trig-polynomial symbol (named)
   8
   9Names the Stage-1 unit-cell exact flat Hessian as a finite trig polynomial
  10over `ReggeExactFlatHessianBlochData4D.couplingTable` (1208 couplings).
  11
  12Centered Tendsto to the cosine two-jet is proved by specializing
  13`ReggeExactFlatHessianBlochTendsto4D.tendsto_centeredTrigPoly_div_sq`
  14through irreducible weight/phase/univ wrappers (avoids Fin-1208 array
  15whnf blowup during elaboration).
  16
  17Algebraic normalization identity: discrete bookkeeping ×2 recovers
  18frozen `-1/4` (`ReggeExactFlatHessianNormGate4D`).  Ledger
  19`S_RS_converges_EH_4d` / `gap_action_recovery` remain open/false;
  20mesh ContinuumSymbolIs geometric Tendsto is the ledger gate.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Gravity
  25namespace Analysis
  26namespace ReggeExactFlatHessianBlochSymbol4D
  27
  28open ReggeExactFlatHessianBlochData4D
  29open ReggeExactFlatHessianBlochTendsto4D
  30open ReggeExactFlatHessianNormGate4D
  31open BigOperators Filter Topology
  32
  33noncomputable section
  34
  35abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  36abbrev Wave4 := Fin 4 → ℝ
  37abbrev CouplingIdx := Fin couplingTable.size
  38
  39/-! ## §1. Trig-polynomial symbol (MODEL) -/
  40
  41def edgeStrain (H : Mat4) (D : Fin 4 → ℤ) : ℝ :=
  42  ∑ i : Fin 4, ∑ j : Fin 4, H i j * (D i : ℝ) * (D j : ℝ)
  43
  44def couplingPhase (c : Coupling) (k : Wave4) : ℝ :=
  45  ∑ i : Fin 4, k i * c.delta i
  46
  47def couplingWeight (H : Mat4) (c : Coupling) : ℝ :=
  48  (1 / 2 : ℝ) * (c.s : ℝ) * edgeStrain H c.De * edgeStrain H c.Dep
  49
  50def couplingWeightIdx (H : Mat4) (i : CouplingIdx) : ℝ :=
  51  couplingWeight H couplingTable[i]
  52
  53def couplingPhaseIdx (k : Wave4) (i : CouplingIdx) : ℝ :=
  54  couplingPhase couplingTable[i] k
  55
  56/-- Exact midpoint Bloch symbol: finite trig polynomial over the unit-cell
  57coupling table. -/
  58def exactMidpointBlochSymbol (H : Mat4) (k : Wave4) : ℝ :=
  59  ∑ i : CouplingIdx,
  60    couplingWeightIdx H i * Real.cos (couplingPhaseIdx k i)
  61
  62/-- Cosine two-jet m² coefficient of the centered symbol. -/
  63def exactMidpointBlochM2 (H : Mat4) (k : Wave4) : ℝ :=
  64  ∑ i : CouplingIdx,
  65    couplingWeightIdx H i * (-(couplingPhaseIdx k i) ^ 2 / 2)
  66
  67/-- Zero-momentum value of the trig polynomial. -/
  68def exactMidpointBlochSymbolZero (H : Mat4) : ℝ :=
  69  ∑ i : CouplingIdx, couplingWeightIdx H i
  70
  71/-! ## §2. Irreducible specialization surface (Fin-1208 hygiene) -/
  72
  73/-- Opaque univ: keeps `Finset.univ : Finset (Fin 1208)` from exploding
  74during Tendsto specialization. -/
  75irreducible_def couplingUniv : Finset CouplingIdx := Finset.univ
  76
  77irreducible_def weightFn (H : Mat4) : CouplingIdx → ℝ := couplingWeightIdx H
  78
  79irreducible_def phaseFn (dir : Wave4) : CouplingIdx → ℝ := couplingPhaseIdx dir
  80
  81theorem couplingPhase_smul (t : ℝ) (dir : Wave4) (c : Coupling) :
  82    couplingPhase c (fun j => t * dir j) = t * couplingPhase c dir := by
  83  unfold couplingPhase
  84  simp_rw [mul_assoc]
  85  exact Eq.symm (Finset.mul_sum _ (fun i => dir i * c.delta i) t)
  86
  87theorem couplingPhaseIdx_smul (t : ℝ) (dir : Wave4) (i : CouplingIdx) :
  88    couplingPhaseIdx (fun j => t * dir j) i =
  89      t * couplingPhaseIdx dir i := by
  90  unfold couplingPhaseIdx
  91  exact couplingPhase_smul t dir _
  92
  93theorem couplingPhase_zero (c : Coupling) :
  94    couplingPhase c (fun _ => (0 : ℝ)) = 0 := by
  95  unfold couplingPhase
  96  simp only [zero_mul, Finset.sum_const_zero]
  97
  98theorem couplingPhaseIdx_zero (i : CouplingIdx) :
  99    couplingPhaseIdx (fun _ => (0 : ℝ)) i = 0 := by
 100  unfold couplingPhaseIdx
 101  exact couplingPhase_zero _
 102
 103theorem exactMidpointBlochSymbol_zero_eq (H : Mat4) :
 104    exactMidpointBlochSymbol H (fun _ => 0) = exactMidpointBlochSymbolZero H := by
 105  unfold exactMidpointBlochSymbol exactMidpointBlochSymbolZero
 106  refine Finset.sum_congr rfl fun i _ => ?_
 107  rw [couplingPhaseIdx_zero, Real.cos_zero, mul_one]
 108
 109private theorem sum_w_cos_sub_sum_w (H : Mat4) (dir : Wave4) (t : ℝ) :
 110    (∑ i : CouplingIdx,
 111        couplingWeightIdx H i *
 112          Real.cos (couplingPhaseIdx (fun j => t * dir j) i)) -
 113        ∑ i : CouplingIdx, couplingWeightIdx H i =
 114      ∑ i : CouplingIdx,
 115        couplingWeightIdx H i *
 116          (Real.cos (couplingPhaseIdx (fun j => t * dir j) i) - 1) := by
 117  simp_rw [mul_sub, mul_one, Finset.sum_sub_distrib]
 118
 119private theorem centered_eq_irred (H : Mat4) (dir : Wave4) (t : ℝ) :
 120    exactMidpointBlochSymbol H (fun j => t * dir j) -
 121        exactMidpointBlochSymbolZero H =
 122      centeredTrigPoly (weightFn H) (phaseFn dir) couplingUniv t := by
 123  rw [weightFn_def, phaseFn_def, couplingUniv_def]
 124  unfold exactMidpointBlochSymbol exactMidpointBlochSymbolZero centeredTrigPoly
 125  rw [sum_w_cos_sub_sum_w]
 126  refine Finset.sum_congr rfl fun i _ => ?_
 127  rw [couplingPhaseIdx_smul]
 128
 129private theorem m2_eq_irred (H : Mat4) (dir : Wave4) :
 130    exactMidpointBlochM2 H dir =
 131      centeredTrigPolyM2 (weightFn H) (phaseFn dir) couplingUniv := by
 132  rw [weightFn_def, phaseFn_def, couplingUniv_def]
 133  rfl
 134
 135/-- **THEOREM:** centered exact midpoint Bloch `/ t²` tends to its cosine
 136two-jet.  Specialized through irreducible wrappers (no Fin-1208 whnf). -/
 137theorem tendsto_exactMidpointBloch_centered_div_sq
 138    (H : Mat4) (dir : Wave4) :
 139    Tendsto
 140      (fun t : ℝ =>
 141        (exactMidpointBlochSymbol H (fun j => t * dir j) -
 142            exactMidpointBlochSymbolZero H) / t ^ 2)
 143      (𝓝[≠] (0 : ℝ)) (nhds (exactMidpointBlochM2 H dir)) := by
 144  have habs :=
 145    tendsto_centeredTrigPoly_div_sq (weightFn H) (phaseFn dir) couplingUniv
 146  have htarget :
 147      centeredTrigPolyM2 (weightFn H) (phaseFn dir) couplingUniv =
 148        exactMidpointBlochM2 H dir := (m2_eq_irred H dir).symm
 149  rw [← htarget]
 150  refine (tendsto_congr' ?_).mpr habs
 151  filter_upwards with t
 152  rw [centered_eq_irred]
 153
 154/-- Division form: centered `/ (t² n)` tends to `m2 / n` when `n ≠ 0`. -/
 155theorem tendsto_exactMidpointBloch_m2_div
 156    (H : Mat4) (dir : Wave4) (n : ℝ) (hn : n ≠ 0) :
 157    Tendsto
 158      (fun t : ℝ =>
 159        (exactMidpointBlochSymbol H (fun j => t * dir j) -
 160            exactMidpointBlochSymbolZero H) / (t ^ 2 * n))
 161      (𝓝[≠] (0 : ℝ)) (nhds (exactMidpointBlochM2 H dir / n)) := by
 162  have h := tendsto_exactMidpointBloch_centered_div_sq H dir
 163  have hdiv := h.div_const n
 164  refine (tendsto_congr' ?_).mpr hdiv
 165  filter_upwards [self_mem_nhdsWithin] with t ht
 166  field_simp [ht, hn]
 167
 168/-! ## §3. Status -/
 169
 170structure ExactBlochSymbolStatus where
 171  trigPolyNamed : Bool
 172  abstractTendstoProved : Bool
 173  specializedTendstoProved : Bool
 174  normalizationGatePass : Bool
 175  srsInhabited : Bool
 176  gapActionRecovery : Bool
 177
 178def exactBlochSymbolStatus : ExactBlochSymbolStatus where
 179  trigPolyNamed := true
 180  abstractTendstoProved := true
 181  specializedTendstoProved := true
 182  normalizationGatePass := true
 183  srsInhabited := false
 184  gapActionRecovery := false
 185
 186theorem exactBlochSymbolStatus_flags :
 187    exactBlochSymbolStatus.trigPolyNamed = true ∧
 188      exactBlochSymbolStatus.abstractTendstoProved = true ∧
 189        exactBlochSymbolStatus.specializedTendstoProved = true ∧
 190          exactBlochSymbolStatus.normalizationGatePass = true ∧
 191            exactBlochSymbolStatus.srsInhabited = false ∧
 192              exactBlochSymbolStatus.gapActionRecovery = false :=
 193  ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
 194
 195theorem gate_passes_with_discrete_bookkeeping :
 196    NormalizationGatePass = true ∧
 197      discreteBookkeepingFactor * exactUnitFrobeniusTTCoefficient =
 198        frozenPreflightEHCoefficient ∧
 199          continuumEHDiscreteFace (1 : ℝ) = frozenPreflightEHCoefficient :=
 200  ⟨normalizationGatePass_true, frozen_EH_is_discrete_bookkeeping_times_unitF.symm,
 201    continuumEHDiscreteFace_on_unitF⟩
 202
 203/-- Compat alias: former option-C gate name. -/
 204theorem gate_passes_under_restatement_C :
 205    NormalizationGatePass = true ∧
 206      einsteinHilbertTTCoefficient4D_unitFrobenius =
 207        exactUnitFrobeniusTTCoefficient :=
 208  ⟨normalizationGatePass_true, unitFrobenius_EH_eq_exact⟩
 209
 210/-- Re-export: abstract centered Tendsto is available for any weight/phase. -/
 211theorem abstract_centered_tendsto_available
 212    {ι : Type*} (w θ : ι → ℝ) (s : Finset ι) :
 213    Filter.Tendsto (fun t : ℝ => centeredTrigPoly w θ s t / t ^ 2)
 214      (nhdsWithin 0 {0}ᶜ) (nhds (centeredTrigPolyM2 w θ s)) :=
 215  tendsto_centeredTrigPoly_div_sq w θ s
 216
 217/-- Historical residual string (closed by irreducible specialization). -/
 218def typedResidual_exact_bloch_fin1208_specialize : String :=
 219  "CLOSED: tendsto_exactMidpointBloch_centered_div_sq via irreducible couplingUniv/weightFn/phaseFn; abstract Tendsto specialized without Fin-1208 array whnf."
 220
 221end
 222
 223end ReggeExactFlatHessianBlochSymbol4D
 224end Analysis
 225end Gravity
 226end IndisputableMonolith
 227