Gravity Analysis One Mode Cylinder Preflight Second Moment Mode Measure

The second moment

The second moment of a probability distribution is the average of the squared value of the random variable. For a vibration mode with amplitude x, the second moment measures the typical energy carried by that mode. The declaration secondMoment_modeMeasure proves, in the framework's machine-checked library of formal theorems, that for a single Fourier mode on a discretized circle, this average equals the variance of the Gaussian measure that describes the mode's fluctuations.

Classically, a vibrating string or circle can be decomposed into modes, each with a characteristic spatial frequency k. On a continuous circle of unit length, the mode with frequency k has an eigenvalue of (2πk)² for the operator −d²/dx². When the circle is replaced by a lattice of N equally spaced points, this eigenvalue changes to 4N² sin²(πk/N). The framework's declaration establishes that the second moment of the mode's amplitude distribution is exactly the reciprocal of this discrete eigenvalue, and that this reciprocal converges to the continuous value (2πk)⁻² as N grows.

The rate of convergence is also proved. For any mode with k ≥ 1 and any lattice with N ≥ 4k, the difference between the discrete second moment and its continuous limit is at most 1/(6N²). This uniform bound, independent of k, follows from a lower bound on the discrete eigenvalue that cancels the naive growth with k. The declaration secondMoment_tendsto then shows that the second moment itself tends to (2πk)⁻² as N goes to infinity.

What this does not claim is equally important. The declaration concerns a single mode on a one-dimensional lattice; it does not construct a measure for a full field theory. It does not claim weak convergence of the measures, only convergence of the second moment and of the characteristic function pointwise in t. The classical Lévy continuity theorem would upgrade the characteristic function convergence to weak convergence, but that theorem is not available in the library and is not claimed. The declaration also carries no weight for any campaign flag; it is a standalone preflight check of a toy model.

In the framework's account, this result provides a quantitative bridge between the discrete lattice description and the continuous limit for a single mode. The uniform error bound means that the approximation degrades gracefully as the mode number grows, which is a useful property for any eventual multi-mode construction. The proof is axiom-clean, using only the standard real Gaussian measure from the library, with no new axioms and no formal-symbol stand-ins.

/-- TARGET 1 (second moment): `∫ x² dμ_N = v_N`. Proved from Mathlib's
`variance_fun_id_gaussianReal` plus the zero-mean identity. -/
theorem secondMoment_modeMeasure (k N : ℕ) :
    ∫ x, x ^ 2 ∂(modeMeasure k N) = ((modeVariance k N : ℝ≥0) : ℝ) := by
  have h := variance_fun_id_gaussianReal (μ := (0 : ℝ)) (v := modeVariance k N)
  rw [variance_eq_integral measurable_id'.aemeasurable] at h
  simp only [integral_id_gaussianReal, sub_zero] at h
  unfold modeMeasure
  exact h

/-- 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

/-- TARGET 3 (second moments converge): the actual Gaussian integrals
`∫ x² dμ_N` converge to the continuum mode variance `(2πk)⁻²`. -/
theorem secondMoment_tendsto (k : ℕ) (hk : 1 ≤ k) :
    Filter.Tendsto (fun N : ℕ => ∫ x, x ^ 2 ∂(modeMeasure k N))
      Filter.atTop (nhds ((continuumEigenvalue k)⁻¹)) := by
  refine Filter.Tendsto.congr (fun N => ?_) (modeVarianceReal_tendsto k hk)
  rw [secondMoment_modeMeasure, coe_modeVariance]

What this page does not claim

The declaration does not construct a measure for a full field theory; it concerns only a single Fourier mode on a one-dimensional lattice. The declaration does not claim weak convergence of the measures, only convergence of the second moment and characteristic function pointwise. The declaration carries no weight for any campaign flag; it is a standalone preflight check of a toy model.

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: