Gravity Analysis One Mode Cylinder Preflight Integral Exp Mode Measure

A single-mode Gaussian

A Gaussian measure on the real line is the familiar bell-shaped distribution, centered at zero and spread by a variance. The declaration integral_exp_modeMeasure proves the exact moment-generating identity for one such measure: the integral of exp(t·x) against the measure equals exp(v·t²/2), where v is the variance. This is a standard fact of probability theory, and the proof is a genuine theorem about the real Gaussian measure, not a formal stand-in.

The measure in question arises from a single Fourier mode k on a one-dimensional periodic lattice with N sites. The variance v is the reciprocal of the discrete Hessian eigenvalue λ_N(k) = 4N² sin²(πk/N), the exact expression whose continuum limit is (2πk)². The declaration is scoped to non-degenerate resolutions, N ≥ 4k, where the eigenvalue is positive and the Gaussian is genuinely spread out; at degenerate resolutions the measure collapses to a Dirac mass at zero, and the identity still holds but describes a point mass.

The single identity is one member of a small family of proved statements about this measure. The characteristic function is exp(−v·t²/2), the second moment is v, and as N grows the variance converges to (2πk)⁻² at a rate bounded by 1/(6N²), uniformly in k. The characteristic functions converge pointwise to the limiting Gaussian's, though the framework does not claim weak convergence of measures, as the underlying library lacks the classical Lévy continuity theorem.

In Recognition Science, this result is a one-mode toy preflight for a proposed Gaussian cylinder-measure limit over a frozen quadratic energy. It is not the path-sum measure and does not construct any field-theoretic measure. It carries no campaign flag weight and is separate from the Test G lane. The identity is a clean, self-contained probability statement, offered as a checked building block, not as a physical claim about gravity.

The practical consequence is that the framework now has a verified, exact formula for the exponential integral of a single-mode Gaussian, with a uniform convergence rate to the continuum limit. This is the kind of small, precise result that a larger construction can safely rest on. What it does not do is reach beyond the single mode: there is no measure on fields, no path integral, and no physical interpretation of the Gaussian as a gravitational fluctuation.

/-- TARGET 1 (moment-generating identity, exactly as briefed): for the
actual normalized Gaussian measure `μ_N`,
`∫ exp(t·x) dμ_N = exp(v_N t²/2)`. Proved from Mathlib's
`mgf_id_gaussianReal` with mean `0`. -/
theorem integral_exp_modeMeasure (k N : ℕ) (t : ℝ) :
    ∫ x, Real.exp (t * x) ∂(modeMeasure k N)
      = Real.exp ((modeVariance k N : ℝ) * t ^ 2 / 2) := by
  unfold modeMeasure
  have h := congrFun
    (mgf_id_gaussianReal (μ := (0 : ℝ)) (v := modeVariance k N)) t
  simp only [mgf, id_eq, zero_mul, zero_add] at h
  exact h

/-- 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)⁻¹

/-- TARGET 1 (characteristic function): `charFun μ_N t = exp(−v_N t²/2)`.
Proved from Mathlib's `charFun_gaussianReal` with mean `0`. -/
theorem charFun_modeMeasure (k N : ℕ) (t : ℝ) :
    charFun (modeMeasure k N) t
      = Complex.exp (-(((modeVariance k N : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2)) := by
  unfold modeMeasure
  rw [charFun_gaussianReal]
  congr 1
  push_cast
  ring

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

What this page does not claim

This is not a field-theoretic measure and does not construct any path-sum measure. The framework does not claim weak convergence of measures, only pointwise convergence of characteristic functions. The declaration carries no campaign flag weight and is separate from the Test G lane.

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: