IndisputableMonolith.Gravity.Analysis.OneModeCylinderPreflight

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.SpectralConvergence
   3
   4/-!
   5# One-mode cylinder-measure preflight (candidate C10 preflight; NOT the path-sum measure)
   6
   7QG full-theory campaign, Phase 2b SLACK lane M.
   8
   9## HONESTY / SCOPE HEADER (read before citing)
  10
  11This module is a ONE-MODE TOY PREFLIGHT for the panel's live bet C10 (a
  12Gaussian cylinder-measure limit over the frozen quadratic energy). It
  13
  14* is NOT the path-sum measure and does NOT construct any field-theoretic
  15  measure: everything here concerns a single Fourier mode `k` on a
  16  one-dimensional periodic lattice;
  17* carries NO flag weight: no campaign flag is flipped, claimed, or
  18  supported by this file;
  19* is separate from the Test G lane by design (separate file, separate
  20  claims, no shared definitions).
  21
  22Everything proved below is a genuine Mathlib-measure statement about the
  23real Gaussian measure `ProbabilityTheory.gaussianReal`; there are no
  24formal-symbol stand-ins, no `sorry`, no new axioms, no `True` shells.
  25
  26## Fixed normalization (declared a priori; nothing below is fitted)
  27
  28The lattice is the `N`-site discretization of the unit circle (spacing
  29`1/N`). For Fourier mode `k ≥ 1` the discrete Hessian eigenvalue of the
  30frozen quadratic energy, in lattice units, is
  31
  32  `λ_N(k) := 4 N² sin²(πk/N)`  (`latticeEigenvalue`),
  33
  34exactly the expression whose quantitative continuum limit
  35`|λ_N(k) − (2πk)²| ≤ ((2πk)⁴/12)/N²` is proved in
  36`SpectralConvergence.discrete_sine_eigenvalue_expansion` (and whose
  37qualitative version lives in `DiscreteLichnerowicz`). The continuum
  38eigenvalue is `(2πk)²` (`continuumEigenvalue`), the `−d²/dx²` eigenvalue
  39of `e^{2πikx}` on the unit-length circle. The Boltzmann weight of the
  40frozen quadratic energy `½ λ x²` is the centered Gaussian of variance
  41
  42  `v_N(k) := λ_N(k)⁻¹`  (`modeVarianceReal`, packaged as `ℝ≥0` in
  43  `modeVariance`),
  44
  45and the actual one-mode measure is `modeMeasure k N := gaussianReal 0
  46(modeVariance k N)`, a real Mathlib measure on `ℝ`. At degenerate
  47resolutions (`N ∣ k`, where `λ_N(k) = 0`) Lean's `0⁻¹ = 0` convention
  48makes `modeMeasure` the Dirac mass at `0`; every quantitative statement
  49below is therefore scoped to `N ≥ 4k`, where `λ_N(k) ≥ (2πk)²/2 > 0`
  50(`latticeEigenvalue_lower_bound`) and the measure is a genuinely
  51non-degenerate Gaussian (`modeVariance_ne_zero`).
  52
  53## What is proved (all THEOREM, axiom-clean)
  54
  551. Moment/characteristic identities for the actual measure, for every
  56   `k N t`:
  57   `integral_exp_modeMeasure`: `∫ exp(t·x) dμ_N = exp(v_N t²/2)`
  58   (moment-generating identity, real integral against `gaussianReal`);
  59   `charFun_modeMeasure`: `charFun μ_N t = exp(−v_N t²/2)`;
  60   `secondMoment_modeMeasure`: `∫ x² dμ_N = v_N`.
  612. Rate: for `k ≥ 1`, `N ≥ 4k`,
  62   `modeVarianceReal_rate`: `|v_N − (2πk)⁻²| ≤ (1/6)/N²`. The constant
  63   is UNIFORM in `k`: the naive `C(k) = 2·((2πk)⁴/12)/(2πk)⁴` from the
  64   Phase-2a expansion collapses to `1/6` because the eventual eigenvalue
  65   lower bound `λ_N ≥ (2πk)²/2` cancels the `(2πk)⁴` growth.
  663. Measure convergence, two honest formulations (the vendored Mathlib
  67   has no Lévy continuity theorem, so weak convergence is NOT claimed):
  68   `secondMoment_tendsto`: `∫ x² dμ_N → (2πk)⁻²`;
  69   `charFun_modeMeasure_tendsto`: `charFun μ_N t → exp(−(2πk)⁻² t²/2)`
  70   pointwise in `t` (the characteristic function of the limiting
  71   Gaussian; the classical Lévy argument would upgrade this to weak
  72   convergence, but that upgrade is not available in Mathlib and is
  73   not claimed here).
  744. Non-vacuity: `limitVariance_pos`: `(2πk)⁻² > 0` for `k ≥ 1`;
  75   `instIsProbabilityMeasureModeMeasure`: `μ_N` is a probability
  76   measure for ALL `k N` (including degenerate ones); and
  77   `modeVariance_ne_zero`: in scope `N ≥ 4k` the Gaussian is
  78   non-degenerate, so nothing below is a statement about a Dirac mass.
  79
  80## Mathlib API surface used
  81
  82`ProbabilityTheory.gaussianReal` (+ its `IsProbabilityMeasure`
  83instance), `mgf_id_gaussianReal`, `charFun_gaussianReal`,
  84`integral_id_gaussianReal`, `variance_fun_id_gaussianReal`,
  85`variance_eq_integral`, all from
  86`Mathlib.Probability.Distributions.Gaussian.Real`; plus the Phase-2a
  87toolkit `discrete_sine_eigenvalue_expansion` /
  88`eigenvalue_limit_of_uniform_bound` from `SpectralConvergence`.
  89-/
  90
  91namespace IndisputableMonolith
  92namespace Gravity
  93namespace Analysis
  94namespace OneModeCylinder
  95
  96open Filter Topology MeasureTheory ProbabilityTheory
  97open scoped NNReal
  98
  99noncomputable section
 100
 101/-- Discrete Hessian eigenvalue of Fourier mode `k` on the `N`-site
 102periodic lattice, in lattice units: `λ_N(k) = 4N² sin²(πk/N)`. This is
 103the exact expression of `discrete_sine_eigenvalue_expansion`. -/
 104def latticeEigenvalue (k N : ℕ) : ℝ :=
 105  4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2
 106
 107/-- Continuum eigenvalue of mode `k`: `(2πk)²`, the `−d²/dx²` eigenvalue
 108of `e^{2πikx}` on the unit circle. -/
 109def continuumEigenvalue (k : ℕ) : ℝ := (2 * Real.pi * (k : ℝ)) ^ 2
 110
 111/-- One-mode Gaussian variance in lattice units: `v_N(k) = λ_N(k)⁻¹`
 112(junk value `0` at degenerate resolutions, by Lean's `0⁻¹ = 0`). -/
 113def modeVarianceReal (k N : ℕ) : ℝ := (latticeEigenvalue k N)⁻¹
 114
 115/-- The variance packaged as `ℝ≥0`, as `gaussianReal` requires. -/
 116def modeVariance (k N : ℕ) : ℝ≥0 := Real.toNNReal (modeVarianceReal k N)
 117
 118/-- The actual one-mode measure: the centered real Gaussian measure of
 119variance `v_N(k)`. A genuine Mathlib measure on `ℝ`, not a symbol. -/
 120def modeMeasure (k N : ℕ) : Measure ℝ := gaussianReal 0 (modeVariance k N)
 121
 122/-- `λ_N(k) ≥ 0` always (it is `4N²` times a square). -/
 123theorem latticeEigenvalue_nonneg (k N : ℕ) : 0 ≤ latticeEigenvalue k N := by
 124  unfold latticeEigenvalue
 125  positivity
 126
 127/-- `v_N(k) ≥ 0` always. -/
 128theorem modeVarianceReal_nonneg (k N : ℕ) : 0 ≤ modeVarianceReal k N :=
 129  inv_nonneg.mpr (latticeEigenvalue_nonneg k N)
 130
 131/-- The `ℝ≥0` packaging is faithful: `(modeVariance k N : ℝ)` is exactly
 132`λ_N(k)⁻¹`. -/
 133theorem coe_modeVariance (k N : ℕ) :
 134    ((modeVariance k N : ℝ≥0) : ℝ) = modeVarianceReal k N :=
 135  Real.coe_toNNReal _ (modeVarianceReal_nonneg k N)
 136
 137/-- NON-VACUITY (target 4): `μ_N` is a probability measure for every
 138`k N`, inherited from Mathlib's `gaussianReal` instance. -/
 139instance instIsProbabilityMeasureModeMeasure (k N : ℕ) :
 140    IsProbabilityMeasure (modeMeasure k N) := by
 141  unfold modeMeasure
 142  infer_instance
 143
 144/-! ## Target 1: moment and characteristic-function identities -/
 145
 146/-- TARGET 1 (moment-generating identity, exactly as briefed): for the
 147actual normalized Gaussian measure `μ_N`,
 148`∫ exp(t·x) dμ_N = exp(v_N t²/2)`. Proved from Mathlib's
 149`mgf_id_gaussianReal` with mean `0`. -/
 150theorem integral_exp_modeMeasure (k N : ℕ) (t : ℝ) :
 151    ∫ x, Real.exp (t * x) ∂(modeMeasure k N)
 152      = Real.exp ((modeVariance k N : ℝ) * t ^ 2 / 2) := by
 153  unfold modeMeasure
 154  have h := congrFun
 155    (mgf_id_gaussianReal (μ := (0 : ℝ)) (v := modeVariance k N)) t
 156  simp only [mgf, id_eq, zero_mul, zero_add] at h
 157  exact h
 158
 159/-- TARGET 1 (characteristic function): `charFun μ_N t = exp(−v_N t²/2)`.
 160Proved from Mathlib's `charFun_gaussianReal` with mean `0`. -/
 161theorem charFun_modeMeasure (k N : ℕ) (t : ℝ) :
 162    charFun (modeMeasure k N) t
 163      = Complex.exp (-(((modeVariance k N : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2)) := by
 164  unfold modeMeasure
 165  rw [charFun_gaussianReal]
 166  congr 1
 167  push_cast
 168  ring
 169
 170/-- TARGET 1 (second moment): `∫ x² dμ_N = v_N`. Proved from Mathlib's
 171`variance_fun_id_gaussianReal` plus the zero-mean identity. -/
 172theorem secondMoment_modeMeasure (k N : ℕ) :
 173    ∫ x, x ^ 2 ∂(modeMeasure k N) = ((modeVariance k N : ℝ≥0) : ℝ) := by
 174  have h := variance_fun_id_gaussianReal (μ := (0 : ℝ)) (v := modeVariance k N)
 175  rw [variance_eq_integral measurable_id'.aemeasurable] at h
 176  simp only [integral_id_gaussianReal, sub_zero] at h
 177  unfold modeMeasure
 178  exact h
 179
 180/-! ## Target 2: quantitative variance limit with an explicit rate -/
 181
 182/-- Eventual eigenvalue lower bound: for `k ≥ 1` and `N ≥ 4k`,
 183`λ_N(k) ≥ (2πk)²/2`. Derived from the Phase-2a expansion: the error
 184`((2πk)⁴/12)/N²` is at most `(2πk)²/2` once `(2πk)² ≤ 6N²`, which
 185`π ≤ 4` and `N ≥ 4k` guarantee. This is what keeps `λ_N(k)⁻¹`
 186controlled in the rate bound. -/
 187theorem latticeEigenvalue_lower_bound (k N : ℕ) (hk : 1 ≤ k)
 188    (hN : 4 * k ≤ N) :
 189    continuumEigenvalue k / 2 ≤ latticeEigenvalue k N := by
 190  have hN1 : 1 ≤ N := by omega
 191  have hexp := discrete_sine_eigenvalue_expansion k N hN1
 192  have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
 193  have hNR : (4 : ℝ) * (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
 194  have hNpos : (0 : ℝ) < (N : ℝ) := by linarith
 195  have hpi2 : Real.pi * Real.pi ≤ 16 := by
 196    nlinarith [Real.pi_le_four, Real.pi_pos]
 197  have hN2 : 16 * (k : ℝ) ^ 2 ≤ (N : ℝ) ^ 2 := by nlinarith [hkR, hNR]
 198  have h1 : (2 * Real.pi * (k : ℝ)) ^ 2 ≤ 6 * (N : ℝ) ^ 2 := by
 199    nlinarith [hpi2, hN2, sq_nonneg (k : ℝ),
 200      mul_nonneg (by linarith : (0 : ℝ) ≤ 16 - Real.pi * Real.pi)
 201        (sq_nonneg (k : ℝ))]
 202  have h12 : (0 : ℝ) < 12 * (N : ℝ) ^ 2 := by positivity
 203  have hkey : (2 * Real.pi * (k : ℝ)) ^ 4 / 12 / (N : ℝ) ^ 2
 204      ≤ (2 * Real.pi * (k : ℝ)) ^ 2 / 2 := by
 205    rw [div_div, div_le_iff₀ h12]
 206    nlinarith [h1, sq_nonneg (2 * Real.pi * (k : ℝ))]
 207  have habs := abs_le.mp hexp
 208  unfold continuumEigenvalue latticeEigenvalue
 209  linarith [habs.1, hkey]
 210
 211/-- In scope (`k ≥ 1`, `N ≥ 4k`) the eigenvalue is strictly positive. -/
 212theorem latticeEigenvalue_pos (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
 213    0 < latticeEigenvalue k N := by
 214  have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
 215  have hLam : 0 < continuumEigenvalue k := by
 216    unfold continuumEigenvalue
 217    have : 0 < 2 * Real.pi * (k : ℝ) := by
 218      have := Real.pi_pos
 219      nlinarith
 220    positivity
 221  linarith [latticeEigenvalue_lower_bound k N hk hN]
 222
 223/-- In scope the variance is strictly positive: the Gaussian is
 224non-degenerate. -/
 225theorem modeVarianceReal_pos (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
 226    0 < modeVarianceReal k N :=
 227  inv_pos.mpr (latticeEigenvalue_pos k N hk hN)
 228
 229/-- NON-VACUITY (target 4): in scope `μ_N` is a genuinely non-degenerate
 230Gaussian (not the Dirac mass): its `ℝ≥0` variance parameter is
 231nonzero. -/
 232theorem modeVariance_ne_zero (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
 233    modeVariance k N ≠ 0 := by
 234  have hpos := modeVarianceReal_pos k N hk hN
 235  simp only [modeVariance, ne_eq, Real.toNNReal_eq_zero, not_le]
 236  exact hpos
 237
 238/-- TARGET 2 (rate): for `k ≥ 1` and `N ≥ 4k`,
 239`|v_N(k) − (2πk)⁻²| ≤ (1/6)/N²`. The constant `C(k) = 1/6` is uniform
 240in `k`: `|λ⁻¹ − Λ⁻¹| = |Λ − λ|/(λΛ) ≤ (Λ²/12/N²)/(Λ²/2) = (1/6)/N²`
 241with `Λ = (2πk)²`, using the Phase-2a expansion for the numerator and
 242`latticeEigenvalue_lower_bound` for the denominator. -/
 243theorem modeVarianceReal_rate (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
 244    |modeVarianceReal k N - (continuumEigenvalue k)⁻¹|
 245      ≤ 1 / 6 / (N : ℝ) ^ 2 := by
 246  have hN1 : 1 ≤ N := by omega
 247  have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
 248  have hNR : (4 : ℝ) * (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
 249  have hNpos : (0 : ℝ) < (N : ℝ) := by linarith
 250  have hLam_pos : 0 < continuumEigenvalue k := by
 251    unfold continuumEigenvalue
 252    have : 0 < 2 * Real.pi * (k : ℝ) := by
 253      have := Real.pi_pos
 254      nlinarith
 255    positivity
 256  have hlow := latticeEigenvalue_lower_bound k N hk hN
 257  have hlam_pos : 0 < latticeEigenvalue k N := latticeEigenvalue_pos k N hk hN
 258  -- Numerator: the Phase-2a expansion, with `(2πk)⁴ = Λ²`.
 259  have hnum : |continuumEigenvalue k - latticeEigenvalue k N|
 260      ≤ (continuumEigenvalue k) ^ 2 / 12 / (N : ℝ) ^ 2 := by
 261    rw [abs_sub_comm]
 262    have h4 : (continuumEigenvalue k) ^ 2 = (2 * Real.pi * (k : ℝ)) ^ 4 := by
 263      unfold continuumEigenvalue
 264      ring
 265    rw [h4]
 266    exact discrete_sine_eigenvalue_expansion k N hN1
 267  -- Denominator: `λΛ ≥ Λ²/2`.
 268  have hden : (continuumEigenvalue k) ^ 2 / 2
 269      ≤ latticeEigenvalue k N * continuumEigenvalue k := by
 270    have := mul_le_mul_of_nonneg_right hlow hLam_pos.le
 271    nlinarith [this]
 272  have hinv : (latticeEigenvalue k N)⁻¹ - (continuumEigenvalue k)⁻¹
 273      = (continuumEigenvalue k - latticeEigenvalue k N)
 274        / (latticeEigenvalue k N * continuumEigenvalue k) :=
 275    inv_sub_inv hlam_pos.ne' hLam_pos.ne'
 276  unfold modeVarianceReal
 277  rw [hinv, abs_div, abs_of_pos (mul_pos hlam_pos hLam_pos)]
 278  calc |continuumEigenvalue k - latticeEigenvalue k N|
 279        / (latticeEigenvalue k N * continuumEigenvalue k)
 280      ≤ ((continuumEigenvalue k) ^ 2 / 12 / (N : ℝ) ^ 2)
 281        / ((continuumEigenvalue k) ^ 2 / 2) :=
 282        div_le_div₀ (by positivity) hnum (by positivity) hden
 283    _ = 1 / 6 / (N : ℝ) ^ 2 := by
 284        field_simp
 285        ring
 286
 287/-! ## Target 3: measure convergence (two honest formulations) -/
 288
 289/-- The variances converge with the `(1/6)/N²` rate: `v_N(k) → (2πk)⁻²`.
 290Composes the rate with the Phase-2a squeeze
 291`eigenvalue_limit_of_uniform_bound`. -/
 292theorem modeVarianceReal_tendsto (k : ℕ) (hk : 1 ≤ k) :
 293    Filter.Tendsto (fun N : ℕ => modeVarianceReal k N) Filter.atTop
 294      (nhds ((continuumEigenvalue k)⁻¹)) :=
 295  eigenvalue_limit_of_uniform_bound _ _ (1 / 6) (4 * k)
 296    (fun N hN => modeVarianceReal_rate k N hk hN)
 297
 298/-- TARGET 3 (second moments converge): the actual Gaussian integrals
 299`∫ x² dμ_N` converge to the continuum mode variance `(2πk)⁻²`. -/
 300theorem secondMoment_tendsto (k : ℕ) (hk : 1 ≤ k) :
 301    Filter.Tendsto (fun N : ℕ => ∫ x, x ^ 2 ∂(modeMeasure k N))
 302      Filter.atTop (nhds ((continuumEigenvalue k)⁻¹)) := by
 303  refine Filter.Tendsto.congr (fun N => ?_) (modeVarianceReal_tendsto k hk)
 304  rw [secondMoment_modeMeasure, coe_modeVariance]
 305
 306/-- TARGET 3 (characteristic functions converge pointwise): for every
 307`t`, `charFun μ_N t → exp(−(2πk)⁻² t²/2)`, the characteristic function
 308of the centered Gaussian of variance `(2πk)⁻²`. This is the strongest
 309convergence statement the vendored Mathlib supports without new axioms
 310(no Lévy continuity theorem is available, so the classical upgrade to
 311weak convergence is NOT claimed here). -/
 312theorem charFun_modeMeasure_tendsto (k : ℕ) (hk : 1 ≤ k) (t : ℝ) :
 313    Filter.Tendsto (fun N : ℕ => charFun (modeMeasure k N) t)
 314      Filter.atTop
 315      (nhds (Complex.exp
 316        (-((((continuumEigenvalue k)⁻¹ : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2)))) := by
 317  have h0 : Filter.Tendsto
 318      (fun N : ℕ => ((modeVarianceReal k N : ℝ) : ℂ)) Filter.atTop
 319      (nhds ((((continuumEigenvalue k)⁻¹ : ℝ) : ℂ))) :=
 320    (Complex.continuous_ofReal.tendsto _).comp (modeVarianceReal_tendsto k hk)
 321  have h1 : Filter.Tendsto
 322      (fun N : ℕ => -(((modeVarianceReal k N : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2))
 323      Filter.atTop
 324      (nhds (-((((continuumEigenvalue k)⁻¹ : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2))) :=
 325    ((h0.mul_const ((t : ℂ) ^ 2)).div_const (2 : ℂ)).neg
 326  refine Filter.Tendsto.congr (fun N => ?_) h1.cexp
 327  rw [charFun_modeMeasure k N t, coe_modeVariance]
 328
 329/-! ## Target 4: non-vacuity of the limit -/
 330
 331/-- TARGET 4 (J ≠ 0): the limiting variance `(2πk)⁻²` is strictly
 332positive for every mode `k ≥ 1`: the limit object is a non-degenerate
 333Gaussian, not a point mass. -/
 334theorem limitVariance_pos (k : ℕ) (hk : 1 ≤ k) :
 335    0 < (continuumEigenvalue k)⁻¹ := by
 336  have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
 337  have : 0 < continuumEigenvalue k := by
 338    unfold continuumEigenvalue
 339    have : 0 < 2 * Real.pi * (k : ℝ) := by
 340      have := Real.pi_pos
 341      nlinarith
 342    positivity
 343  exact inv_pos.mpr this
 344
 345end
 346
 347end OneModeCylinder
 348end Analysis
 349end Gravity
 350end IndisputableMonolith
 351