IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   3
   4/-!
   5# Regge edge TT attachment (4D), plane-wave layer
   6
   7QG full-theory campaign, Wave 4 / lane W4-1 (`edge_tt_decomposition`),
   8next kernel-checked increment after the algebraic `EdgeTTDecomposition4D`
   9layer: attach the Euclidean `4 × 4` TT / gauge / transverse-trace split to
  10**plane-wave EDGE loadings** on axis edges of the 4-torus, using the same
  11quadratic-form convention as the 3D chain
  12(`polEdgeCoeff E d = Σᵢⱼ Eᵢⱼ Dⁱ Dʲ` in `ReggeTTSymbolPreflight`).
  13
  14## Tier tags (binding)
  15
  16* THEOREM: every named result in this file (kernel-checked; no `sorry`, no
  17  `admit`, no new axioms, no `native_decide`, no `: True` shells).
  18* This does **not** prove the ledger name `edge_tt_decomposition` in full
  19  (no 4D Regge action, no continuum Einstein-Hilbert recovery, no full
  20  Freudenthal edge-class stencil in 4D).
  21* This does **not** prove `S_RS_converges_EH_4d`.
  22* This does **not** flip `gap_action_recovery`.
  23
  24## What is proved (honest scope)
  25
  261. **4D plane-wave edge map.** For a matrix `H` and wave covector `m`, the
  27   axis-edge squared-length loading is `edgeLoad H (axisDisp a) = H a a`,
  28   and the midpoint plane-wave perturbation is that load times
  29   `cos(m·x + mₐ/2)`, mirroring the 3D midpoint convention.
  302. **Linearity + decomposition transport.** The edge load (hence the
  31   plane-wave edge perturbation) of `H` equals the sum of the loads of
  32   `ttProject`, `gaugePart`, and the residual transverse-trace part, by
  33   linearity of `edgeLoad` plus `exists_edgeTTDecomposition`.
  343. **Gauge ↔ discrete Lie (exact finite-difference identity).** For
  35   `gaugePart m v` on the axis edge `a`,
  36   `edgeLoad (gaugePart m v) (axisDisp a) = 2 mₐ vₐ`.
  37   The plane-wave vertex field `ξ_b(x) = v_b sin(m·x)` has discrete
  38   Lie loading
  39   `2 (ξ_a(x+eₐ) - ξ_a(x)) = 4 vₐ sin(mₐ/2) cos(m·x + mₐ/2)`.
  40   Therefore the matrix-gauge plane-wave edge perturbation equals
  41   `(mₐ / (2 sin(mₐ/2)))` times that discrete Lie loading whenever
  42   `sin(mₐ/2) ≠ 0`.  This is the exact lattice identity; it is **not**
  43   the continuum claim `δℓ² = 2 ∂_a ξ_a`.
  44
  45Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  46-/
  47
  48namespace IndisputableMonolith
  49namespace Gravity
  50namespace Analysis
  51namespace ReggeEdgeTTAttachment4D
  52
  53open Matrix BigOperators
  54open EdgeTTDecomposition4D
  55
  56noncomputable section
  57
  58/-! ## §1. 4D axis edges and edge loadings (3D `polEdgeCoeff` convention) -/
  59
  60/-- Unit axis displacement in direction `a` on `Fin 4`. -/
  61def axisDisp (a : Fin 4) : Fin 4 → ℝ :=
  62  fun i => if i = a then (1 : ℝ) else 0
  63
  64/-- Quadratic edge loading `Dᵀ H D = Σᵢⱼ Hᵢⱼ Dⁱ Dʲ` (same convention as
  653D `polEdgeCoeff`). -/
  66def edgeLoad (H : Mat4) (d : Fin 4 → ℝ) : ℝ :=
  67  ∑ i : Fin 4, ∑ j : Fin 4, H i j * d i * d j
  68
  69/-- Midpoint phase of an axis edge based at covering-space coordinate `x`
  70with wave covector `m`: `m · (x + eₐ/2)`. -/
  71def axisMidpointPhase (m x : Fin 4 → ℝ) (a : Fin 4) : ℝ :=
  72  (∑ i : Fin 4, m i * x i) + m a / 2
  73
  74/-- Plane-wave squared-length perturbation amplitude on the axis edge
  75from `x` to `x+eₐ` induced by matrix `H` (the `t`-linear coefficient in
  76the 3D family `ℓ² = ℓ²_flat + t · c_d · cos(mid)`). -/
  77def planeWaveAxisEdgePert (H : Mat4) (m x : Fin 4 → ℝ) (a : Fin 4) : ℝ :=
  78  edgeLoad H (axisDisp a) * Real.cos (axisMidpointPhase m x a)
  79
  80/-! ## §2. Elementary edge-load algebra -/
  81
  82theorem axisDisp_apply (a i : Fin 4) :
  83    axisDisp a i = if i = a then (1 : ℝ) else 0 := rfl
  84
  85theorem edgeLoad_axis (H : Mat4) (a : Fin 4) :
  86    edgeLoad H (axisDisp a) = H a a := by
  87  unfold edgeLoad axisDisp
  88  simp [Finset.sum_ite_eq']
  89
  90theorem edgeLoad_add (A B : Mat4) (d : Fin 4 → ℝ) :
  91    edgeLoad (A + B) d = edgeLoad A d + edgeLoad B d := by
  92  unfold edgeLoad
  93  simp [add_apply, add_mul, Finset.sum_add_distrib]
  94
  95theorem edgeLoad_smul (c : ℝ) (H : Mat4) (d : Fin 4 → ℝ) :
  96    edgeLoad (c • H) d = c * edgeLoad H d := by
  97  unfold edgeLoad
  98  simp only [smul_apply, smul_eq_mul]
  99  calc
 100    ∑ i : Fin 4, ∑ j : Fin 4, c * H i j * d i * d j
 101        = ∑ i : Fin 4, ∑ j : Fin 4, c * (H i j * d i * d j) := by
 102      refine Finset.sum_congr rfl fun i _ =>
 103        Finset.sum_congr rfl fun j _ => by ring
 104    _ = c * ∑ i : Fin 4, ∑ j : Fin 4, H i j * d i * d j := by
 105      simp [Finset.mul_sum]
 106
 107theorem edgeLoad_neg (H : Mat4) (d : Fin 4 → ℝ) :
 108    edgeLoad (-H) d = -edgeLoad H d := by
 109  simpa [neg_one_smul] using edgeLoad_smul (-1) H d
 110
 111theorem edgeLoad_sub (A B : Mat4) (d : Fin 4 → ℝ) :
 112    edgeLoad (A - B) d = edgeLoad A d - edgeLoad B d := by
 113  rw [sub_eq_add_neg, edgeLoad_add, edgeLoad_neg]
 114  ring
 115
 116theorem planeWaveAxisEdgePert_add (A B : Mat4) (m x : Fin 4 → ℝ) (a : Fin 4) :
 117    planeWaveAxisEdgePert (A + B) m x a =
 118      planeWaveAxisEdgePert A m x a + planeWaveAxisEdgePert B m x a := by
 119  unfold planeWaveAxisEdgePert
 120  rw [edgeLoad_add, add_mul]
 121
 122theorem planeWaveAxisEdgePert_smul (c : ℝ) (H : Mat4) (m x : Fin 4 → ℝ)
 123    (a : Fin 4) :
 124    planeWaveAxisEdgePert (c • H) m x a =
 125      c * planeWaveAxisEdgePert H m x a := by
 126  unfold planeWaveAxisEdgePert
 127  rw [edgeLoad_smul, mul_assoc]
 128
 129/-! ## §3. Gauge matrix → edge load (algebraic Lie symbol) -/
 130
 131theorem edgeLoad_gaugePart (m v d : Fin 4 → ℝ) :
 132    edgeLoad (gaugePart m v) d =
 133      2 * (∑ i : Fin 4, m i * d i) * (∑ j : Fin 4, v j * d j) := by
 134  -- Direct: Dᵀ (m⊗v+v⊗m) D = 2 (m·D)(v·D).  Expand on axis basis later;
 135  -- here prove by rewriting each summand.
 136  have hαβ :
 137      (∑ i : Fin 4, ∑ j : Fin 4, m i * v j * d i * d j) =
 138        (∑ i : Fin 4, m i * d i) * (∑ j : Fin 4, v j * d j) := by
 139    calc
 140      ∑ i : Fin 4, ∑ j : Fin 4, m i * v j * d i * d j
 141          = ∑ i : Fin 4, ∑ j : Fin 4, (m i * d i) * (v j * d j) := by
 142        refine Finset.sum_congr rfl fun i _ =>
 143          Finset.sum_congr rfl fun j _ => by ring
 144      _ = ∑ i : Fin 4, (m i * d i) * ∑ j : Fin 4, v j * d j := by
 145        refine Finset.sum_congr rfl fun i _ => ?_
 146        rw [← Finset.mul_sum]
 147      _ = (∑ i : Fin 4, m i * d i) * (∑ j : Fin 4, v j * d j) := by
 148        rw [← Finset.sum_mul]
 149  have hβα :
 150      (∑ i : Fin 4, ∑ j : Fin 4, v i * m j * d i * d j) =
 151        (∑ i : Fin 4, v i * d i) * (∑ j : Fin 4, m j * d j) := by
 152    calc
 153      ∑ i : Fin 4, ∑ j : Fin 4, v i * m j * d i * d j
 154          = ∑ i : Fin 4, ∑ j : Fin 4, (v i * d i) * (m j * d j) := by
 155        refine Finset.sum_congr rfl fun i _ =>
 156          Finset.sum_congr rfl fun j _ => by ring
 157      _ = ∑ i : Fin 4, (v i * d i) * ∑ j : Fin 4, m j * d j := by
 158        refine Finset.sum_congr rfl fun i _ => ?_
 159        rw [← Finset.mul_sum]
 160      _ = (∑ i : Fin 4, v i * d i) * (∑ j : Fin 4, m j * d j) := by
 161        rw [← Finset.sum_mul]
 162  unfold edgeLoad gaugePart
 163  calc
 164    ∑ i : Fin 4, ∑ j : Fin 4, (m i * v j + v i * m j) * d i * d j
 165        = ∑ i : Fin 4, ∑ j : Fin 4,
 166            (m i * v j * d i * d j + v i * m j * d i * d j) := by
 167      refine Finset.sum_congr rfl fun i _ =>
 168        Finset.sum_congr rfl fun j _ => by ring
 169    _ = (∑ i : Fin 4, ∑ j : Fin 4, m i * v j * d i * d j) +
 170          (∑ i : Fin 4, ∑ j : Fin 4, v i * m j * d i * d j) := by
 171      simp [Finset.sum_add_distrib]
 172    _ = (∑ i : Fin 4, m i * d i) * (∑ j : Fin 4, v j * d j) +
 173          (∑ i : Fin 4, v i * d i) * (∑ j : Fin 4, m j * d j) := by
 174      rw [hαβ, hβα]
 175    _ = 2 * (∑ i : Fin 4, m i * d i) * (∑ j : Fin 4, v j * d j) := by
 176      set α := ∑ i : Fin 4, m i * d i
 177      set β := ∑ i : Fin 4, v i * d i
 178      ring
 179
 180/-- Axis specialization: `edgeLoad (gaugePart m v) eₐ = 2 mₐ vₐ`. -/
 181theorem edgeLoad_gaugePart_axis (m v : Fin 4 → ℝ) (a : Fin 4) :
 182    edgeLoad (gaugePart m v) (axisDisp a) = 2 * m a * v a := by
 183  rw [edgeLoad_gaugePart]
 184  have hm : (∑ i : Fin 4, m i * axisDisp a i) = m a := by
 185    unfold axisDisp; simp [Finset.sum_ite_eq']
 186  have hv : (∑ j : Fin 4, v j * axisDisp a j) = v a := by
 187    unfold axisDisp; simp [Finset.sum_ite_eq']
 188  rw [hm, hv]
 189
 190/-! ## §4. Discrete Lie form of a plane-wave vertex shift -/
 191
 192/-- Plane-wave vertex displacement field `ξ_b(x) = v_b sin(m·x)`. -/
 193def gaugeVertexField (v m x : Fin 4 → ℝ) (b : Fin 4) : ℝ :=
 194  v b * Real.sin (∑ i : Fin 4, m i * x i)
 195
 196/-- Covering-space shift of the basepoint by one lattice step along axis `a`. -/
 197def shiftAxis (x : Fin 4 → ℝ) (a : Fin 4) : Fin 4 → ℝ :=
 198  fun i => if i = a then x i + 1 else x i
 199
 200/-- Discrete Lie loading of squared axis-edge length from the vertex field:
 201`2 (ξ_a(x+eₐ) - ξ_a(x))` (first-order change of `|eₐ + Δξ|²`). -/
 202def discreteLieAxis (v m x : Fin 4 → ℝ) (a : Fin 4) : ℝ :=
 203  2 * (gaugeVertexField v m (shiftAxis x a) a - gaugeVertexField v m x a)
 204
 205/-- Lattice derivative symbol along axis `a`: `2 sin(mₐ/2)`. -/
 206def latticeDerivSymbol (m : Fin 4 → ℝ) (a : Fin 4) : ℝ :=
 207  2 * Real.sin (m a / 2)
 208
 209theorem shiftAxis_dot (m x : Fin 4 → ℝ) (a : Fin 4) :
 210    (∑ i : Fin 4, m i * shiftAxis x a i) =
 211      (∑ i : Fin 4, m i * x i) + m a := by
 212  unfold shiftAxis
 213  have h (i : Fin 4) :
 214      m i * (if i = a then x i + 1 else x i) =
 215        m i * x i + m i * (if i = a then (1 : ℝ) else 0) := by
 216    split_ifs <;> ring
 217  simp_rw [h, Finset.sum_add_distrib]
 218  simp [Finset.sum_ite_eq']
 219
 220theorem sin_add_sub_sin (θ φ : ℝ) :
 221    Real.sin (θ + φ) - Real.sin θ =
 222      2 * Real.sin (φ / 2) * Real.cos (θ + φ / 2) := by
 223  have h := Real.sin_sub_sin (θ + φ) θ
 224  -- sin(A)-sin(B) = 2 sin((A-B)/2) cos((A+B)/2)
 225  have hAB : ((θ + φ) - θ) / 2 = φ / 2 := by ring
 226  have hsum : ((θ + φ) + θ) / 2 = θ + φ / 2 := by ring
 227  rw [h, hAB, hsum]
 228
 229/-- Exact trig expansion of the discrete Lie loading on an axis edge. -/
 230theorem discreteLieAxis_eq (v m x : Fin 4 → ℝ) (a : Fin 4) :
 231    discreteLieAxis v m x a =
 232      2 * v a * latticeDerivSymbol m a *
 233        Real.cos (axisMidpointPhase m x a) := by
 234  unfold discreteLieAxis gaugeVertexField axisMidpointPhase latticeDerivSymbol
 235  set θ : ℝ := ∑ i : Fin 4, m i * x i
 236  have hθ' : (∑ i : Fin 4, m i * shiftAxis x a i) = θ + m a :=
 237    shiftAxis_dot m x a
 238  simp only [hθ']
 239  have htrig := sin_add_sub_sin θ (m a)
 240  calc
 241    2 * (v a * Real.sin (θ + m a) - v a * Real.sin θ)
 242        = 2 * v a * (Real.sin (θ + m a) - Real.sin θ) := by ring
 243    _ = 2 * v a * (2 * Real.sin (m a / 2) * Real.cos (θ + m a / 2)) := by
 244      rw [htrig]
 245    _ = 2 * v a * (2 * Real.sin (m a / 2)) * Real.cos (θ + m a / 2) := by
 246      ring
 247
 248/-- Plane-wave edge perturbation of a gauge matrix on an axis edge. -/
 249theorem planeWaveAxisEdgePert_gaugePart (m v x : Fin 4 → ℝ) (a : Fin 4) :
 250    planeWaveAxisEdgePert (gaugePart m v) m x a =
 251      2 * m a * v a * Real.cos (axisMidpointPhase m x a) := by
 252  unfold planeWaveAxisEdgePert
 253  rw [edgeLoad_gaugePart_axis]
 254
 255/-- **THEOREM (exact finite-difference gauge identity).**
 256Whenever `sin(mₐ/2) ≠ 0`, the matrix-gauge plane-wave edge perturbation
 257equals `(mₐ / (2 sin(mₐ/2)))` times the discrete Lie loading of the
 258plane-wave vertex field.  Continuum `∂ ↦ multiply by m` is the small-`mₐ`
 259limit of this factor and is **not** claimed here. -/
 260theorem planeWaveAxisEdgePert_gaugePart_eq_discreteLie
 261    (m v x : Fin 4 → ℝ) (a : Fin 4)
 262    (hsin : Real.sin (m a / 2) ≠ 0) :
 263    planeWaveAxisEdgePert (gaugePart m v) m x a =
 264      (m a / latticeDerivSymbol m a) * discreteLieAxis v m x a := by
 265  have hden : latticeDerivSymbol m a ≠ 0 := by
 266    unfold latticeDerivSymbol
 267    exact mul_ne_zero two_ne_zero hsin
 268  rw [planeWaveAxisEdgePert_gaugePart, discreteLieAxis_eq]
 269  -- 2 mₐ vₐ cos = (mₐ / (2 sin(mₐ/2))) * (2 vₐ * (2 sin(mₐ/2)) * cos)
 270  unfold latticeDerivSymbol
 271  field_simp [hsin, hden]
 272
 273/-! ## §5. Decomposition transports to edge loads -/
 274
 275theorem edgeLoad_decomposition (m : Fin 4 → ℝ) (H : Mat4)
 276    (hH : IsSymmetric H) (hm : momentumSq m ≠ 0) (d : Fin 4 → ℝ) :
 277    edgeLoad H d =
 278      edgeLoad (ttProject m H) d +
 279        edgeLoad (gaugePart m (gaugeVector m H)) d +
 280        edgeLoad (residualTrace m H • transverseProjector m) d := by
 281  have h := (exists_edgeTTDecomposition m H hH hm).1
 282  -- Rewrite only the left-hand `H`, not the occurrences inside `ttProject m H`.
 283  conv_lhs => rw [h]
 284  rw [edgeLoad_add, edgeLoad_add]
 285
 286theorem planeWaveAxisEdgePert_decomposition (m : Fin 4 → ℝ) (H : Mat4)
 287    (hH : IsSymmetric H) (hm : momentumSq m ≠ 0) (x : Fin 4 → ℝ)
 288    (a : Fin 4) :
 289    planeWaveAxisEdgePert H m x a =
 290      planeWaveAxisEdgePert (ttProject m H) m x a +
 291        planeWaveAxisEdgePert (gaugePart m (gaugeVector m H)) m x a +
 292        planeWaveAxisEdgePert (residualTrace m H • transverseProjector m)
 293          m x a := by
 294  unfold planeWaveAxisEdgePert
 295  rw [edgeLoad_decomposition m H hH hm]
 296  ring
 297
 298/-! ## §6. TT matrices are fixed by the projector -/
 299
 300theorem load_eq_zero_of_isTT (m : Fin 4 → ℝ) (H : Mat4) (h : IsTT m H)
 301    (i : Fin 4) : load H m i = 0 :=
 302  h.2.2 i
 303
 304theorem gaugeVector_eq_zero_of_isTT (m : Fin 4 → ℝ) (H : Mat4)
 305    (hTT : IsTT m H) (_hm : momentumSq m ≠ 0) :
 306    gaugeVector m H = fun _ => 0 := by
 307  funext i
 308  unfold gaugeVector
 309  have hw : load H m = fun _ => 0 := by
 310    funext j; exact load_eq_zero_of_isTT m H hTT j
 311  have hdot : dot (fun _ : Fin 4 => (0 : ℝ)) m = 0 := by
 312    unfold dot; simp
 313  simp [hw, hdot]
 314
 315theorem gaugePart_zero (m : Fin 4 → ℝ) :
 316    gaugePart m (fun _ => (0 : ℝ)) = 0 := by
 317  funext i j
 318  simp [gaugePart]
 319
 320theorem gaugeCorrected_eq_of_isTT (m : Fin 4 → ℝ) (H : Mat4)
 321    (hTT : IsTT m H) (hm : momentumSq m ≠ 0) :
 322    gaugeCorrected m H = H := by
 323  unfold gaugeCorrected
 324  rw [gaugeVector_eq_zero_of_isTT m H hTT hm, gaugePart_zero]
 325  simp
 326
 327theorem residualTrace_eq_zero_of_isTT (m : Fin 4 → ℝ) (H : Mat4)
 328    (hTT : IsTT m H) (hm : momentumSq m ≠ 0) :
 329    residualTrace m H = 0 := by
 330  unfold residualTrace
 331  rw [gaugeCorrected_eq_of_isTT m H hTT hm]
 332  have := hTT.2.1
 333  simp [IsTraceless] at this
 334  simp [this]
 335
 336theorem ttProject_eq_of_isTT (m : Fin 4 → ℝ) (H : Mat4)
 337    (hTT : IsTT m H) (hm : momentumSq m ≠ 0) :
 338    ttProject m H = H := by
 339  unfold ttProject
 340  rw [gaugeCorrected_eq_of_isTT m H hTT hm,
 341    residualTrace_eq_zero_of_isTT m H hTT hm]
 342  simp
 343
 344/-! ## §7. Decoy: a non-gauge matrix is not a discrete Lie shift -/
 345
 346/-- Decoy witness matrix: the algebraic plus TT polarization
 347`diag(0,0,1,−1)` against `axisWave`. -/
 348def decoyTT : Mat4 := axisTTPlus
 349
 350/-- A plane-wave edge perturbation equals some gauge discrete-Lie form on
 351axis `a` when there exists `v` with matching axis load `2 mₐ vₐ`. -/
 352def IsGaugeDiscreteLieOnAxis (m : Fin 4 → ℝ) (H : Mat4) (a : Fin 4) :
 353    Prop :=
 354  ∃ v : Fin 4 → ℝ, edgeLoad H (axisDisp a) = 2 * m a * v a
 355
 356theorem decoyTT_edgeLoad_axis2 :
 357    edgeLoad decoyTT (axisDisp 2) = 1 := by
 358  simp [decoyTT, edgeLoad_axis, axisTTPlus]
 359
 360theorem decoyTT_not_gaugeDiscreteLie_axis2 :
 361    ¬ IsGaugeDiscreteLieOnAxis axisWave decoyTT 2 := by
 362  rintro ⟨v, hv⟩
 363  have hm : axisWave 2 = 0 := by simp [axisWave]
 364  rw [decoyTT_edgeLoad_axis2, hm] at hv
 365  norm_num at hv
 366
 367theorem decoyTT_isTT : IsTT axisWave decoyTT :=
 368  axisTTPlus_isTT
 369
 370/-! ## §8. Nonvacuity: a concrete nonzero TT edge perturbation -/
 371
 372def witnessWave : Fin 4 → ℝ := axisWave
 373def witnessH : Mat4 := axisTTPlus
 374def witnessBase : Fin 4 → ℝ := fun _ => 0
 375
 376theorem witness_isTT : IsTT witnessWave witnessH :=
 377  axisTTPlus_isTT
 378
 379theorem witness_momentumSq : momentumSq witnessWave ≠ 0 := by
 380  simp [witnessWave, axisWave_momentumSq]
 381
 382theorem witness_ttProject_eq : ttProject witnessWave witnessH = witnessH :=
 383  ttProject_eq_of_isTT witnessWave witnessH witness_isTT witness_momentumSq
 384
 385theorem witness_edgeLoad_tt_ne_zero :
 386    edgeLoad (ttProject witnessWave witnessH) (axisDisp 2) ≠ 0 := by
 387  rw [witness_ttProject_eq, edgeLoad_axis]
 388  simp [witnessH, axisTTPlus]
 389
 390theorem witness_tt_edge_ne_zero :
 391    planeWaveAxisEdgePert (ttProject witnessWave witnessH) witnessWave
 392        witnessBase 2 ≠ 0 := by
 393  unfold planeWaveAxisEdgePert
 394  rw [witness_ttProject_eq, edgeLoad_axis]
 395  simp [witnessH, witnessWave, witnessBase, axisTTPlus, axisMidpointPhase,
 396    axisWave, Real.cos_zero]
 397
 398end
 399
 400end ReggeEdgeTTAttachment4D
 401end Analysis
 402end Gravity
 403end IndisputableMonolith
 404