module module moderate

`IndisputableMonolith.Gravity.Analysis.OneModeCylinderPreflight`

Preflight definitions for a single Fourier mode on a periodic lattice cylinder: discrete and continuum Hessian eigenvalues, the associated Gaussian mode measure, and its first Fourier and second-moment identities. Analysts working the QG spectral-convergence campaign cite it before taking N→∞ limits. The file is mostly definitional setup plus short nonnegativity and measure lemmas, not a deep existence proof.

claimOn the $N$-site periodic lattice, the discrete Hessian eigenvalue of Fourier mode $k$ is $\lambda_N(k)=4N^2\sin^2(\pi k/N)$. The continuum counterpart, the real mode variance, the complex mode variance, and the Gaussian probability measure $\mu_k$ with density proportional to $e^{-\lambda|z|^2/2}$ are introduced, together with nonnegativity, characteristic-function, and second-moment identities for $\mu_k$.

background

This module sits in the Gravity analysis layer of the Recognition Science monolith and imports the SpectralConvergence toolkit (QG full-theory campaign, Phase 2a). That upstream file supplies quantitative eigenvalue limits and is marked theorem-complete: axiom-clean, no sorry.

The local objects are the discrete sine eigenvalue on a periodic $N$-site ring, $\lambda_N(k)=4N^2\sin^2(\pi k/N)$, its continuum limit, and the one-mode Gaussian built from that eigenvalue. In lattice units the discrete operator is the exact finite-difference Hessian of a free scalar (or linearized metric mode) on the cylinder; the continuum eigenvalue is the corresponding $k^2$-type symbol. Mode variance is the reciprocal scale that normalizes the Gaussian, and modeMeasure is the resulting probability measure on the complex (or real) mode amplitude.

Sibling lemmas record nonnegativity of $\lambda_N$ and of the real variance, the coercion between real and complex variance, that modeMeasure is a probability measure, and closed forms for $\int e^{it\cdot},d\mu$ and the second moment.

proof idea

Definition-heavy preflight module. Eigenvalues and variances are closed-form defs; nonnegativity follows from $\sin^2\ge 0$ and algebraic rearrangement. The probability-measure instance, characteristic function, and second-moment identities are short measure-theory calculations against the explicit Gaussian density (Mathlib Gaussian/characteristic-function lemmas), not a multi-step spectral argument. No deep induction or forcing-chain step lives here.

why it matters in Recognition Science

One-mode cylinder preflight is the bookkeeping layer before spectral convergence and continuum limits in the gravity analysis campaign. Upstream SpectralConvergence is the reusable Phase 2a toolkit this file prepares inputs for; downstream consumers are not yet wired in the graph (used_by empty), so the module is infrastructure rather than a cited parent theorem.

In the broader RS gravity story, discrete-to-continuum eigenvalue control is the analytic step that lets lattice recognition costs pass to continuum effective actions. The eight-tick and $D=3$ landmarks are not invoked directly; the file stays inside classical Fourier analysis on the circle. It closes no open scaffold by itself, but supplies the exact $\lambda_N(k)$ expression referenced as discrete_sine_eigenvalue_expansion.

scope and limits

Does not prove N→∞ spectral convergence; only defines the finite-N and continuum symbols.
Does not treat multi-mode coupling, interactions, or nonlinear Hessian terms.
Does not derive continuum gravity field equations or RS mass/ladder formulae.
Does not claim axiom-level status beyond the imported SpectralConvergence toolkit.
Does not fix boundary conditions other than the periodic N-site ring.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.SpectralConvergence module_import

declarations in this module (21)

def latticeEigenvalue L104
def continuumEigenvalue L109
def modeVarianceReal L113
def modeVariance L116
def modeMeasure L120
theorem latticeEigenvalue_nonneg L123
theorem modeVarianceReal_nonneg L128
theorem coe_modeVariance L133
instance instIsProbabilityMeasureModeMeasure L139
theorem integral_exp_modeMeasure L150
theorem charFun_modeMeasure L161
theorem secondMoment_modeMeasure L172
theorem latticeEigenvalue_lower_bound L187
theorem latticeEigenvalue_pos L212
theorem modeVarianceReal_pos L225
theorem modeVariance_ne_zero L232
theorem modeVarianceReal_rate L243
theorem modeVarianceReal_tendsto L292
theorem secondMoment_tendsto L300
theorem charFun_modeMeasure_tendsto L312
theorem limitVariance_pos L334