Gravity Analysis One Mode Cylinder Preflight Char Fun Mode Measure Tendsto

The one-mode limit

A Fourier mode is a pure sine or cosine wave of a fixed frequency, and on a circle of circumference one the smooth mode with integer frequency k has eigenvalue (2πk)² for the operator −d²/dx². The Recognition Science library discretizes this circle into N evenly spaced points and defines a discrete eigenvalue λ_N(k) = 4N² sin²(πk/N), which approximates the continuum value. The library then builds a Gaussian probability measure on the real line for this single mode, with variance equal to the reciprocal of the discrete eigenvalue. This is a toy model: it concerns exactly one Fourier mode on a one-dimensional lattice, not a full field theory.

The characteristic function of a probability measure is its Fourier transform, a complex-valued function that completely determines the measure. For the one-mode Gaussian measure, the library proves the exact identity charFun_modeMeasure: the characteristic function at argument t equals exp(−v_N t²/2), where v_N is the discrete variance. The central theorem charFun_modeMeasure_tendsto states that as the lattice resolution N grows, this characteristic function converges pointwise in t to exp(−(2πk)⁻² t²/2), which is precisely the characteristic function of the Gaussian with the continuum variance (2πk)⁻². This is a genuine statement about real probability measures, proved with no gaps and no extra axioms.

In Recognition Science, this result is a preflight check for a proposed construction called C10, a Gaussian cylinder-measure limit over a frozen quadratic energy. The library explicitly labels this file as a one-mode toy preflight, separate from the path-sum measure and carrying no campaign flag. The convergence of characteristic functions is the classical Lévy continuity theorem's hypothesis: if the characteristic functions of a sequence of measures converge pointwise to a continuous function, then the measures converge weakly. However, the vendored Mathlib library does not contain the Lévy continuity theorem, so the weak convergence upgrade is not claimed. The library proves the variance itself converges at rate |v_N − (2πk)⁻²| ≤ (1/6)/N², uniformly in k, which is a stronger quantitative statement than mere convergence.

The theorem's scope is carefully delimited. It holds for k ≥ 1 and N ≥ 4k, where the discrete eigenvalue is bounded below by half the continuum eigenvalue and the Gaussian is non-degenerate. At degenerate resolutions where N divides k, the discrete eigenvalue vanishes and the measure collapses to a Dirac mass at zero; those cases are excluded from the quantitative statements. The library also proves the second moment converges to the continuum variance, and that the limit variance is strictly positive for all k ≥ 1, so the limiting object is a genuine non-degenerate Gaussian, not a trivial point mass.

What this theorem changes for a reader is the confidence that a specific discretization scheme for a single Fourier mode reproduces the continuum Gaussian structure with a uniform error bound. It is a building block, not a destination: it validates one technical step in a larger program, while explicitly leaving the full measure construction, the path-sum measure, and any physical interpretation of gravity as open targets.

/-- TARGET 3 (characteristic functions converge pointwise): for every
`t`, `charFun μ_N t → exp(−(2πk)⁻² t²/2)`, the characteristic function
of the centered Gaussian of variance `(2πk)⁻²`. This is the strongest
convergence statement the vendored Mathlib supports without new axioms
(no Lévy continuity theorem is available, so the classical upgrade to
weak convergence is NOT claimed here). -/
theorem charFun_modeMeasure_tendsto (k : ℕ) (hk : 1 ≤ k) (t : ℝ) :
    Filter.Tendsto (fun N : ℕ => charFun (modeMeasure k N) t)
      Filter.atTop
      (nhds (Complex.exp
        (-((((continuumEigenvalue k)⁻¹ : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2)))) := by
  have h0 : Filter.Tendsto
      (fun N : ℕ => ((modeVarianceReal k N : ℝ) : ℂ)) Filter.atTop
      (nhds ((((continuumEigenvalue k)⁻¹ : ℝ) : ℂ))) :=
    (Complex.continuous_ofReal.tendsto _).comp (modeVarianceReal_tendsto k hk)
  have h1 : Filter.Tendsto
      (fun N : ℕ => -(((modeVarianceReal k N : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2))
      Filter.atTop
      (nhds (-((((continuumEigenvalue k)⁻¹ : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2))) :=
    ((h0.mul_const ((t : ℂ) ^ 2)).div_const (2 : ℂ)).neg
  refine Filter.Tendsto.congr (fun N => ?_) h1.cexp
  rw [charFun_modeMeasure k N t, coe_modeVariance]

/-- TARGET 2 (rate): for `k ≥ 1` and `N ≥ 4k`,
`|v_N(k) − (2πk)⁻²| ≤ (1/6)/N²`. The constant `C(k) = 1/6` is uniform
in `k`: `|λ⁻¹ − Λ⁻¹| = |Λ − λ|/(λΛ) ≤ (Λ²/12/N²)/(Λ²/2) = (1/6)/N²`
with `Λ = (2πk)²`, using the Phase-2a expansion for the numerator and
`latticeEigenvalue_lower_bound` for the denominator. -/
theorem modeVarianceReal_rate (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
    |modeVarianceReal k N - (continuumEigenvalue k)⁻¹|
      ≤ 1 / 6 / (N : ℝ) ^ 2 := by
  have hN1 : 1 ≤ N := by omega
  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 hLam_pos : 0 < continuumEigenvalue k := by
    unfold continuumEigenvalue
    have : 0 < 2 * Real.pi * (k : ℝ) := by
      have := Real.pi_pos
      nlinarith
    positivity
  have hlow := latticeEigenvalue_lower_bound k N hk hN
  have hlam_pos : 0 < latticeEigenvalue k N := latticeEigenvalue_pos k N hk hN
  -- Numerator: the Phase-2a expansion, with `(2πk)⁴ = Λ²`.
  have hnum : |continuumEigenvalue k - latticeEigenvalue k N|
      ≤ (continuumEigenvalue k) ^ 2 / 12 / (N : ℝ) ^ 2 := by
    rw [abs_sub_comm]
    have h4 : (continuumEigenvalue k) ^ 2 = (2 * Real.pi * (k : ℝ)) ^ 4 := by
      unfold continuumEigenvalue
      ring
    rw [h4]
    exact discrete_sine_eigenvalue_expansion k N hN1
  -- Denominator: `λΛ ≥ Λ²/2`.
  have hden : (continuumEigenvalue k) ^ 2 / 2
      ≤ latticeEigenvalue k N * continuumEigenvalue k := by
    have := mul_le_mul_of_nonneg_right hlow hLam_pos.le
    nlinarith [this]
  have hinv : (latticeEigenvalue k N)⁻¹ - (continuumEigenvalue k)⁻¹
      = (continuumEigenvalue k - latticeEigenvalue k N)
        / (latticeEigenvalue k N * continuumEigenvalue k) :=
    inv_sub_inv hlam_pos.ne' hLam_pos.ne'
  unfold modeVarianceReal
  rw [hinv, abs_div, abs_of_pos (mul_pos hlam_pos hLam_pos)]
  calc |continuumEigenvalue k - latticeEigenvalue k N|
        / (latticeEigenvalue k N * continuumEigenvalue k)
      ≤ ((continuumEigenvalue k) ^ 2 / 12 / (N : ℝ) ^ 2)
        / ((continuumEigenvalue k) ^ 2 / 2) :=
        div_le_div₀ (by positivity) hnum (by positivity) hden
    _ = 1 / 6 / (N : ℝ) ^ 2 := by
        field_simp
        ring

/-- 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 a field-theoretic measure or any path-sum measure. The theorem does not claim weak convergence of the measures, only pointwise convergence of characteristic functions. The theorem does not apply at degenerate resolutions where N divides k.

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: