Gravity Analysis One Mode Cylinder Preflight Lattice Eigenvalue Lower Bound

The eigenvalue bound

The declaration latticeEigenvalue_lower_bound is a theorem in the framework's machine-checked library of formal theorems. It concerns a standard object from numerical analysis: the discrete approximation to the second derivative operator on a circle. When you replace a continuous circle by N equally spaced points, the second derivative becomes a matrix, and its eigenvalues are 4N² sin²(πk/N) for integer mode numbers k. The theorem states that when N is at least four times k, this discrete eigenvalue is at least half the corresponding continuous eigenvalue (2πk)². In plain terms, the discrete approximation cannot collapse toward zero; it stays bounded below by a positive multiple of the true value.

The bound matters because it prevents a technical failure. The framework is testing a candidate measure for a single Fourier mode on a lattice, and the variance of that measure is the reciprocal of the eigenvalue. If the eigenvalue could approach zero, the variance would blow up and the Gaussian measure would become ill-defined. The theorem rules that out, for every mode k and every lattice size N satisfying 4k ≤ N. It is a genuine statement about the real Gaussian measure, proved without gaps, new axioms, or placeholder symbols.

The theorem has sharp limits. It says nothing about the full path-sum measure, which the module explicitly does not construct. It carries no weight for any campaign claim, being a toy preflight for a single mode. It also excludes the degenerate case where N divides k, where the eigenvalue is exactly zero and the measure degenerates to a Dirac mass. All quantitative statements, including the variance convergence rate of order 1/N², are scoped to the non-degenerate regime N ≥ 4k. The lower bound is the load-bearing ingredient that makes the variance well-defined and the convergence statements meaningful.

What the bound enables is a clean convergence result: as N grows, the variance of the discrete Gaussian tends to the continuous value (2πk)⁻², and the characteristic function tends to that of the limiting Gaussian. The classical Lévy continuity theorem would upgrade this to weak convergence of measures, but that upgrade is not available in the library and is not claimed. The lower bound itself is the quiet foundation that lets the rest of the module stand.

/-- Eventual eigenvalue lower bound: for `k ≥ 1` and `N ≥ 4k`,
`λ_N(k) ≥ (2πk)²/2`. Derived from the Phase-2a expansion: the error
`((2πk)⁴/12)/N²` is at most `(2πk)²/2` once `(2πk)² ≤ 6N²`, which
`π ≤ 4` and `N ≥ 4k` guarantee. This is what keeps `λ_N(k)⁻¹`
controlled in the rate bound. -/
theorem latticeEigenvalue_lower_bound (k N : ℕ) (hk : 1 ≤ k)
    (hN : 4 * k ≤ N) :
    continuumEigenvalue k / 2 ≤ latticeEigenvalue k N := by
  have hN1 : 1 ≤ N := by omega
  have hexp := discrete_sine_eigenvalue_expansion k N hN1
  have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
  have hNR : (4 : ℝ) * (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
  have hNpos : (0 : ℝ) < (N : ℝ) := by linarith
  have hpi2 : Real.pi * Real.pi ≤ 16 := by
    nlinarith [Real.pi_le_four, Real.pi_pos]
  have hN2 : 16 * (k : ℝ) ^ 2 ≤ (N : ℝ) ^ 2 := by nlinarith [hkR, hNR]
  have h1 : (2 * Real.pi * (k : ℝ)) ^ 2 ≤ 6 * (N : ℝ) ^ 2 := by
    nlinarith [hpi2, hN2, sq_nonneg (k : ℝ),
      mul_nonneg (by linarith : (0 : ℝ) ≤ 16 - Real.pi * Real.pi)
        (sq_nonneg (k : ℝ))]
  have h12 : (0 : ℝ) < 12 * (N : ℝ) ^ 2 := by positivity
  have hkey : (2 * Real.pi * (k : ℝ)) ^ 4 / 12 / (N : ℝ) ^ 2
      ≤ (2 * Real.pi * (k : ℝ)) ^ 2 / 2 := by
    rw [div_div, div_le_iff₀ h12]
    nlinarith [h1, sq_nonneg (2 * Real.pi * (k : ℝ))]
  have habs := abs_le.mp hexp
  unfold continuumEigenvalue latticeEigenvalue
  linarith [habs.1, hkey]

/-- One-mode Gaussian variance in lattice units: `v_N(k) = λ_N(k)⁻¹`
(junk value `0` at degenerate resolutions, by Lean's `0⁻¹ = 0`). -/
def modeVarianceReal (k N : ℕ) : ℝ := (latticeEigenvalue k N)⁻¹

/-- NON-VACUITY (target 4): in scope `μ_N` is a genuinely non-degenerate
Gaussian (not the Dirac mass): its `ℝ≥0` variance parameter is
nonzero. -/
theorem modeVariance_ne_zero (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
    modeVariance k N ≠ 0 := by
  have hpos := modeVarianceReal_pos k N hk hN
  simp only [modeVariance, ne_eq, Real.toNNReal_eq_zero, not_le]
  exact hpos

What this page does not claim

The theorem does not construct or validate any field-theoretic path-sum measure; it concerns only one Fourier mode on a one-dimensional lattice. The theorem does not apply when N divides k, where the eigenvalue vanishes and the Gaussian degenerates. The theorem does not establish weak convergence of measures, only pointwise convergence of characteristic functions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: