IndisputableMonolith.Gravity.SevenGaps.DiscreteLichnerowicz

   1import Mathlib
   2
   3/-!
   4# Discrete Lichnerowicz operator: flat 3-torus TT spectrum convergence
   5
   6Seven-Gaps campaign, Lane 4 ("operator convergence" gap).
   7
   8This file builds the first genuine Lean connection between the discrete
   9perturbation spectrum on a lattice and the continuum Lichnerowicz operator,
  10on the FLAT 3-torus background. Nothing here imports or cites the old
  11`Relativity/` GW files (which are vacuous).
  12
  13## AXIS-SECTOR SCOPE (re-tagged 2026-07-15, panel mandate C14)
  14
  15Every convergence result in this file is proved along the AXIS stencil
  16sector only: plane waves `k = (k, 0, 0)` acted on by the componentwise
  17axis-stencil Laplacian `discLap3`. Test G
  18(`Gravity.Analysis.FreudenthalStencilPreflight` /
  19`Gravity.Analysis.FreudenthalEnergyLimit`, commits 7b808f75b4 and
  201d3ed6da06) kernel-proved that the continuum moment tensor of the
  21canonical Freudenthal frozen quadratic energy is ANISOTROPIC:
  22`A₀ = (1+√2)·I + (√2+√3)·J`, with the body-diagonal direction roughly
  234.9x stiffer than an axis direction. Axis stencils are blind to that
  24anisotropy, so the axis-sector results below MUST NOT be read as
  25isotropic flat-space recovery of the full Lichnerowicz spectrum. The
  26direction-resolved symbol question is governed by the C10 probe (plan
  27receipt P-iso, 2026-07-15).
  28
  29## Representation choice
  30
  31Lattice functions are represented as N-periodic functions `ℤ → ℂ` (period `N`,
  32spacing `h = 1/N` on the unit circle), NOT as functions on `ZMod N`. This
  33avoids `ZMod.val` wraparound arithmetic entirely: the discrete Laplacian
  34stencil and the Fourier-mode eigenvalue identity hold pointwise for every
  35`j : ℤ`, and periodicity of the modes (`fourierMode_periodic`) is what
  36grounds the torus interpretation. 3D lattice sites are `ℤ × ℤ × ℤ` with
  37periodicity along each axis (`planeH_periodic_axis`, `planeH_shift_yz`).
  38
  39## Honest tiers
  40
  41* THEOREM (proved below, axiom-clean):
  42  - `discLap_fourierMode` / `discLap_fourierMode_apply`: the Fourier mode
  43    `exp(2πik j/N)` is an eigenvector of the spacing-normalized discrete
  44    Laplacian with eigenvalue `-(4 N² sin²(πk/N))`.
  45  - `discreteEigenvalue_tendsto`: for fixed wavenumber `k`, the discrete
  46    (positive, i.e. minus-Laplacian) eigenvalue `4 N² sin²(πk/N)` of the
  47    AXIS mode converges to `(2πk)²` as the lattice is refined (`N → ∞`).
  48    Axis sector only; see the scope note above.
  49  - `planeH_transverse`: the axis plane wave with first-row-zero polarization
  50    is exactly discrete-transverse (forward-difference divergence ≡ 0).
  51  - `epsPlus_*` / `epsCross_*` / `polarizations_linearIndependent`: the two
  52    standard TT polarizations are symmetric, traceless, first-row/column
  53    zero, and linearly independent over ℂ.
  54  - `discLap3_planeH`: the 3D axis plane wave is an eigenvector of the 3D
  55    discrete Laplacian with the same eigenvalue as the 1D mode.
  56  - `continuumProfile_hasDerivAt` / `continuumProfile_second_deriv`: the
  57    continuum plane-wave profile `exp(2πik t)` has second derivative
  58    `-(2πk)²` times itself, so `(2πk)²` is the genuine `-Δ` eigenvalue of
  59    the continuum mode along the wave direction.
  60
  61* MODEL (definitional, justified in docstring, not a curved-space theorem):
  62  - `lichnerowiczFlatEigenvalue`: on a flat background the Lichnerowicz
  63    operator on TT tensors reduces to `-Δ` (the Riemann curvature term
  64    vanishes identically), so its eigenvalue on the wavenumber-`k` TT plane
  65    wave is `(2πk)²`. We encode this reduction as a definition; no
  66    curved-space geometry is formalized or claimed here.
  67
  68* OPEN: curved backgrounds (Schwarzschild, Kerr) and quasinormal-mode
  69  spectra are NOT treated. See `status` flags at the bottom.
  70
  71The packaged claim (`discrete_tt_spectrum_converges_to_flat_lichnerowicz`):
  72discrete TT eigenvalues of AXIS modes converge to `(2πk)²`, the flat
  73Lichnerowicz eigenvalue on that axis sector. Per the AXIS-SECTOR SCOPE
  74note above, this is a sector statement, not isotropic flat-space recovery.
  75-/
  76
  77namespace IndisputableMonolith
  78namespace Gravity
  79namespace SevenGaps
  80namespace DiscreteLichnerowicz
  81
  82open Filter Topology
  83
  84/-! ## 1D core: lattice functions on the unit circle -/
  85
  86/-- Spacing-normalized 1D discrete Laplacian for a lattice of `N` sites on
  87the unit circle (spacing `h = 1/N`): `(discLap f) j = (f(j+1) - 2 f(j) + f(j-1)) / h²`. -/
  88noncomputable def discLap (N : ℕ) (f : ℤ → ℂ) : ℤ → ℂ :=
  89  fun j => (N : ℂ) ^ 2 * (f (j + 1) - 2 * f j + f (j - 1))
  90
  91/-- Fourier mode of wavenumber `k` on the `N`-site lattice:
  92`j ↦ exp(2πi k j / N)`. -/
  93noncomputable def fourierMode (N : ℕ) (k : ℤ) : ℤ → ℂ :=
  94  fun j => Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * (j : ℂ) / (N : ℂ))
  95
  96/-- THEOREM. The Fourier mode is `N`-periodic: it genuinely lives on the
  97`N`-site discrete circle (torus). For `N = 0` periodicity is trivial. -/
  98theorem fourierMode_periodic (N : ℕ) (k : ℤ) :
  99    Function.Periodic (fourierMode N k) (N : ℤ) := by
 100  intro j
 101  rcases Nat.eq_zero_or_pos N with h | h
 102  · subst h; simp
 103  · have hN : (N : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr h.ne'
 104    simp only [fourierMode]
 105    have hexp : 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * ((j + (N : ℤ) : ℤ) : ℂ) / (N : ℂ)
 106        = 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * (j : ℂ) / (N : ℂ)
 107          + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := by
 108      push_cast
 109      field_simp
 110    rw [hexp, Complex.exp_add, Complex.exp_int_mul_two_pi_mul_I, mul_one]
 111
 112/-- One-step shift of the Fourier mode: multiplication by `exp(iθ)` with
 113`θ = 2πk/N`. -/
 114lemma fourierMode_step (N : ℕ) (k : ℤ) (j : ℤ) :
 115    fourierMode N k (j + 1)
 116      = fourierMode N k j
 117        * Complex.exp (((2 * Real.pi * (k : ℝ) / (N : ℝ) : ℝ) : ℂ) * Complex.I) := by
 118  simp only [fourierMode]
 119  rw [← Complex.exp_add]
 120  congr 1
 121  push_cast
 122  ring
 123
 124/-- One-step down-shift of the Fourier mode: multiplication by `exp(-iθ)`. -/
 125lemma fourierMode_step_down (N : ℕ) (k : ℤ) (j : ℤ) :
 126    fourierMode N k (j - 1)
 127      = fourierMode N k j
 128        * Complex.exp (-(((2 * Real.pi * (k : ℝ) / (N : ℝ) : ℝ) : ℂ) * Complex.I)) := by
 129  simp only [fourierMode]
 130  rw [← Complex.exp_add]
 131  congr 1
 132  push_cast
 133  ring
 134
 135/-- `exp(iθ) + exp(-iθ) = 2 cos θ` for real `θ` (viewed in ℂ). -/
 136lemma exp_add_exp_neg_mul_I (θ : ℝ) :
 137    Complex.exp ((θ : ℂ) * Complex.I) + Complex.exp (-((θ : ℂ) * Complex.I))
 138      = 2 * Complex.cos (θ : ℂ) := by
 139  rw [show -((θ : ℂ) * Complex.I) = (-(θ : ℂ)) * Complex.I by ring]
 140  rw [Complex.exp_mul_I, Complex.exp_mul_I, Complex.cos_neg, Complex.sin_neg]
 141  ring
 142
 143/-- THEOREM (pointwise eigenvalue identity). The discrete Laplacian acts on
 144the Fourier mode by the scalar `-(4 N² sin²(πk/N))`, at every lattice point.
 145Derivation: `f(j±1) = f(j) exp(±iθ)`, `exp(iθ)+exp(-iθ) = 2cos θ`, and
 146`2cos θ - 2 = -4 sin²(θ/2)` with `θ = 2πk/N`. -/
 147theorem discLap_fourierMode_apply (N : ℕ) (k : ℤ) (j : ℤ) :
 148    discLap N (fourierMode N k) j
 149      = ((-(4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2) : ℝ) : ℂ)
 150          * fourierMode N k j := by
 151  have hstep := fourierMode_step N k j
 152  have hstepd := fourierMode_step_down N k j
 153  have hsum := exp_add_exp_neg_mul_I (2 * Real.pi * (k : ℝ) / (N : ℝ))
 154  have hreal : (2 * Real.cos (2 * Real.pi * (k : ℝ) / (N : ℝ)) - 2 : ℝ)
 155      = -(4 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2) := by
 156    have h := Real.sin_sq_eq_half_sub (x := Real.pi * (k : ℝ) / (N : ℝ))
 157    have h2 : 2 * (Real.pi * (k : ℝ) / (N : ℝ)) = 2 * Real.pi * (k : ℝ) / (N : ℝ) := by
 158      ring
 159    rw [h2] at h
 160    linarith
 161  simp only [discLap]
 162  rw [hstep, hstepd]
 163  rw [show (N : ℂ) ^ 2 *
 164        (fourierMode N k j
 165            * Complex.exp (((2 * Real.pi * (k : ℝ) / (N : ℝ) : ℝ) : ℂ) * Complex.I)
 166          - 2 * fourierMode N k j
 167          + fourierMode N k j
 168            * Complex.exp (-(((2 * Real.pi * (k : ℝ) / (N : ℝ) : ℝ) : ℂ) * Complex.I)))
 169      = (N : ℂ) ^ 2 * fourierMode N k j *
 170          ((Complex.exp (((2 * Real.pi * (k : ℝ) / (N : ℝ) : ℝ) : ℂ) * Complex.I)
 171            + Complex.exp (-(((2 * Real.pi * (k : ℝ) / (N : ℝ) : ℝ) : ℂ) * Complex.I))) - 2)
 172      by ring]
 173  rw [hsum, ← Complex.ofReal_cos]
 174  calc (N : ℂ) ^ 2 * fourierMode N k j
 175        * (2 * ((Real.cos (2 * Real.pi * (k : ℝ) / (N : ℝ)) : ℝ) : ℂ) - 2)
 176      = ((2 * Real.cos (2 * Real.pi * (k : ℝ) / (N : ℝ)) - 2 : ℝ) : ℂ)
 177          * ((N : ℂ) ^ 2 * fourierMode N k j) := by
 178        push_cast
 179        ring
 180    _ = ((-(4 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2) : ℝ) : ℂ)
 181          * ((N : ℂ) ^ 2 * fourierMode N k j) := by
 182        rw [hreal]
 183    _ = ((-(4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2) : ℝ) : ℂ)
 184          * fourierMode N k j := by
 185        push_cast
 186        ring
 187
 188/-- THEOREM (eigenvalue identity, function form).
 189`discLap (fourierMode k) = -(4 N² sin²(πk/N)) • fourierMode k`. -/
 190theorem discLap_fourierMode (N : ℕ) (k : ℤ) :
 191    discLap N (fourierMode N k)
 192      = (-(4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2)) • fourierMode N k := by
 193  funext j
 194  rw [Pi.smul_apply, Complex.real_smul]
 195  exact discLap_fourierMode_apply N k j
 196
 197/-! ## Convergence of the discrete spectrum -/
 198
 199/-- The (positive, minus-Laplacian) discrete eigenvalue of the wavenumber-`k`
 200mode on the `N`-site lattice: `4 N² sin²(πk/N)`. -/
 201noncomputable def discreteEigenvalue (N k : ℕ) : ℝ :=
 202  4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2
 203
 204/-- THEOREM (the core convergence result; AXIS SECTOR ONLY). For fixed
 205wavenumber `k`, the discrete eigenvalue `4 N² sin²(πk/N)` of the AXIS mode
 206converges to the continuum eigenvalue `(2πk)²` as the lattice is refined.
 207Proof: `4N² sin²(πk/N) = (2πk)² (sin x / x)²` with `x = πk/N → 0`, and
 208`sin x / x → 1` at `0` (from `HasDerivAt sin 1 0` via the slope
 209characterization); the wavenumber `k = 0` is handled separately (both sides
 210vanish identically).
 211
 212Scope: this is a statement about axis-aligned modes of the axis-stencil
 213Laplacian. Test G (`FreudenthalStencilPreflight`/`FreudenthalEnergyLimit`,
 214commits 7b808f75b4, 1d3ed6da06) kernel-proved the full continuum moment
 215tensor is anisotropic, `A₀ = (1+√2)I + (√2+√3)J`, which axis stencils
 216cannot see; do not read this as isotropic flat-space recovery. The
 217direction-resolved symbol question is governed by the C10 probe (plan
 218receipt P-iso, 2026-07-15). -/
 219theorem discreteEigenvalue_tendsto (k : ℕ) :
 220    Filter.Tendsto (fun N : ℕ => discreteEigenvalue N k) Filter.atTop
 221      (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) := by
 222  rcases Nat.eq_zero_or_pos k with hk | hk
 223  · subst hk
 224    have hzero : (fun N : ℕ => discreteEigenvalue N 0) = fun _ : ℕ => (0 : ℝ) := by
 225      funext N
 226      norm_num [discreteEigenvalue]
 227    rw [hzero]
 228    have h0 : ((2 * Real.pi * ((0 : ℕ) : ℝ)) ^ 2 : ℝ) = 0 := by norm_num
 229    rw [h0]
 230    exact tendsto_const_nhds
 231  · have hk' : (0 : ℝ) < (k : ℝ) := by exact_mod_cast hk
 232    -- sin y / y → 1 as y → 0 (through nonzero values)
 233    have hslope : Filter.Tendsto (fun y : ℝ => Real.sin y / y) (𝓝[≠] (0 : ℝ)) (nhds 1) := by
 234      have h := Real.hasDerivAt_sin 0
 235      rw [Real.cos_zero] at h
 236      have h2 := hasDerivAt_iff_tendsto_slope.mp h
 237      refine h2.congr ?_
 238      intro y
 239      rw [slope_def_field]
 240      simp
 241    -- x_N = πk/N → 0 within nonzero values
 242    have hx0 : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
 243        (nhds 0) := tendsto_const_div_atTop_nhds_zero_nat (Real.pi * (k : ℝ))
 244    have hxmem : ∀ᶠ N : ℕ in Filter.atTop,
 245        Real.pi * (k : ℝ) / (N : ℝ) ∈ ({0}ᶜ : Set ℝ) := by
 246      filter_upwards [Filter.eventually_ge_atTop 1] with N hN
 247      have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
 248      have hpos : 0 < Real.pi * (k : ℝ) / (N : ℝ) :=
 249        div_pos (mul_pos Real.pi_pos hk') hNpos
 250      simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
 251      exact ne_of_gt hpos
 252    have hx : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
 253        (𝓝[≠] (0 : ℝ)) :=
 254      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hx0 hxmem
 255    have hcomp := hslope.comp hx
 256    simp only [Function.comp_def] at hcomp
 257    have hmul : Filter.Tendsto
 258        (fun N : ℕ => (2 * Real.pi * (k : ℝ)) ^ 2
 259          * (Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) / (Real.pi * (k : ℝ) / (N : ℝ))) ^ 2)
 260        Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2 * 1 ^ 2)) :=
 261      tendsto_const_nhds.mul (hcomp.pow 2)
 262    rw [one_pow, mul_one] at hmul
 263    refine hmul.congr' ?_
 264    filter_upwards [Filter.eventually_ge_atTop 1] with N hN
 265    have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
 266    have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
 267    have hπk : Real.pi * (k : ℝ) ≠ 0 := ne_of_gt (mul_pos Real.pi_pos hk')
 268    simp only [discreteEigenvalue]
 269    field_simp
 270    ring
 271
 272/-- THEOREM (raw form of the convergence, as in the campaign brief; axis
 273sector only, see the scope note on `discreteEigenvalue_tendsto`). -/
 274theorem discrete_eigenvalue_tendsto_raw (k : ℕ) :
 275    Filter.Tendsto
 276      (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2)
 277      Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) :=
 278  discreteEigenvalue_tendsto k
 279
 280/-! ## 3D TT layer: lattice tensor fields on the 3-torus -/
 281
 282/-- 3D lattice site (periodic interpretation: the flat 3-torus). -/
 283abbrev Site3 : Type := ℤ × ℤ × ℤ
 284
 285/-- Lattice tensor field: a `3 × 3` complex matrix at every lattice site. -/
 286abbrev LatticeTensorField : Type := Site3 → Matrix (Fin 3) (Fin 3) ℂ
 287
 288/-- Lattice unit vectors along the three axes. -/
 289def unitVec : Fin 3 → Site3
 290  | 0 => (1, 0, 0)
 291  | 1 => (0, 1, 0)
 292  | 2 => (0, 0, 1)
 293
 294@[simp] lemma fst_add_e0 (x : Site3) : (x + unitVec 0).1 = x.1 + 1 := rfl
 295@[simp] lemma fst_sub_e0 (x : Site3) : (x - unitVec 0).1 = x.1 - 1 := rfl
 296@[simp] lemma fst_add_e1 (x : Site3) : (x + unitVec 1).1 = x.1 := add_zero _
 297@[simp] lemma fst_sub_e1 (x : Site3) : (x - unitVec 1).1 = x.1 := sub_zero _
 298@[simp] lemma fst_add_e2 (x : Site3) : (x + unitVec 2).1 = x.1 := add_zero _
 299@[simp] lemma fst_sub_e2 (x : Site3) : (x - unitVec 2).1 = x.1 := sub_zero _
 300
 301/-- Forward-difference discrete divergence of a lattice tensor field:
 302`(div H) x b = Σ_a N (H(x + e_a) a b - H(x) a b)`. -/
 303noncomputable def discDiv (N : ℕ) (H : LatticeTensorField) : Site3 → Fin 3 → ℂ :=
 304  fun x b => ∑ a : Fin 3, (N : ℂ) * (H (x + unitVec a) a b - H x a b)
 305
 306/-- 3D discrete Laplacian, componentwise sum of the three 1D stencils. -/
 307noncomputable def discLap3 (N : ℕ) (H : LatticeTensorField) : LatticeTensorField :=
 308  fun x => Matrix.of fun i j =>
 309    ∑ a : Fin 3, (N : ℂ) ^ 2 *
 310      (H (x + unitVec a) i j - 2 * H x i j + H (x - unitVec a) i j)
 311
 312/-- Axis plane wave `k = (k, 0, 0)`: the 1D Fourier mode in the first
 313coordinate times a constant polarization matrix. -/
 314noncomputable def planeH (N : ℕ) (k : ℤ) (eps : Matrix (Fin 3) (Fin 3) ℂ) :
 315    LatticeTensorField :=
 316  fun x => fourierMode N k x.1 • eps
 317
 318lemma planeH_apply (N : ℕ) (k : ℤ) (eps : Matrix (Fin 3) (Fin 3) ℂ)
 319    (x : Site3) (i j : Fin 3) :
 320    planeH N k eps x i j = fourierMode N k x.1 * eps i j := by
 321  simp [planeH, Matrix.smul_apply, smul_eq_mul]
 322
 323/-- THEOREM. The axis plane wave is periodic along the wave axis with period
 324`N` (torus grounding). -/
 325theorem planeH_periodic_axis (N : ℕ) (k : ℤ) (eps : Matrix (Fin 3) (Fin 3) ℂ)
 326    (x : Site3) :
 327    planeH N k eps (x + ((N : ℤ), 0, 0)) = planeH N k eps x := by
 328  show fourierMode N k (x.1 + (N : ℤ)) • eps = fourierMode N k x.1 • eps
 329  rw [fourierMode_periodic N k x.1]
 330
 331/-- THEOREM. The axis plane wave is invariant under arbitrary shifts in the
 332transverse (y, z) directions; in particular it is periodic along those axes. -/
 333theorem planeH_shift_yz (N : ℕ) (k : ℤ) (eps : Matrix (Fin 3) (Fin 3) ℂ)
 334    (x : Site3) (s t : ℤ) :
 335    planeH N k eps (x + ((0 : ℤ), s, t)) = planeH N k eps x := by
 336  show fourierMode N k (x.1 + 0) • eps = fourierMode N k x.1 • eps
 337  rw [add_zero]
 338
 339/-- THEOREM (discrete transversality). For a polarization with vanishing
 340first row, the axis plane wave is exactly discrete-transverse: the
 341forward-difference divergence vanishes identically. Only the `a = 0` term
 342could contribute (the mode is constant in `y, z`), and `eps 0 b = 0` kills it. -/
 343theorem planeH_transverse (N : ℕ) (k : ℤ) (eps : Matrix (Fin 3) (Fin 3) ℂ)
 344    (hrow : ∀ j, eps 0 j = 0) (x : Site3) (b : Fin 3) :
 345    discDiv N (planeH N k eps) x b = 0 := by
 346  simp only [discDiv, Fin.sum_univ_three, planeH_apply,
 347    fst_add_e0, fst_add_e1, fst_add_e2, hrow]
 348  ring
 349
 350/-- THEOREM (3D eigenvector identity). The axis plane wave is an eigenvector
 351of the 3D discrete Laplacian with the SAME eigenvalue as the 1D mode: the
 352`y, z` stencils act trivially on a mode constant in `y, z`. -/
 353theorem discLap3_planeH (N : ℕ) (k : ℤ) (eps : Matrix (Fin 3) (Fin 3) ℂ)
 354    (x : Site3) :
 355    discLap3 N (planeH N k eps) x
 356      = (-(4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2))
 357          • planeH N k eps x := by
 358  ext i j
 359  simp only [discLap3, Matrix.of_apply, Fin.sum_univ_three, planeH_apply,
 360    fst_add_e0, fst_sub_e0, fst_add_e1, fst_sub_e1, fst_add_e2, fst_sub_e2,
 361    Matrix.smul_apply, Complex.real_smul]
 362  have h1d := discLap_fourierMode_apply N k x.1
 363  simp only [discLap] at h1d
 364  linear_combination eps i j * h1d
 365
 366/-! ## Standard TT polarizations -/
 367
 368/-- Plus polarization: `diag(0, 1, -1)`. -/
 369def epsPlus : Matrix (Fin 3) (Fin 3) ℂ := !![0, 0, 0; 0, 1, 0; 0, 0, -1]
 370
 371/-- Cross polarization: `E₂₃ + E₃₂`. -/
 372def epsCross : Matrix (Fin 3) (Fin 3) ℂ := !![0, 0, 0; 0, 0, 1; 0, 1, 0]
 373
 374theorem epsPlus_isSymm : epsPlus.IsSymm := by
 375  ext i j
 376  fin_cases i <;> fin_cases j <;> simp [epsPlus]
 377
 378theorem epsCross_isSymm : epsCross.IsSymm := by
 379  ext i j
 380  fin_cases i <;> fin_cases j <;> simp [epsCross]
 381
 382theorem epsPlus_traceless : Matrix.trace epsPlus = 0 := by
 383  rw [Matrix.trace_fin_three]
 384  show (0 : ℂ) + 1 + (-1) = 0
 385  norm_num
 386
 387theorem epsCross_traceless : Matrix.trace epsCross = 0 := by
 388  rw [Matrix.trace_fin_three]
 389  show (0 : ℂ) + 0 + 0 = 0
 390  norm_num
 391
 392theorem epsPlus_row0 : ∀ j, epsPlus 0 j = 0 := by
 393  intro j
 394  fin_cases j <;> simp [epsPlus]
 395
 396theorem epsCross_row0 : ∀ j, epsCross 0 j = 0 := by
 397  intro j
 398  fin_cases j <;> simp [epsCross]
 399
 400theorem epsPlus_col0 : ∀ i, epsPlus i 0 = 0 := by
 401  intro i
 402  fin_cases i <;> simp [epsPlus]
 403
 404theorem epsCross_col0 : ∀ i, epsCross i 0 = 0 := by
 405  intro i
 406  fin_cases i <;> simp [epsCross]
 407
 408/-- THEOREM. The two standard polarizations are linearly independent over ℂ:
 409they span the 2D TT polarization space for the axis wave. -/
 410theorem polarizations_linearIndependent :
 411    LinearIndependent ℂ ![epsPlus, epsCross] := by
 412  rw [linearIndependent_fin2]
 413  constructor
 414  · intro h
 415    have h12 : (![epsPlus, epsCross] 1) 1 2 = (0 : Matrix (Fin 3) (Fin 3) ℂ) 1 2 := by
 416      rw [h]
 417    have e1 : (![epsPlus, epsCross] 1) 1 2 = (1 : ℂ) := rfl
 418    have e2 : ((0 : Matrix (Fin 3) (Fin 3) ℂ) 1 2 : ℂ) = 0 := rfl
 419    rw [e1, e2] at h12
 420    exact one_ne_zero h12
 421  · intro a h
 422    have h11 : (a • ![epsPlus, epsCross] 1) 1 1 = (![epsPlus, epsCross] 0) 1 1 := by
 423      rw [h]
 424    have e1 : (a • ![epsPlus, epsCross] 1) 1 1 = a * 0 := rfl
 425    have e2 : ((![epsPlus, epsCross] 0) 1 1 : ℂ) = 1 := rfl
 426    rw [e1, e2, mul_zero] at h11
 427    exact zero_ne_one h11
 428
 429/-! ## Flat Lichnerowicz connection (MODEL layer) -/
 430
 431/-- Continuum plane-wave profile along the wave axis: `t ↦ exp(2πik t)`. -/
 432noncomputable def continuumProfile (k : ℕ) (t : ℝ) : ℂ :=
 433  Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * (t : ℂ))
 434
 435/-- Continuum TT plane wave on the unit 3-torus (axis mode `k = (k,0,0)`). -/
 436noncomputable def continuumPlaneH (k : ℕ) (eps : Matrix (Fin 3) (Fin 3) ℂ) :
 437    (ℝ × ℝ × ℝ) → Matrix (Fin 3) (Fin 3) ℂ :=
 438  fun x => continuumProfile k x.1 • eps
 439
 440/-- THEOREM. First derivative of the continuum profile. -/
 441theorem continuumProfile_hasDerivAt (k : ℕ) (t : ℝ) :
 442    HasDerivAt (continuumProfile k)
 443      (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k t) t := by
 444  have hlin : HasDerivAt (fun s : ℝ => 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * ((s : ℝ) : ℂ))
 445      (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ)) t := by
 446    simpa using (Complex.ofRealCLM.hasDerivAt (x := t)).const_mul
 447      (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ))
 448  have hcomm : 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k t
 449      = continuumProfile k t * (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ)) := mul_comm _ _
 450  rw [hcomm]
 451  exact hlin.cexp
 452
 453/-- THEOREM. Second derivative of the continuum profile: `-(2πk)²` times the
 454profile. So `(2πk)²` is the genuine `-d²/dt²` eigenvalue of the continuum
 455mode along the wave direction (the mode is constant in the transverse
 456directions). -/
 457theorem continuumProfile_second_deriv (k : ℕ) (t : ℝ) :
 458    HasDerivAt (fun s : ℝ => 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k s)
 459      (((-((2 * Real.pi * (k : ℝ)) ^ 2) : ℝ) : ℂ) * continuumProfile k t) t := by
 460  have h := (continuumProfile_hasDerivAt k t).const_mul
 461    (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ))
 462  have heq : ((-((2 * Real.pi * (k : ℝ)) ^ 2) : ℝ) : ℂ) * continuumProfile k t
 463      = 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ)
 464        * (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k t) := by
 465    push_cast
 466    linear_combination (-4 * (Real.pi : ℂ) ^ 2 * (k : ℂ) ^ 2 * continuumProfile k t)
 467      * Complex.I_sq
 468  rw [heq]
 469  exact h
 470
 471/-- MODEL. Flat-background Lichnerowicz eigenvalue on the wavenumber-`k` TT
 472plane wave: `(2πk)²`.
 473
 474Justification (why this is the honest definition): the Lichnerowicz operator
 475on a Ricci-flat background acts on TT perturbations as
 476`Δ_L h_ab = -∇² h_ab - 2 R_acbd h^cd`. On the FLAT 3-torus the Riemann
 477tensor vanishes identically, so `Δ_L` reduces to `-∇²` (minus the flat
 478Laplacian) on TT tensors. The TT plane wave with wavenumber `k` along an
 479axis of the unit torus has `-∇²` eigenvalue `(2πk)²`; the along-axis part of
 480this is PROVED above (`continuumProfile_second_deriv`), and the transverse
 481derivatives vanish because the mode is constant in `y, z`. No curved-space
 482geometry is formalized here; this definition encodes the flat reduction
 483only. -/
 484noncomputable def lichnerowiczFlatEigenvalue (k : ℕ) : ℝ :=
 485  (2 * Real.pi * (k : ℝ)) ^ 2
 486
 487/-! ## Package theorem -/
 488
 489/-- THEOREM + MODEL (package; AXIS SECTOR ONLY). For every wavenumber `k`
 490and every polarization `eps` with vanishing first row (in particular
 491`epsPlus`, `epsCross`):
 492
 4931. the discrete axis plane wave is exactly discrete-transverse at every
 494   lattice resolution `N`;
 4952. it is an eigenvector of the 3D discrete Laplacian with eigenvalue
 496   `-(discreteEigenvalue N k)` at every resolution;
 4973. the discrete (minus-Laplacian) eigenvalues converge, as the lattice is
 498   refined, to `(2πk)²` = the flat Lichnerowicz eigenvalue (MODEL
 499   identification; see `lichnerowiczFlatEigenvalue`).
 500
 501Items 1-2 and the convergence in 3 are proved; only the name
 502"Lichnerowicz" on the limit is the MODEL layer.
 503
 504Scope caveat (panel mandate C14, 2026-07-15): everything here lives in the
 505AXIS stencil sector, `k = (k, 0, 0)` with the componentwise axis-stencil
 506Laplacian. Test G (`FreudenthalStencilPreflight`/`FreudenthalEnergyLimit`,
 507commits 7b808f75b4, 1d3ed6da06) kernel-proved the canonical Freudenthal
 508frozen quadratic energy has the ANISOTROPIC continuum moment tensor
 509`A₀ = (1+√2)I + (√2+√3)J` (body diagonal ~4.9x stiffer), which the axis
 510sector cannot detect. This theorem must therefore NOT be read as isotropic
 511flat-space recovery of the full Lichnerowicz spectrum; the
 512direction-resolved symbol question is governed by the C10 probe (plan
 513receipt P-iso, 2026-07-15). -/
 514theorem discrete_tt_spectrum_converges_to_flat_lichnerowicz
 515    (k : ℕ) (eps : Matrix (Fin 3) (Fin 3) ℂ) (hrow : ∀ j, eps 0 j = 0) :
 516    (∀ (N : ℕ) (x : Site3) (b : Fin 3),
 517        discDiv N (planeH N (k : ℤ) eps) x b = 0)
 518    ∧ (∀ (N : ℕ) (x : Site3),
 519        discLap3 N (planeH N (k : ℤ) eps) x
 520          = (-(discreteEigenvalue N k)) • planeH N (k : ℤ) eps x)
 521    ∧ Filter.Tendsto (fun N : ℕ => discreteEigenvalue N k) Filter.atTop
 522        (nhds (lichnerowiczFlatEigenvalue k)) := by
 523  refine ⟨fun N x b => planeH_transverse N (k : ℤ) eps hrow x b, fun N x => ?_, ?_⟩
 524  · have h := discLap3_planeH N (k : ℤ) eps x
 525    have hcast : (-(discreteEigenvalue N k) : ℝ)
 526        = -(4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * ((k : ℤ) : ℝ) / (N : ℝ)) ^ 2) := by
 527      simp [discreteEigenvalue]
 528    rw [hcast]
 529    exact h
 530  · exact discreteEigenvalue_tendsto k
 531
 532/-! ## Status flags (scoped claim; what remains OPEN) -/
 533
 534/-- Status record for the "operator convergence" gap. -/
 535structure OperatorConvergenceStatus where
 536  /-- Flat 3-torus TT convergence: proved in this file for the AXIS stencil
 537  sector only (`k = (k,0,0)` modes of the axis-stencil Laplacian). NOT
 538  isotropic flat-space recovery: Test G kernel-proved the full moment tensor
 539  is anisotropic, `A₀ = (1+√2)I + (√2+√3)J`. -/
 540  flat_tt_convergence_proved : Bool
 541  /-- Curved backgrounds (Schwarzschild, Kerr): NOT formalized; OPEN. -/
 542  curved_background_open : Bool
 543  /-- Quasinormal-mode spectra: NOT formalized; OPEN. -/
 544  qnm_spectrum_open : Bool
 545
 546/-- The scoped claim of this file, stated plainly: the discrete-to-continuum
 547operator convergence is PROVED on the flat 3-torus for TT AXIS modes only
 548(eigenvalue identity at every resolution + spectral convergence to the flat
 549Lichnerowicz eigenvalue `(2πk)²` on that sector). This is an axis-sector
 550statement, not isotropic flat-space recovery: Test G
 551(`FreudenthalStencilPreflight`/`FreudenthalEnergyLimit`, commits 7b808f75b4,
 5521d3ed6da06) kernel-proved the anisotropic moment tensor
 553`A₀ = (1+√2)I + (√2+√3)J`; the direction-resolved symbol question is
 554governed by the C10 probe (plan receipt P-iso, 2026-07-15). Curved
 555backgrounds and quasinormal-mode spectra remain OPEN: nothing in this file
 556(and nothing genuine elsewhere in the repository) formalizes them. -/
 557def status : OperatorConvergenceStatus :=
 558  { flat_tt_convergence_proved := true
 559    curved_background_open := true
 560    qnm_spectrum_open := true }
 561
 562theorem status_flat_tt_convergence_proved :
 563    status.flat_tt_convergence_proved = true := rfl
 564
 565theorem status_curved_background_open :
 566    status.curved_background_open = true := rfl
 567
 568theorem status_qnm_spectrum_open :
 569    status.qnm_spectrum_open = true := rfl
 570
 571end DiscreteLichnerowicz
 572end SevenGaps
 573end Gravity
 574end IndisputableMonolith
 575