Encyclopedia Gravity Gravity Analysis One Mode Cylinder Preflight Mode Variance Real Tendsto
ARTICLE 4 claims 4 theorems
Gravity Analysis One Mode Cylinder Preflight Mode Variance Real Tendsto
A single Fourier mode on a circle has a variance that approaches a known continuum value as the lattice gets finer, a fact proved for one toy case and nothing more.
The mode variance limit
In classical Fourier analysis, a function on a circle can be decomposed into modes e^{2πikx}, and the operator −d²/dx² acts on each mode by multiplying it by the eigenvalue (2πk)². When one discretizes the circle into N equally spaced points, this eigenvalue is approximated by the discrete expression λ_N(k) = 4N² sin²(πk/N), which converges to the continuum value as N grows. The framework's declaration modeVarianceReal_tendsto (a machine-checked theorem in its library of formal mathematics) proves that the reciprocal of this discrete eigenvalue, the variance v_N(k) = 1/λ_N(k), converges to the reciprocal continuum eigenvalue 1/(2πk)² as N tends to infinity. The proof uses a uniform rate bound |v_N(k) − (2πk)⁻²| ≤ (1/6)/N², valid for all k ≥ 1 once N ≥ 4k, which is a stronger statement than mere convergence: it gives a quantitative speed.
The result is one component of a larger preflight check for a proposed Gaussian cylinder measure, a candidate construction in the framework's gravity program. The preflight is deliberately minimal: it concerns a single Fourier mode on a one-dimensional periodic lattice, not a full field-theoretic measure. The declaration itself is a statement about real numbers and limits, and it is proved without any new axioms or unproven assumptions. The convergence is pointwise in the mode index k; the uniform constant 1/6 does not depend on k, which is the technical reason the proof succeeds. The limiting variance 1/(2πk)² is positive for every k ≥ 1, so the limit is a genuine non-degenerate Gaussian, not a delta function.
What the declaration does not claim is as important as what it proves. It does not construct a path-sum measure, does not flip any campaign flag, and does not establish weak convergence of probability measures. The latter would require a Lévy continuity theorem, which the underlying library does not provide; the preflight instead proves convergence of characteristic functions pointwise in t, a weaker statement. The result is scoped to N ≥ 4k, where the discrete eigenvalue is positive; at degenerate resolutions where N divides k, the variance is zero and the measure collapses to a Dirac mass. Within the framework, this is a stepping stone: it shows that a single-mode toy model has the correct continuum limit, which is a necessary but not sufficient condition for the full cylinder measure to exist.
THEOREM modeVarianceReal_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- The variances converge with the `(1/6)/N²` rate: `v_N(k) → (2πk)⁻²`.
Composes the rate with the Phase-2a squeeze
`eigenvalue_limit_of_uniform_bound`. -/
theorem modeVarianceReal_tendsto (k : ℕ) (hk : 1 ≤ k) :
Filter.Tendsto (fun N : ℕ => modeVarianceReal k N) Filter.atTop
(nhds ((continuumEigenvalue k)⁻¹)) :=
eigenvalue_limit_of_uniform_bound _ _ (1 / 6) (4 * k)
(fun N hN => modeVarianceReal_rate k N hk hN)
THEOREM modeVarianceReal_rate · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- 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
THEOREM limitVariance_pos · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- TARGET 4 (J ≠ 0): the limiting variance `(2πk)⁻²` is strictly
positive for every mode `k ≥ 1`: the limit object is a non-degenerate
Gaussian, not a point mass. -/
theorem limitVariance_pos (k : ℕ) (hk : 1 ≤ k) :
0 < (continuumEigenvalue k)⁻¹ := by
have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
have : 0 < continuumEigenvalue k := by
unfold continuumEigenvalue
have : 0 < 2 * Real.pi * (k : ℝ) := by
have := Real.pi_pos
nlinarith
positivity
exact inv_pos.mpr this
THEOREM charFun_modeMeasure_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- 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]
What this page does not claim
The declaration does not construct any field-theoretic measure. The declaration does not claim weak convergence of probability measures. The declaration does not apply to 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:
- How does the single-mode variance limit extend to a full cylinder measure over all modes?
- What is the role of the uniform rate bound in proving convergence of the full measure?
- Does the framework's gravity program require weak convergence, and if so, how would it be obtained?
- What distinguishes this preflight from the path-sum measure it is not?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM modeVarianceReal_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- The variances converge with the `(1/6)/N²` rate: `v_N(k) → (2πk)⁻²`. Composes the rate with the Phase-2a squeeze `eigenvalue_limit_of_uniform_bound`. -/ theorem modeVarianceReal_tendsto (k : ℕ) (hk : 1 ≤ k) : Filter.Tendsto (fun N : ℕ => modeVarianceReal k N) Filter.atTop (nhds ((continuumEigenvalue k)⁻¹)) := eigenvalue_limit_of_uniform_bound _ _ (1 / 6) (4 * k) (fun N hN => modeVarianceReal_rate k N hk hN)the framework's declaration modeVarianceReal_tendsto proves that the reciprocal of this discrete eigenvalue, the variance v_N(k) = 1/λ_N(k), converges to the reciprocal continuum eigenvalue 1/(2πk)² as N tends to infinity modeVarianceReal_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.leanTHEOREM modeVarianceReal_rate · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- 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 ringThe proof uses a uniform rate bound |v_N(k) − (2πk)⁻²| ≤ (1/6)/N², valid for all k ≥ 1 once N ≥ 4k modeVarianceReal_rate · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.leanTHEOREM limitVariance_pos · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- TARGET 4 (J ≠ 0): the limiting variance `(2πk)⁻²` is strictly positive for every mode `k ≥ 1`: the limit object is a non-degenerate Gaussian, not a point mass. -/ theorem limitVariance_pos (k : ℕ) (hk : 1 ≤ k) : 0 < (continuumEigenvalue k)⁻¹ := by have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk have : 0 < continuumEigenvalue k := by unfold continuumEigenvalue have : 0 < 2 * Real.pi * (k : ℝ) := by have := Real.pi_pos nlinarith positivity exact inv_pos.mpr thisThe limiting variance 1/(2πk)² is positive for every k ≥ 1, so the limit is a genuine non-degenerate Gaussian, not a delta function limitVariance_pos · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.leanTHEOREM charFun_modeMeasure_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
/-- 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]It does not establish weak convergence of probability measures charFun_modeMeasure_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean